MeanInequalities.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

24 declarations, 0 contain sorry, 0 declared as axioms

Imports (3)

Imported by 4 files

theorem ENNReal.Lp_add_le_sum Minkowski inequality for finite sums of ENNReal-valued functions line 19 source
Source documentation
Minkowski inequality for finite sums of ENNReal-valued functions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finset, ENNReal, Real, LE.le, OfNat.ofNat, HPow.hPow, Finset.sum, HDiv.hDiv
Proof uses: LT.lt, lt_of_lt_of_le, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, Nat, div_pos, Finset.cons_induction, id, EmptyCollection.emptyCollection, Eq.mpr, Eq, congrFun', congrArg, Finset.sum_congr, Membership.mem, ENNReal.zero_rpow_of_pos and 14 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem Lp_add_le_sum
    {ι κ : Type*} {s : Finset ι} {t : Finset κ} {f : ι → κ → ℝ≥0∞} {p : ℝ} (hp : 1 ≤ p) :
    (∑ i ∈ s, (∑ j ∈ t, f i j) ^ p) ^ (1 / p) ≤ ∑ j ∈ t, (∑ i ∈ s, f i j ^ p) ^ (1 / p) := by
…
```
Mentions: s
theorem ENNReal.lintegral_prod_norm_pow_le' A version of Hölder with multiple arguments, allowing ∞ as an exponent line 37 source
Source documentation
A version of Hölder with multiple arguments, allowing ∞ as an exponent.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Finset, ENNReal, Membership.mem, AEMeasurable, Eq, Finset.sum, Inv.inv, OfNat.ofNat, LE.le, MeasureTheory.lintegral, Finset.prod, MeasureTheory.eLpNorm
Proof uses: Finset.strongInduction, LT.lt, dite, Exists, And, Top.top, Trans.trans, HMul.hMul, Finset.erase, Classical.propDecidable, rfl, MeasureTheory.lintegral_congr, Eq.symm, Finset.mul_prod_erase, Eq.mpr, id, congrArg, MeasureTheory.lintegral_const_mul'', Finset.aemeasurable_fun_prod, Finset.mem_of_mem_erase and 57 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
theorem lintegral_prod_norm_pow_le' {α ι : Type*} [MeasurableSpace α] {μ : Measure α}
    {s : Finset ι} {f : ι → α → ℝ≥0∞} (hf : ∀ i ∈ s, AEMeasurable (f i) μ)
    {p : ι → ℝ≥0∞} (hp : ∑ i ∈ s, (p i)⁻¹ = 1) :
    ∫⁻ (a : α), ∏ i ∈ s, f i a ∂μ ≤ ∏ i ∈ s, eLpNorm (f i) (p i) μ := by
…
```
Mentions: s
theorem ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm Hölder's inequality for functions α → ℝ≥0∞, using exponents in ℝ≥0∞ line 78 source
Source documentation
Hölder's inequality for functions α → ℝ≥0∞, using exponents in ℝ≥0∞

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, ENNReal.HolderConjugate, AEMeasurable, LE.le, MeasureTheory.lintegral, HMul.hMul, MeasureTheory.eLpNorm
Proof uses: dite, Or, Eq, Top.top, Not, Classical.em, le_of_le_of_eq, essSup, MeasureTheory.lintegral_mono_ae, Filter.Eventually.mono, MeasureTheory.ae, ENNReal.ae_le_essSup, mul_left_mono, of_eq_true, Eq.trans, True, congr, congrArg, MeasureTheory.lintegral_const_mul'', ite and 47 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
theorem lintegral_mul_le_eLpNorm_mul_eLqNorm {p q : ℝ≥0∞} (hpq : p.HolderConjugate q)
    {f g : α → ENNReal} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    ∫⁻ (a : α), (f * g) a ∂μ ≤ eLpNorm f p μ * eLpNorm g q μ := by
