Convolution.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 981 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned Carleson blueprint

5 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Mathlib.Analysis.Convolution

Imported by 1 file

Carleson.lean

theorem MeasureTheory.convolution_symm Special case of convolution_flip when L is symmetric line 28 source
Source documentation
Special case of convolution_flip when L is symmetric.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, NontriviallyNormedField, NormedSpace, MeasurableSpace, ContinuousLinearMap, RingHom.id, Eq, Real, AddCommGroup, MeasureTheory.Measure, MeasureTheory.Measure.IsAddLeftInvariant, MeasureTheory.Measure.IsNegInvariant, MeasurableNeg, MeasurableAdd, MeasureTheory.convolution
Proof uses: ContinuousLinearMap.flip, ContinuousLinearMap.ext, of_eq_true, Eq.trans, True, congrFun', congrArg, eq_self, Eq.mpr, id, Eq.symm, MeasureTheory.convolution_flip, Eq.refl
114 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem convolution_symm {f : G → E} {g : G → E} (L : E →L[𝕜] E →L[𝕜] F)
    (hL : ∀ (x y : E), L x y = L y x) [NormedSpace ℝ F] [AddCommGroup G]
    {μ : Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant] [MeasurableNeg G] [MeasurableAdd G] :
    f ⋆[L, μ] g = g ⋆[L, μ] f := by
…
```
Mentions: E, g
theorem MeasureTheory.AEStronglyMeasurable.convolution The convolution of two a.e. strongly measurable functions is a.e. strongly measurable line 39 source
Source documentation
The convolution of two a.e. strongly measurable functions is a.e. strongly measurable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, NontriviallyNormedField, NormedSpace, ContinuousLinearMap, RingHom.id, MeasurableSpace, AddGroup, MeasurableAdd₂, MeasurableNeg, MeasureTheory.Measure, MeasureTheory.SigmaFinite, Real, MeasureTheory.Measure.IsAddRightInvariant, MeasureTheory.AEStronglyMeasurable, MeasureTheory.convolution
Proof uses: Prod, HSub.hSub, MeasureTheory.Measure.prod, MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving, Prod.fst, Prod.snd, MeasureTheory.QuasiMeasurePreserving.prod_of_left, MeasurableSub₂.measurable_sub, Filter.univ_mem', MeasureTheory.ae, Set.ofPred, MeasureTheory.Measure.QuasiMeasurePreserving, Prod.mk, id, Membership.mem, Set, MeasureTheory.Measure.QuasiMeasurePreserving.mk, MeasurableSub.measurable_sub_const, Eq.mpr, MeasureTheory.Measure.AbsolutelyContinuous and 8 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
protected theorem AEStronglyMeasurable.convolution [NormedSpace ℝ F] [μ.IsAddRightInvariant]
    (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
    AEStronglyMeasurable (f ⋆[L, μ] g) μ := by
…
```
Mentions: g
lemma MeasureTheory.lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm This implies both of the following theorems convolutionExists_of_memLp_memLp and enorm_convolution_le_eLpNorm_mul_eLpNorm line 49 source
Source documentation
This implies both of the following theorems convolutionExists_of_memLp_memLp and enorm_convolution_le_eLpNorm_mul_eLpNorm.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, NontriviallyNormedField, NormedSpace, ContinuousLinearMap, RingHom.id, MeasurableSpace, AddGroup, MeasurableAdd₂, MeasurableNeg, MeasureTheory.Measure, MeasureTheory.SigmaFinite, MeasureTheory.Measure.IsNegInvariant, MeasureTheory.Measure.IsAddLeftInvariant, ENNReal, ENNReal.HolderConjugate, LE.le, Real, Norm.norm, HMul.hMul, MeasureTheory.AEStronglyMeasurable and 4 more
Proof uses: Eq.mpr, Function.comp, id, Eq, congrArg, Eq.symm, MeasureTheory.eLpNorm_comp_measurePreserving, MeasureTheory.Measure.measurePreserving_sub_left, HDiv.hDiv, OfNat.ofNat, HAdd.hAdd, Inv.inv, congr, div_one, one_div, ENNReal.HolderConjugate.inv_add_inv_eq_one, ENNReal.HolderTriple, ENNReal.HolderTriple.mk, semiOutParam, inv_one and 34 more
197 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm
    [μ.IsNegInvariant] [μ.IsAddLeftInvariant] {p q : ENNReal} (hpq : p.HolderConjugate q)
    (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖)
    (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) :
    ∫⁻ a, ‖L (f a) (g (x₀ - a))‖ₑ ∂μ ≤ eLpNorm f p μ * eLpNorm g q μ := by
