Could not infer OfNat in definition of measure-convolution

Stream: new members

[Josha Dekker]

I'm trying to define the convolution of measures through Measure.ofMeasurable, but I'm getting a 'failed to synthesise instance' error in my Set.indicator function; what am I doing wrong?

import Mathlib.Analysis.Fourier.FourierTransform
import Mathlib.Probability.Notation
import Mathlib.MeasureTheory.Measure.MeasureSpaceDef
import Mathlib.Algebra.Function.Indicator

open MeasureTheory ComplexConjugate Complex

noncomputable def convolution [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) (ν : Measure G) : Measure G := by
  apply Measure.ofMeasurable ((s : Set G) → MeasurableSet s → ∫ x, ∫ y, Set.indicator ∅ (fun _ ↦ 1) (x*y) ∂μ ∂ν)

[Josha Dekker]

(deleted)

[Ruben Van de Velde]

Lean doesn't know what type the 1 should be. What is that type?

[Josha Dekker]

Ruben Van de Velde said:

Lean doesn't know what type the 1 should be. What is that type?

(extended) real numbers, it’s supposed to give a measure… I’m using the definition based on push forward of group action now, I think that is slightly more useful for what I’m doing!

[Yaël Dillies]

Are you sure you want docs#EReal and not docs#ENNReal ?

[Ruben Van de Velde]

Did you mean

noncomputable def convolution [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) (ν : Measure G) : Measure G := by
  apply Measure.ofMeasurable (fun (s : Set G) (hs : MeasurableSet s) => ∫ x, ∫ y, (Set.indicator ∅ (fun _ ↦ 1) (x*y)) ∂μ ∂ν)

? Though that still doesn't work

[Josha Dekker]

Yes, ENNReal

[Josha Dekker]

Ruben Van de Velde said:

Did you mean

noncomputable def convolution [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ : Measure G) (ν : Measure G) : Measure G := by
  apply Measure.ofMeasurable (fun (s : Set G) (hs : MeasurableSet s) => ∫ x, ∫ y, (Set.indicator ∅ (fun _ ↦ 1) (x*y)) ∂μ ∂ν)

? Though that still doesn't work

Yes, that placement of brackets is correct indeed, I’ll change it and see if I can figure out what is going wrong

[Rémy Degenne]

Another problem in your code: Measure.ofMeasurable takes a first argument with type (s : Set α) → MeasurableSet s → ENNReal, but you are using Bochner integrals: they work in a NormedAddCommGroup and ENNReal isn't one. You should use the Lebesgue integral instead, which is ENNReal valued.

[Rémy Degenne]

A better start:

noncomputable def convolution [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G] [BorelSpace G] (μ ν : Measure G) :
    Measure G :=
  Measure.ofMeasurable (fun s hs ↦ ∫⁻ x, ∫⁻ y, s.indicator (fun _ ↦ 1) (x*y) ∂μ ∂ν) _ _

[Josha Dekker]

Hmm, that is a bit problematic indeed. I was planning to add convolution of probability measures, so would you suggest first defining convolution of measures in maximum generality (push-forward of the group action) and later-on specialising to NormedAddCommGroup's or using the Bochner integral definition and focusing only on NormedAddCommGroup's?

[Rémy Degenne]

I don't get what the problem is. You want to define a measure, with values in ENNReal, hence in the code I wrote we use the Lebesgue measure, which takes values in ENNReal. Why do you want to use the Bochner integral?

[Josha Dekker]

I'm sorry, my message was a bit vague/confused as I was still wrapping my head around this. Your definition works perfectly fine! I'll try to work out the basic API for convolution of measures; this can then hopefully be used to show that the charFun of the sum of two independent random variables is the product of their charFun's

[Josha Dekker]

I'm finding that I need to improve my familiarity with Lean a bit more, I'll probably have to focus on that first for now. I'll get back at defining convolutions when I have a bit more lean-tricks up my sleeve, if someone hasn't added them by then (e.g. for the CLT project)

[Terence Tao]

I would have thought it would be simpler to use as a definition

import Mathlib

open MeasureTheory

noncomputable def conv {G : Type*} [TopologicalSpace G] [Group G] [TopologicalGroup G] [MeasurableSpace G]
                              [BorelSpace G] (μ : Measure G) (ν : Measure G) : Measure G :=
  Measure.map (fun x : G × G ↦ x.1 * x.2) (Measure.prod μ ν)

[Josha Dekker]

You are right, that definition is certainly nicer to work with and probably the one we should add to Mathlib and the CLT project; I tried getting the other approach to work today, but I find explicitly working with Lebesgue integrals and series a bit unwieldy in Lean. This may be due to my severe lack of experience with those in Lean. I'll try to write something up for this definition if I have time for this. If someone else wants to add convolutions of measures and basic API, please go ahead!

[Terence Tao]

Incidentally this definition works just fine for monoids with a measurable multiplication structure. I can't think of an immediate application of this (convolution on the natural numbers or the nonnegative reals, perhaps?), but I thought I'd mention it before anyone gets too deep in building the API in case this extension becomes useful in the future.

[Josha Dekker]

My work on measure-convolution has been laying around for a bit on #9372, I guess the next step would be to show that the integral and Measure.map definitions agree. For the latter I tried working it out, but I had some issues that I could not resolve quickly. I've commented it out for now (this is #9372), I'm happy to receive feedback in the meantime (I can also remove it and make a follow-up PR later!)

I'll make a new Zulip thread for the sorry's that I couldn't fill in yet