…
```
Mentions: g
theorem ENNReal.sq_lintegral_mul_le_mul_lintegral_sq Cauchy–Schwarz inequality for functions α → ℝ≥0∞ (Hölder's inequality squared) line 93 source
Source documentation
Cauchy–Schwarz inequality for functions α → ℝ≥0∞ (Hölder's inequality squared).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ENNReal, AEMeasurable, LE.le, HPow.hPow, Nat, MeasureTheory.lintegral, HMul.hMul, OfNat.ofNat
Proof uses: Eq.mpr, Real, HDiv.hDiv, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, HPow, funext, id, congrArg, mul_pow, ENNReal.rpow_natCast, ENNReal.rpow_mul, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.instAddMonoidWithOne' and 22 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem sq_lintegral_mul_le_mul_lintegral_sq {f g : α → ℝ≥0∞}
    (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    (∫⁻ a, f a * g a ∂μ) ^ 2 ≤ (∫⁻ a, f a ^ 2 ∂μ) * ∫⁻ a, g a ^ 2 ∂μ := by
…
```
Mentions: g

lemma r_sub_p_nonneg Used in the proof of Young's convolution inequality line 111 source

Source comment

Used in the proof of Young's convolution inequality

private lemma r_sub_p_nonneg {p q r : ℝ} (p0 : 0 < p) (hq : 1 ≤ q) (r0 : 0 < r)
    (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1) : 0 ≤ r - p := by
…

lemma ENNReal.eLpNorm_eq_eLpNorm_rpow line 128 source
theorem ENNReal.convolution_zero_of_c_nonpos Used to handle trivial case c ≤ 0 when proving versions of Young's convolution inequality assuming ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) line 152 source
Source comment
Used to handle trivial case `c ≤ 0` when proving versions of Young's convolution inequality assuming `∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖)`
```
private theorem convolution_zero_of_c_nonpos [AddGroup G] {f : G → E} {g : G → E'} {c : ℝ}
    (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) (hc : c ≤ 0) : f ⋆[L, μ] g = 0 := by
…
```
Mentions: E, g, c

theorem ENNReal.eLpNorm_top_convolution_le_aux Auxiliary inequality used to prove inequalities with simpler conditions on f and g line 162 source

Source comment

Auxiliary inequality used to prove inequalities with simpler conditions on f and g.