…
```
Mentions: g
theorem MeasureTheory.ConvolutionExists.of_memLp_memLp If MemLp f p μ and MemLp g q μ, where p and q are Hölder conjugates, then the convolution of f and g exists everywhere line 67 source
Source documentation
If MemLp f p μ and MemLp g q μ, where p and q are Hölder conjugates, then the convolution of f and g exists everywhere.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, NontriviallyNormedField, NormedSpace, ContinuousLinearMap, RingHom.id, MeasurableSpace, AddGroup, MeasurableAdd₂, MeasurableNeg, MeasureTheory.Measure, MeasureTheory.SigmaFinite, MeasureTheory.Measure.IsNegInvariant, MeasureTheory.Measure.IsAddLeftInvariant, MeasureTheory.Measure.IsAddRightInvariant, ENNReal, ENNReal.HolderConjugate, LE.le, Real, Norm.norm, HMul.hMul and 3 more
Proof uses: And.intro, HSub.hSub, MeasureTheory.HasFiniteIntegral, MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd, lt_of_le_of_lt, MeasureTheory.lintegral, ENorm.enorm, MeasureTheory.eLpNorm, Top.top, MeasureTheory.lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm, Ne.lt_top, ENNReal.mul_ne_top, MeasureTheory.MemLp.eLpNorm_ne_top
142 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem ConvolutionExists.of_memLp_memLp
    [μ.IsNegInvariant] [μ.IsAddLeftInvariant] [μ.IsAddRightInvariant]
    {p q : ENNReal} (hpq : p.HolderConjugate q)
    (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖) (hf : AEStronglyMeasurable f μ)
    (hg : AEStronglyMeasurable g μ) (hfp : MemLp f p μ) (hgq : MemLp g q μ) :
    ConvolutionExists f g L μ := by
…
```
Mentions: g
theorem MeasureTheory.enorm_convolution_le_eLpNorm_mul_eLpNorm If p and q are Hölder conjugates, then the convolution of f and g is bounded everywhere by eLpNorm f p μ * eLpNorm g q μ line 79 source
Source documentation
If p and q are Hölder conjugates, then the convolution of f and g is bounded everywhere by eLpNorm f p μ * eLpNorm g q μ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, NontriviallyNormedField, NormedSpace, ContinuousLinearMap, RingHom.id, MeasurableSpace, AddGroup, MeasurableAdd₂, MeasurableNeg, MeasureTheory.Measure, MeasureTheory.SigmaFinite, Real, MeasureTheory.Measure.IsNegInvariant, MeasureTheory.Measure.IsAddLeftInvariant, ENNReal, ENNReal.HolderConjugate, LE.le, Norm.norm, HMul.hMul, MeasureTheory.AEStronglyMeasurable and 3 more
Proof uses: LE.le.trans, MeasureTheory.integral, HSub.hSub, MeasureTheory.lintegral, MeasureTheory.enorm_integral_le_lintegral_enorm, MeasureTheory.lintegral_enorm_convolution_integrand_le_eLpNorm_mul_eLpNorm
146 instances, coercions and auxiliary constants left out.
```
theorem enorm_convolution_le_eLpNorm_mul_eLpNorm [NormedSpace ℝ F]
    [μ.IsNegInvariant] [μ.IsAddLeftInvariant] {p q : ENNReal} (hpq : p.HolderConjugate q)
    (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ ‖f x‖ * ‖g y‖)
    (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x₀ : G) :
    ‖(f ⋆[L, μ] g) x₀‖ₑ ≤ eLpNorm f p μ * eLpNorm g q μ :=
…
```
Mentions: g