Switch order of product of measurable spaces

Stream: Is there code for X?

[Josha Dekker]

I'm trying to show that convolution of measures on a CommMonoid is commutative. On paper the proof is straightforward (included in the docstring in the below example), but I need to somehow reverse the order of coordinates in both the function and the product of measures in the application of map, and I'm not sure how to do this; it would boil down to filling in the sorry.

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 μ ν)

/-- To get commutativity, we need the underlying multiplication to be commutative. In this case,
we get for f(x,y) = xy that f⁻¹(B) = symm f⁻¹(B), where 'symm' is suggestive notation for flipping
around the cartesian coordinates. We can then use:
(μ*ν)(B) = (μ × ν)(f⁻¹(B)) = (μ × ν) (symm f⁻¹(B)) = (ν × μ) (f⁻¹(B)) = (ν × μ)(B). -/
theorem comm {M : Type*} [CommMonoid M] [MeasurableSpace M] (μ : Measure M) (ν : Measure M) :
    μ.conv ν = ν.conv μ := by
  unfold conv
  have : (fun x : (M × M) ↦ x.1 * x.2) = (fun x : (M × M) ↦ x.2 * x.1) := by
    ext x
    exact mul_comm x.1 x.2
  calc
    map (fun x ↦ x.1 * x.2) (Measure.prod μ ν) = map (fun x ↦ x.2 * x.1) (Measure.prod μ ν) := by
      rw [this]
    _ = map (fun x ↦ x.1 * x.2) (Measure.prod ν μ) := by
      sorry

[Josha Dekker]

Any suggestions to make the proof more streamlined are welcome as well, of course! I had an earlier post about associativity of convolution, but (as far as I could tell) that requires stronger assumptions on the underlying space than I originally thought, so I've removed that post.

[Yury G. Kudryashov]

Try docs#MeasureTheory.Measure.prod_swap

[Yury G. Kudryashov]

Note that the definition of the product of measures is not symmetric, so you need the measures to be s-finite.

[Yaël Dillies]

Can't you use the fact that Prod.swap : M × M → M × M sends μ.prod ν to ν.prod μ?

[Yury G. Kudryashov]

The following proof should work (not tested):

  unfold conv
  rw [← prod_swap]
  simp only [Prod.swap, mul_comm]

[Yury G. Kudryashov]

Should we introduce Measure.map₂ similarly to Set.image2, Filter.map₂ etc?

[Yury G. Kudryashov]

With conv μ ν := map₂ (⋅ * ⋅) μ ν

[Josha Dekker]

I've tried that proof, but it doesn't fully cut it yet. Simp doesn't make progress (I've added SFinite for both measures)

[Josha Dekker]

I've written out three versions, all three proofs are incomplete.

Also, perhaps I'm misunderstanding this, but I'm a bit confused that we would need SFinite for this, or is this assumption very innocuous?

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 μ ν)

theorem comm1 {M : Type*} [CommMonoid M] [MeasurableSpace M] (μ : Measure M) (ν : Measure M) [SFinite μ] [SFinite ν]:
    μ.conv ν = ν.conv μ := by
  unfold conv
  rw [← prod_swap]
  have : map (fun x ↦ x.1 * x.2) (map Prod.swap (Measure.prod ν μ)) =
      map (fun x ↦ x.2 * x.1) (map Prod.swap (Measure.prod ν μ)) := by
    simp only [mul_comm]
  rw [this]
  sorry

theorem comm2 {M : Type*} [CommMonoid M] [MeasurableSpace M] (μ : Measure M) (ν : Measure M) [SFinite μ] [SFinite ν]:
    μ.conv ν = ν.conv μ := by
  unfold conv
  rw [← prod_swap]
  simp only [Prod.swap, mul_comm]
  sorry

theorem comm3 {M : Type*} [CommMonoid M] [MeasurableSpace M] (μ : Measure M) (ν : Measure M) [SFinite μ] [SFinite ν]:
    μ.conv ν = ν.conv μ := by
  unfold conv
  have : (fun x : (M × M) ↦ x.1 * x.2) = (fun x : (M × M) ↦ x.2 * x.1) := by
    ext x
    exact mul_comm x.1 x.2
  calc
    map (fun x ↦ x.1 * x.2) (Measure.prod μ ν) = map (fun x ↦ x.2 * x.1) (Measure.prod μ ν) := by
      rw [this]
    _ = map (fun x ↦ x.1 * x.2) (Measure.prod ν μ) := by
      rw [← prod_swap]
      simp only [Prod.swap, mul_comm]
      sorry

[Josha Dekker]

Yury G. Kudryashov said:

Should we introduce Measure.map₂ similarly to Set.image2, Filter.map₂ etc?

Perhaps that is useful yes, do you think that would make it easier to work with e.g. convolutions of measures?

[Yury G. Kudryashov]

theorem comm {M : Type*} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M]
    (μ : Measure M) (ν : Measure M) [SFinite μ] [SFinite ν] : μ.conv ν = ν.conv μ := by
  unfold conv
  rw [← prod_swap, map_map]
  · simp [Function.comp_def, mul_comm]
  all_goals { measurability }

[Yury G. Kudryashov]

@Floris van Doorn @Sebastien Gouezel What do you think about map₂?

[Yury G. Kudryashov]

I'm not sure if there are applications besides convolution (multiplicative+additive).

[Yury G. Kudryashov]

If no, then it makes no sense to introduce map₂.

[Floris van Doorn]

I'm not sure if there are applications other than convolution of map₂, but it seems like a natural operation to define.

[Terence Tao]

It would describe the law of any binary operation applied to two independent random variables, which is a common enough operation in probability theory that I think it's worth setting up some API for (and for this application at least, the sigma-finite hypothesis is no restriction). For instance, besides addition and multiplication, subtraction of two random variables is quite common, as is max and min. And one can start accessing triples, quadruples, etc. of independent random variables once one has API for pairs by grouping together one pair at a time (although it is possible to also work with iIndepFun after developing some further API there, which is what we did for PFR).

[Josha Dekker]

Yury G. Kudryashov said:

theorem comm {M : Type*} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M]
    (μ : Measure M) (ν : Measure M) [SFinite μ] [SFinite ν] : μ.conv ν = ν.conv μ := by
  unfold conv
  rw [← prod_swap, map_map]
  · simp [Function.comp_def, mul_comm]
  all_goals { measurability }

Thank you!

[Josha Dekker]

I put the definition of convolution of measures, commutativity of convolution of measures on CommMonoid and the finiteness of convolution of measures in #9372. This is very much WIP, feel free to add to this! Progress will probably be slow on my end, from my background I'm used to dealing with convolutions of measures in the probability theory setting, for which I'm used to having a bit more structure on the underlying space! If anyone has any recommendations for a good source for the more general theory, I am happy to hear them!

[Josha Dekker]

If we want to integrate this with a pr that adds Measure.map₂, that is also fine with me of course!