private theorem eLpNorm_top_convolution_le_aux [AddGroup G] {p q : ℝ≥0∞}
    (hpq : p.HolderConjugate q) {f : G → E} {g : G → E'} (hf : AEMeasurable (‖f ·‖ₑ) μ)
    (hg : ∀ x : G, AEMeasurable (‖g <| x - ·‖ₑ) μ)
    (hg' : ∀ x : G, eLpNorm (‖g <| x - ·‖ₑ) q μ = eLpNorm (‖g ·‖ₑ) q μ)
    (c : ℝ) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :
    eLpNorm (f ⋆[L, μ] g) ∞ μ ≤ ENNReal.ofReal c * eLpNorm f p μ * eLpNorm g q μ := by
…

Mentions: E, g, c

theorem ENNReal.eLpNorm_top_convolution_le Special case of Young's convolution inequality when r = ∞ line 187 source
Source documentation
Special case of Young's convolution inequality when r = ∞.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, NontriviallyNormedField, NormedSpace, Real, ContinuousLinearMap, RingHom.id, AddGroup, TopologicalSpace, IsTopologicalAddGroup, BorelSpace, MeasureTheory.Measure.IsAddHaarMeasure, LocallyCompactSpace, SecondCountableTopology, OpensMeasurableSpace, MeasureTheory.Measure.IsNegInvariant, ENNReal, ENNReal.HolderConjugate, AEMeasurable and 7 more
Proof uses: AEMeasurable.enorm, Function.comp, HSub.hSub, AEMeasurable.comp_quasiMeasurePreserving, MeasureTheory.quasiMeasurePreserving_sub_left, MeasureTheory.eLpNorm_comp_measurePreserving', MeasureTheory.Measure.measurePreserving_sub_left
144 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_top_convolution_le [MeasurableSpace E] [OpensMeasurableSpace E]
    [MeasurableSpace E'] [OpensMeasurableSpace E'] [μ.IsNegInvariant] {p q : ℝ≥0∞}
    (hpq : p.HolderConjugate q) {f : G → E} {g : G → E'} (hf : AEMeasurable f μ)
    (hg : AEMeasurable g μ) (c : ℝ) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :
    eLpNorm (f ⋆[L, μ] g) ∞ μ ≤ ENNReal.ofReal c * eLpNorm f p μ * eLpNorm g q μ := by
…
```
Mentions: E, g, c
theorem ENNReal.eLpNorm_top_convolution_le' Special case of Young's convolution inequality when r = ∞ line 197 source
Source documentation
Special case of Young's convolution inequality when r = ∞.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, NontriviallyNormedField, NormedSpace, Real, ContinuousLinearMap, RingHom.id, AddGroup, TopologicalSpace, IsTopologicalAddGroup, BorelSpace, MeasureTheory.Measure.IsAddHaarMeasure, LocallyCompactSpace, SecondCountableTopology, MeasureTheory.Measure.IsNegInvariant, ENNReal, ENNReal.HolderConjugate, MeasureTheory.AEStronglyMeasurable, LE.le and 6 more
Proof uses: MeasureTheory.AEStronglyMeasurable.enorm, Function.comp, HSub.hSub, MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving, MeasureTheory.quasiMeasurePreserving_sub_left, MeasureTheory.eLpNorm_comp_measurePreserving, MeasureTheory.Measure.measurePreserving_sub_left
144 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_top_convolution_le' [μ.IsNegInvariant] {p q : ℝ≥0∞} (hpq : p.HolderConjugate q) {f : G → E} {g : G → E'}
    (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (c : ℝ)
    (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :
    eLpNorm (f ⋆[L, μ] g) ∞ μ ≤ ENNReal.ofReal c * eLpNorm f p μ * eLpNorm g q μ := by
…
```
Mentions: E, g, c
theorem ENNReal.enorm_convolution_le_eLpNorm_mul_eLpNorm_mul_eLpNorm_aux line 208 source
theorem ENNReal.enorm_convolution_le_eLpNorm_mul_eLpNorm_mul_eLpNorm This inequality is used in the proof of Young's convolution inequality eLpNorm_convolution_le_ofReal line 298 source
Source documentation
This inequality is used in the proof of Young's convolution inequality eLpNorm_convolution_le_ofReal. See enorm_convolution_le_eLpNorm_mul_eLpNorm_mul_eLpNorm' for a version assuming a.e. strong measurability instead.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, NontriviallyNormedField, NormedSpace, Real, ContinuousLinearMap, RingHom.id, AddGroup, TopologicalSpace, IsTopologicalAddGroup, BorelSpace, MeasureTheory.Measure.IsAddHaarMeasure, LocallyCompactSpace, SecondCountableTopology, OpensMeasurableSpace, MeasureTheory.Measure.IsNegInvariant, LE.le, OfNat.ofNat, Eq and 13 more
Proof uses: AEMeasurable.enorm, Function.comp, AEMeasurable.comp_quasiMeasurePreserving, MeasureTheory.quasiMeasurePreserving_sub_left
158 instances, coercions and auxiliary constants left out.
```
theorem enorm_convolution_le_eLpNorm_mul_eLpNorm_mul_eLpNorm [MeasurableSpace E]
    [OpensMeasurableSpace E] [MeasurableSpace E'] [OpensMeasurableSpace E']
    [μ.IsNegInvariant] {p q r : ℝ}
    (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
    {f : G → E} {g : G → E'} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
    (c : ℝ) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) (x : G) :
    ‖(f ⋆[L, μ] g) x‖ₑ ≤
      .ofReal c * eLpNorm (fun y ↦ (‖f y‖ₑ ^ p * ‖g (x - y)‖ₑ ^ q) ^ (1 / r)) (.ofReal r) μ *
      ((eLpNorm f (.ofReal p) μ) ^ ((r - p) / r) *
      (eLpNorm g (.ofReal q) μ) ^ ((r - q) / r)) :=
…
```
Mentions: E, g, c
theorem ENNReal.enorm_convolution_le_eLpNorm_mul_eLpNorm_mul_eLpNorm' This inequality is used in the proof of Young's convolution inequality eLpNorm_convolution_le_ofReal' line 314 source
Source documentation
This inequality is used in the proof of Young's convolution inequality eLpNorm_convolution_le_ofReal'.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, NontriviallyNormedField, NormedSpace, Real, ContinuousLinearMap, RingHom.id, AddGroup, TopologicalSpace, IsTopologicalAddGroup, BorelSpace, MeasureTheory.Measure.IsAddHaarMeasure, LocallyCompactSpace, SecondCountableTopology, MeasureTheory.Measure.IsNegInvariant, LE.le, OfNat.ofNat, Eq, HAdd.hAdd and 12 more
Proof uses: MeasureTheory.AEStronglyMeasurable.enorm, Function.comp, MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving, MeasureTheory.quasiMeasurePreserving_sub_left
158 instances, coercions and auxiliary constants left out.
```
theorem enorm_convolution_le_eLpNorm_mul_eLpNorm_mul_eLpNorm'
    [μ.IsNegInvariant] {p q r : ℝ}
    (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
    {f : G → E} {g : G → E'} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ)
    (c : ℝ) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) (x : G) :
    ‖(f ⋆[L, μ] g) x‖ₑ ≤
      .ofReal c * eLpNorm (fun y ↦ (‖f y‖ₑ ^ p * ‖g (x - y)‖ₑ ^ q) ^ (1 / r)) (.ofReal r) μ *
      ((eLpNorm f (.ofReal p) μ) ^ ((r - p) / r) *
      (eLpNorm g (.ofReal q) μ) ^ ((r - q) / r)) :=
…
```
Mentions: E, g, c

theorem ENNReal.eLpNorm_convolution_le_ofReal_aux Auxiliary inequality used to prove versions with simpler conditions on f and g line 327 source

Source comment

Auxiliary inequality used to prove versions with simpler conditions on `f` and `g`

private theorem eLpNorm_convolution_le_ofReal_aux
    [μ.IsAddRightInvariant] {p q r : ℝ}
    (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1) {f : G → E} {g : G → E'}
    (hf : AEMeasurable (‖f ·‖ₑ) μ) (hg : ∀ x : G, AEMeasurable (‖g <| x - ·‖ₑ) μ)
    (hg' : AEMeasurable (fun (x : G × G) ↦ ‖(g ∘ fun p ↦ p.1 - p.2) x‖ₑ ^ q) (μ.prod μ))
    (c : ℝ) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :
    eLpNorm (f ⋆[L, μ] g) (.ofReal r) μ ≤
    .ofReal c * eLpNorm f (.ofReal p) μ * eLpNorm g (.ofReal q) μ := by
…

Mentions: E, g, c

theorem ENNReal.eLpNorm_convolution_le_ofReal line 382 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, NontriviallyNormedField, NormedSpace, Real, ContinuousLinearMap, RingHom.id, AddGroup, TopologicalSpace, IsTopologicalAddGroup, BorelSpace, MeasureTheory.Measure.IsAddHaarMeasure, LocallyCompactSpace, SecondCountableTopology, OpensMeasurableSpace, MeasureTheory.Measure.IsAddRightInvariant, LE.le, OfNat.ofNat, Eq and 9 more
Proof uses: AEMeasurable.enorm, Function.comp, HSub.hSub, AEMeasurable.comp_quasiMeasurePreserving, MeasureTheory.quasiMeasurePreserving_sub_left, AEMeasurable.pow_const, Prod, MeasureTheory.Measure.prod, ENorm.enorm, Prod.fst, Prod.snd, MeasureTheory.quasiMeasurePreserving_sub
159 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem ENNReal.eLpNorm_convolution_le_ofReal' line 394 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, NontriviallyNormedField, NormedSpace, Real, ContinuousLinearMap, RingHom.id, AddGroup, TopologicalSpace, IsTopologicalAddGroup, BorelSpace, MeasureTheory.Measure.IsAddHaarMeasure, LocallyCompactSpace, SecondCountableTopology, MeasureTheory.Measure.IsAddRightInvariant, LE.le, OfNat.ofNat, Eq, HAdd.hAdd and 8 more
Proof uses: MeasureTheory.AEStronglyMeasurable.enorm, Function.comp, HSub.hSub, MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving, MeasureTheory.quasiMeasurePreserving_sub_left, AEMeasurable.pow_const, Prod, MeasureTheory.Measure.prod, ENorm.enorm, Prod.fst, Prod.snd, MeasureTheory.quasiMeasurePreserving_sub
159 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.

theorem ENNReal.eLpNorm_convolution_le_of_norm_le_mul_aux Auxiliary result to prove the following versions with simpler assumptions on f and g line 406 source

Source comment

Auxiliary result to prove the following versions with simpler assumptions on `f` and `g`

private theorem eLpNorm_convolution_le_of_norm_le_mul_aux
    [μ.IsAddRightInvariant] {p q r : ℝ≥0∞}
    (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
    {f : G → E} {g : G → E'} (hf : AEMeasurable (‖f ·‖ₑ) μ)
    (hg : ∀ (x : G), AEMeasurable (‖g <| x - ·‖ₑ) μ)
    (hg' : ∀ (x : G), eLpNorm (‖g <| x - ·‖ₑ) q μ = eLpNorm (‖g ·‖ₑ) q μ)
    (hg'' : AEMeasurable (fun x ↦ ‖(g ∘ fun p ↦ p.1 - p.2) x‖ₑ ^ q.toReal) (μ.prod μ))
    (c : ℝ) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :
    eLpNorm (f ⋆[L, μ] g) r μ ≤ .ofReal c * eLpNorm f p μ * eLpNorm g q μ := by
…

Mentions: E, g, c

theorem ENNReal.eLpNorm_convolution_le_of_norm_le_mul Documented declaration: eLpNorm_convolution_le_of_norm_le_mul line 443 source
Source documentation
Young's convolution inequality: the L^r seminorm of a convolution (f ⋆[L, μ] g) is bounded by ‖L‖ₑ times the product of the L^p and L^q seminorms, where 1 / p + 1 / q = 1 / r + 1. Here ‖L‖ₑ is replaced with a bound for L restricted to the ranges of f and g; see eLpNorm_convolution_le_enorm_mul for a version using ‖L‖ₑ explicitly.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, NontriviallyNormedField, NormedSpace, Real, ContinuousLinearMap, RingHom.id, AddGroup, TopologicalSpace, IsTopologicalAddGroup, BorelSpace, MeasureTheory.Measure.IsAddHaarMeasure, LocallyCompactSpace, SecondCountableTopology, OpensMeasurableSpace, MeasureTheory.Measure.IsAddRightInvariant, ENNReal, LE.le, OfNat.ofNat and 9 more
Proof uses: AEMeasurable.enorm, AEMeasurable.comp_quasiMeasurePreserving, HSub.hSub, ENorm.enorm, MeasureTheory.quasiMeasurePreserving_sub_left, MeasureTheory.eLpNorm_comp_measurePreserving', MeasureTheory.Measure.measurePreserving_sub_left, AEMeasurable.pow_const, Prod, MeasureTheory.Measure.prod, Function.comp, Prod.fst, Prod.snd, MeasureTheory.quasiMeasurePreserving_sub, ENNReal.toReal
171 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_convolution_le_of_norm_le_mul [MeasurableSpace E] [OpensMeasurableSpace E]
    [MeasurableSpace E'] [OpensMeasurableSpace E']
    [μ.IsAddRightInvariant] {p q r : ℝ≥0∞}
    (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
    {f : G → E} {g : G → E'} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
    (c : ℝ) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :
    eLpNorm (f ⋆[L, μ] g) r μ ≤ .ofReal c * eLpNorm f p μ * eLpNorm g q μ := by
…
```
Mentions: E, g, c
theorem ENNReal.eLpNorm_convolution_le_of_norm_le_mul' Documented declaration: eLpNorm_convolution_le_of_norm_le_mul' line 459 source
Source documentation
Young's convolution inequality: the L^r seminorm of a convolution (f ⋆[L, μ] g) is bounded by ‖L‖ₑ times the product of the L^p and L^q seminorms, where 1 / p + 1 / q = 1 / r + 1. Here ‖L‖ₑ is replaced with a bound for L restricted to the ranges of f and g; see eLpNorm_convolution_le_enorm_mul for a version using ‖L‖ₑ explicitly.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, NontriviallyNormedField, NormedSpace, Real, ContinuousLinearMap, RingHom.id, AddGroup, TopologicalSpace, IsTopologicalAddGroup, BorelSpace, MeasureTheory.Measure.IsAddHaarMeasure, LocallyCompactSpace, SecondCountableTopology, MeasureTheory.Measure.IsAddRightInvariant, ENNReal, LE.le, OfNat.ofNat, Eq and 8 more
Proof uses: MeasureTheory.AEStronglyMeasurable.enorm, AEMeasurable.comp_quasiMeasurePreserving, HSub.hSub, ENorm.enorm, MeasureTheory.quasiMeasurePreserving_sub_left, MeasureTheory.eLpNorm_comp_measurePreserving, MeasureTheory.Measure.measurePreserving_sub_left, AEMeasurable.pow_const, Prod, MeasureTheory.Measure.prod, Function.comp, Prod.fst, Prod.snd, MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving, MeasureTheory.quasiMeasurePreserving_sub, ENNReal.toReal
171 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_convolution_le_of_norm_le_mul'
    [μ.IsAddRightInvariant] {p q r : ℝ≥0∞}
    (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
    {f : G → E} {g : G → E'} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ)
    (c : ℝ) (hL : ∀ (x y : G), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :
    eLpNorm (f ⋆[L, μ] g) r μ ≤ .ofReal c * eLpNorm f p μ * eLpNorm g q μ := by
…
```
Mentions: E, g, c
theorem ENNReal.eLpNorm_convolution_le_enorm_mul Documented declaration: eLpNorm_convolution_le_enorm_mul line 473 source
Source documentation
Young's convolution inequality: the L^r seminorm of a convolution (f ⋆[L, μ] g) is bounded by ‖L‖ₑ times the product of the L^p and L^q seminorms, where 1 / p + 1 / q = 1 / r + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, NontriviallyNormedField, NormedSpace, Real, ContinuousLinearMap, RingHom.id, AddGroup, TopologicalSpace, IsTopologicalAddGroup, BorelSpace, MeasureTheory.Measure.IsAddHaarMeasure, LocallyCompactSpace, SecondCountableTopology, OpensMeasurableSpace, MeasureTheory.Measure.IsAddRightInvariant, ENNReal, LE.le, OfNat.ofNat and 8 more
Proof uses: Eq.mpr, Norm.norm, id, congrArg, Eq.symm, enorm_norm, ENNReal.ofReal, Real.enorm_of_nonneg, norm_nonneg, ENNReal.eLpNorm_convolution_le_of_norm_le_mul, LE.le.trans, ContinuousLinearMap.le_opNorm, mul_le_mul_of_nonneg_right
164 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_convolution_le_enorm_mul [MeasurableSpace E] [OpensMeasurableSpace E]
    [MeasurableSpace E'] [OpensMeasurableSpace E']
    [μ.IsAddRightInvariant] {p q r : ℝ≥0∞}
    (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
    {f : G → E} {g : G → E'} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    eLpNorm (f ⋆[L, μ] g) r μ ≤ ‖L‖ₑ * eLpNorm f p μ * eLpNorm g q μ := by
…
```
Mentions: E, g
theorem ENNReal.eLpNorm_convolution_le_enorm_mul' Documented declaration: eLpNorm_convolution_le_enorm_mul' line 486 source
Source documentation
Young's convolution inequality: the L^r seminorm of a convolution (f ⋆[L, μ] g) is bounded by ‖L‖ₑ times the product of the L^p and L^q seminorms, where 1 / p + 1 / q = 1 / r + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, NontriviallyNormedField, NormedSpace, Real, ContinuousLinearMap, RingHom.id, AddGroup, TopologicalSpace, IsTopologicalAddGroup, BorelSpace, MeasureTheory.Measure.IsAddHaarMeasure, LocallyCompactSpace, SecondCountableTopology, MeasureTheory.Measure.IsAddRightInvariant, ENNReal, LE.le, OfNat.ofNat, Eq and 7 more
Proof uses: Eq.mpr, Norm.norm, id, congrArg, Eq.symm, enorm_norm, ENNReal.ofReal, Real.enorm_of_nonneg, norm_nonneg, ENNReal.eLpNorm_convolution_le_of_norm_le_mul', LE.le.trans, ContinuousLinearMap.le_opNorm, mul_le_mul_of_nonneg_right
164 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_convolution_le_enorm_mul' [μ.IsAddRightInvariant] {p q r : ℝ≥0∞}
    (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
    {f : G → E} {g : G → E'} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) :
    eLpNorm (f ⋆[L, μ] g) r μ ≤ ‖L‖ₑ * eLpNorm f p μ * eLpNorm g q μ := by
…
```
Mentions: E, g
lemma ENNReal.eLpNorm_Ioc_convolution_le_of_norm_le_mul_aux line 495 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, NontriviallyNormedField, NormedSpace, Real, ContinuousLinearMap, RingHom.id, Fact, LT.lt, OfNat.ofNat, ENNReal, LE.le, Eq, HAdd.hAdd, Inv.inv, Function.Periodic, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, Norm.norm, HMul.hMul, MeasureTheory.eLpNorm and 5 more
Proof uses: Trans.trans, AddCircle, AddCircle.liftIoc, MeasureTheory.convolution, AddSubgroup.zmultiples, Eq.mpr, id, congrArg, Eq.symm, AddCircle.eLpNorm_liftIoc', MeasureTheory.AEStronglyMeasurable.sub, MeasureTheory.integral, MeasureTheory.AEStronglyMeasurable.integral_prod_right', Prod, Prod.snd, Prod.fst, ContinuousLinearMap.aestronglyMeasurable_comp₂, MeasureTheory.Measure.prod, MeasureTheory.AEStronglyMeasurable.comp_snd, MeasureTheory.AEStronglyMeasurable.restrict and 24 more
253 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
theorem ENNReal.eLpNorm_Ioc_convolution_le_of_norm_le_mul Documented declaration: eLpNorm_Ioc_convolution_le_of_norm_le_mul line 526 source
Source documentation
Young's convolution inequality on (a, a + T]: the L^r seminorm of the convolution of T-periodic functions over (a, a + T] is bounded by ‖L‖ₑ times the product of the L^p and L^q seminorms on that interval, where 1 / p + 1 / q = 1 / r + 1. Here ‖L‖ₑ is replaced with a bound for L restricted to the ranges of f and g; see eLpNorm_Ioc_convolution_le_enorm_mul for a version using ‖L‖ₑ explicitly.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, NontriviallyNormedField, NormedSpace, Real, ContinuousLinearMap, RingHom.id, Fact, LT.lt, OfNat.ofNat, ENNReal, LE.le, Eq, HAdd.hAdd, Inv.inv, Function.Periodic, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, Norm.norm, HMul.hMul, MeasureTheory.eLpNorm and 5 more
Proof uses: AddCircle, AddCircle.liftIoc, AddSubgroup.zmultiples, of_eq_true, Eq.trans, True, forall_congr, congrFun', congrArg, HasQuotient.Quotient, AddSubgroup, QuotientAddGroup.mk_add_of_mem, Membership.mem, eq_self, implies_true, ENNReal.eLpNorm_Ioc_convolution_le_of_norm_le_mul_aux, MeasureTheory.Measure.map, MeasureTheory.AEStronglyMeasurable.mono_ac, MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous, MeasureTheory.quasiMeasurePreserving_coe_addCircle and 79 more
220 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_Ioc_convolution_le_of_norm_le_mul (a : ℝ) {T : ℝ} [hT : Fact (0 < T)]
    {p q r : ℝ≥0∞} (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
    {f : ℝ → E} {g : ℝ → E'} (hgT : g.Periodic T)
    (hf : AEStronglyMeasurable f) (hg : AEStronglyMeasurable g)
    (c : ℝ) (hL : ∀ (x y : ℝ), ‖L (f x) (g y)‖ ≤ c * ‖f x‖ * ‖g y‖) :
    eLpNorm (fun x ↦ ∫ y in a..a+T, L (f y) (g (x - y))) r (volume.restrict (Ioc a (a + T))) ≤
    .ofReal c * eLpNorm f p (volume.restrict (Ioc a (a + T))) *
      eLpNorm g q (volume.restrict (Ioc a (a + T))) := by
…
```
Mentions: T, E, g, c
theorem ENNReal.eLpNorm_Ioc_convolution_le_enorm_mul Documented declaration: eLpNorm_Ioc_convolution_le_enorm_mul line 564 source
Source documentation
Young's convolution inequality on (a, a + T]: the L^r seminorm of the convolution of T-periodic functions over (a, a + T] is bounded by ‖L‖ₑ times the product of the L^p and L^q seminorms on that interval, where 1 / p + 1 / q = 1 / r + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NormedAddCommGroup, NontriviallyNormedField, NormedSpace, Real, ContinuousLinearMap, RingHom.id, Fact, LT.lt, OfNat.ofNat, ENNReal, LE.le, Eq, HAdd.hAdd, Inv.inv, Function.Periodic, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, MeasureTheory.eLpNorm, intervalIntegral, HSub.hSub and 4 more
Proof uses: Eq.mpr, Norm.norm, id, congrArg, Eq.symm, enorm_norm, ENNReal.ofReal, Real.enorm_of_nonneg, norm_nonneg, ENNReal.eLpNorm_Ioc_convolution_le_of_norm_le_mul, LE.le.trans, ContinuousLinearMap.le_opNorm, mul_le_mul_of_nonneg_right
174 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem eLpNorm_Ioc_convolution_le_enorm_mul (a : ℝ) {T : ℝ} [hT : Fact (0 < T)]
    {p q r : ℝ≥0∞} (hp : 1 ≤ p) (hq : 1 ≤ q) (hr : 1 ≤ r) (hpqr : p⁻¹ + q⁻¹ = r⁻¹ + 1)
    {f : ℝ → E} {g : ℝ → E'} (hgT : g.Periodic T)
    (hf : AEStronglyMeasurable f) (hg : AEStronglyMeasurable g) :
    eLpNorm (fun x ↦ ∫ y in a..a+T, L (f y) (g (x - y))) r (volume.restrict (Ioc a (a + T))) ≤
    ‖L‖ₑ * eLpNorm f p (volume.restrict (Ioc a (a + T)))
      * eLpNorm g q (volume.restrict (Ioc a (a + T))) := by
…
```
Mentions: T, E, g