Three questions on Set.indicator

Stream: mathlib4

[Josha Dekker]

In working on #9372, I found that I could not fill in three sorry's in the following, where each sorry revolves around the behaviour of Set.indicator:

import Mathlib.MeasureTheory.Constructions.Prod.Basic
import Mathlib.MeasureTheory.Measure.MeasureSpace

noncomputable section

namespace MeasureTheory

namespace Measure

def conv_int {M : Type*} [TopologicalSpace M] [Group M] [TopologicalGroup M]
    [MeasurableSpace M] [BorelSpace M] (μ ν : Measure M) : Measure M := by
  apply Measure.ofMeasurable (fun s hs ↦ ∫⁻ x, ∫⁻ y, s.indicator (fun _ ↦ 1) (x*y) ∂μ ∂ν)
  · rw [Set.indicator_empty]
    simp
  · intro f hf hfdis
    rw [← MeasureTheory.lintegral_tsum]
    · congr
      ext x
      rw [← MeasureTheory.lintegral_tsum]
      · congr
        ext y
        sorry
      · intro i
        sorry
    · intro i
      sorry

The first is due to that we only have things like https://github.com/leanprover-community/mathlib4/blob/8666bd82efec40b8b3a5abca02dc9b24bbdf2652/Mathlib/Algebra/IndicatorFunction.lean#L668-L668 and not a countable version of this (we'd perhaps need non-negativity assumptions, but these are fine in my setting).
The second and third seem very easy, but my various Loogle and Moogle searches have failed me so far...

[Yury G. Kudryashov]

What's your goal? E.g., can you define the measure you're looking for using existing prod, map, and withDensity constructions?

[Yury G. Kudryashov]

Or some of these constructions need more assumptions about the original measures than you want to have here?

[Yury G. Kudryashov]

(e.g., can we assume that the measures are SFinite?)

[Josha Dekker]

So what I'm trying to do is to define a definition of the convolution of measures, different from the one in my PR #9372, to hopefully show (at one point) that they're equal, to add some more API to that PR (I feel that sometimes this definition may be easier to show certain properties of convolutions)

[Josha Dekker]

The other definition, conv in #9372, does not use SFinite. In the above problem, only one of the sorry's has an integral, so I would want to avoid SFinite if possible.

[Josha Dekker]

(I'm aware that naming the intro f is bad practice as it is a collection of sets, I'll rename that if I add it to the PR of course)

[Yury G. Kudryashov]

The definition doesn't need SFinite but commutativity may need it.

[Yury G. Kudryashov]

What properties of the convolution need this definition and don't follow from the definition using prod and map?

[Josha Dekker]

Yury G. Kudryashov said:

What properties of the convolution need this definition and don't follow from the definition using prod and map?

I'm not yet sure which definitions exactly, I would think that associativity may be easier through this channel. Besides that, it is a common way of writing convolution of measures, so I thought we'd like to have it anyway (as a definition or a theorem)?

[Yury G. Kudryashov]

It may be easier to do it as a theorem.

[Yury G. Kudryashov]

We try to have only 1 definition of each notion and link other "definitions" by theorems.

[Josha Dekker]

Okay! I’ll rewrite it to that later today/this week and see whether my problems disappear!

[Josha Dekker]

I've returned to this and tried to show the following, which I think is about the right way of writing that the map-based definition equals the integral-based one, but I just don't manage to simplify this further. I tried using MeasureTheory.lintegral_prod, but it doesn't seem to work....

import Mathlib.MeasureTheory.Constructions.Prod.Basic
import Mathlib.MeasureTheory.Measure.MeasureSpace

noncomputable section

namespace MeasureTheory

namespace Measure

/-- Convolutions of measures. They are defined for arbitrary measures on a monoid M that is also
a measurable space. TODO: should get a to_additive version for AddMonoids -/
def conv {M : Type*} [Monoid M] [MeasurableSpace M] (μ : Measure M) (ν : Measure M) :
    Measure M := Measure.map (fun x : M × M ↦ x.1 * x.2) (Measure.prod μ ν)

lemma convolution_eq_lintegral {G : Type*} [TopologicalSpace G] [Group G] [TopologicalGroup G]
    [MeasurableSpace G] [BorelSpace G] (μ ν : Measure G) [SFinite μ] [SFinite ν]
    (B : Set G) (hB : MeasurableSet B) :
    (μ.conv ν) B = ∫⁻ x, ∫⁻ y, B.indicator (fun _ ↦ 1) (x*y) ∂μ ∂ν := by
  rw [conv]
  sorry

[Josha Dekker]

I’m still trying to get the hang of map and lintegrals, so any pointers (or a solution) are highly appreciated!

[Josha Dekker]

Probably the assumptions can be weakened, but I wanted to have a ‘nice’ setting first

[Josha Dekker]

#9372 is a PR just introducing the definition of convolution of measures and some very basic results, any feedback on this is very welcome as well as API additions!