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

52 declarations, 0 contain sorry, 0 declared as axioms

Imports (6)

Imported by 2 files

def doublingMeasure_real_two The volume measure on the real line is doubling line 23 source
Source documentation
The volume measure on the real line is doubling.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.DoublingMeasure, Real, OfNat.ofNat, NNReal, Nat
Proof uses: MeasureTheory.DoublingMeasure.mono, HPow.hPow, Module.finrank
37 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def doublingMeasure_real_two : DoublingMeasure ℝ 2 :=
…
```
instance doublingMeasure_real_16 line 26 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.DoublingMeasure, Real, NNReal, HPow.hPow, Nat, OfNat.ofNat
Proof uses: MeasureTheory.DoublingMeasure.mono, doublingMeasure_real_two
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma czOperator_comp_add line 30 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Eq, Function.comp, czOperator, HSub.hSub, HAdd.hAdd
Proof uses: funext, Eq.mpr, MeasureTheory.integral, MeasureTheory.MeasureSpace.volume, HMul.hMul, Set.indicator, Compl.compl, Set, Metric.ball, id, congr, congrArg, Eq.trans, MeasureTheory.Measure.restrict, MeasurableSpace, NormedAddCommGroup, NormedSpace, PseudoMetricSpace, MeasureTheory.Measure, OpensMeasurableSpace and 25 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def modulationOperator The modulation operator M_n g, defined in (11.3.1) line 41 source
Source documentation
The modulation operator M_n g, defined in (11.3.1)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Real, Complex
Proof uses: HMul.hMul, Complex.exp, Complex.I
5 instances, coercions and auxiliary constants left out.
```
def modulationOperator (n : ℤ) (g : ℝ → ℂ) (x : ℝ) : ℂ :=
…
```
Mentions: g
lemma Measurable.modulationOperator line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Real, Complex, Measurable, modulationOperator
Proof uses: Measurable.mul, Complex.exp, HMul.hMul, Complex.I, Measurable.cexp, measurable_const, Complex.measurable_ofReal
32 instances, coercions and auxiliary constants left out.
lemma AEMeasurable.modulationOperator line 48 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Real, Complex, AEMeasurable, MeasureTheory.MeasureSpace.volume, modulationOperator
Proof uses: AEMeasurable.mul, Complex.exp, HMul.hMul, Complex.I, Measurable.aemeasurable, Measurable.cexp, Measurable.mul, measurable_const, Complex.measurable_ofReal
35 instances, coercions and auxiliary constants left out.
def approxHilbertTransform The approximate Hilbert transform L_N g, defined in (11.3.2) line 54 source
Source documentation
The approximate Hilbert transform L_N g, defined in (11.3.2). defined slightly differently.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex
Proof uses: HMul.hMul, Inv.inv, Finset.sum, Finset.Ico, OfNat.ofNat, modulationOperator, Int, partialFourierSum, Neg.neg
12 instances, coercions and auxiliary constants left out.
```
def approxHilbertTransform (n : ℕ) (g : ℝ → ℂ) (x : ℝ) : ℂ :=
…
```
Mentions: g
def niceKernel The kernel k_r(x) defined in (11.3.11) line 61 source
Source documentation
The kernel k_r(x) defined in (11.3.11). When used, we may assume that r ∈ Ioo 0 1. Todo: find better name?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: ite, Eq, Complex, Complex.exp, HMul.hMul, Complex.I, OfNat.ofNat, Inv.inv, Min.min, HAdd.hAdd, HDiv.hDiv, MonoidWithZeroHom, Complex.normSq, HSub.hSub
21 instances, coercions and auxiliary constants left out.
```
def niceKernel (r : ℝ) (x : ℝ) : ℝ :=
…
```
lemma niceKernel_pos line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, niceKernel
Proof uses: id, Eq, Complex, Complex.exp, HMul.hMul, Complex.I, Decidable, ite, Inv.inv, Min.min, HAdd.hAdd, HDiv.hDiv, MonoidWithZeroHom, Complex.normSq, HSub.hSub, Not, Eq.mpr, congrArg, ite_eq_right, lt_min and 7 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma niceKernel_le_inv line 73 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, niceKernel, Inv.inv
Proof uses: id, Eq, Complex, Complex.exp, HMul.hMul, Complex.I, OfNat.ofNat, Decidable, ite, Min.min, HAdd.hAdd, HDiv.hDiv, MonoidWithZeroHom, Complex.normSq, HSub.hSub, Not, Eq.mpr, congrFun', congrArg, ite_eq_right and 4 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma one_le_niceKernel line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, LE.le, niceKernel
Proof uses: Inv.inv, le_inv_of_le_inv₀, Eq.mpr, id, Eq, congrArg, inv_one, LT.lt.le, Complex, Complex.exp, HMul.hMul, Complex.I, Decidable, ite, Min.min, HAdd.hAdd, HDiv.hDiv, MonoidWithZeroHom, Complex.normSq, HSub.hSub and 7 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma niceKernel_neg line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Eq, niceKernel, Neg.neg
Proof uses: Eq.mpr, ite, Complex, Complex.exp, HMul.hMul, Complex.I, OfNat.ofNat, Inv.inv, Min.min, HAdd.hAdd, HDiv.hDiv, MonoidWithZeroHom, Complex.normSq, HSub.hSub, id, congrFun', congrArg, ite_congr, Eq.trans, Complex.ofReal_neg and 21 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma niceKernel_periodic line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Function.Periodic, niceKernel, HMul.hMul, OfNat.ofNat, Nat, Real.pi
Proof uses: of_eq_true, Eq, HAdd.hAdd, ite, Complex, Complex.exp, Complex.I, Inv.inv, Min.min, HDiv.hDiv, MonoidWithZeroHom, Complex.normSq, HSub.hSub, Eq.trans, True, forall_congr, congrFun', congrArg, ite_congr, Complex.ofReal_add and 10 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma measurable_niceKernel line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Measurable, niceKernel
Proof uses: Measurable.piecewise, Eq, Complex, Complex.exp, HMul.hMul, Complex.I, OfNat.ofNat, Inv.inv, Min.min, HAdd.hAdd, HDiv.hDiv, MonoidWithZeroHom, Complex.normSq, HSub.hSub, Classical.propDecidable, Membership.mem, Set, IsClosed.measurableSet, Set.ofPred, isClosed_eq and 16 more
89 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma niceKernel_intervalIntegrable line 101 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, GT.gt, OfNat.ofNat, IntervalIntegrable, niceKernel, MeasureTheory.MeasureSpace.volume
Proof uses: IntervalIntegrable.mono_fun, Inv.inv, intervalIntegrable_const, Measurable.aestronglyMeasurable, MeasureTheory.Measure.restrict, Set.uIoc, measurable_niceKernel, Filter.Eventually.of_forall, LE.le, Norm.norm, MeasureTheory.ae, MeasureTheory.Measure, id, Eq.mpr, abs, Eq, congrFun', congrArg, abs_of_pos, niceKernel_pos and 21 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma niceKernel_eq_inv line 109 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, And, LT.lt, OfNat.ofNat, Real.pi, LE.le, Eq, niceKernel, Inv.inv
Proof uses: Eq.mpr, ite, Complex, Complex.exp, HMul.hMul, Complex.I, Min.min, HAdd.hAdd, HDiv.hDiv, MonoidWithZeroHom, Complex.normSq, HSub.hSub, id, congrArg, niceKernel.eq_1, Not, propext, ite_eq_iff', HPow.hPow, Nat and 130 more
151 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma niceKernel_eq_inv' line 126 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, And, LT.lt, OfNat.ofNat, Real.pi, LE.le, abs, Eq, niceKernel, Inv.inv
Proof uses: Or, le_total, niceKernel_eq_inv, And.intro, LE.le.trans, Norm.norm, Real.le_norm_self, Eq.mpr, Neg.neg, id, congrArg, Eq.symm, niceKernel_neg, of_eq_true, Eq.trans, True, congr, eq_true, Eq.mp, congrFun' and 3 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma niceKernel_upperBound_aux line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, And, LE.le, Real.pi, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Nat, Norm.norm, Complex, HSub.hSub, Complex.exp, HMul.hMul, Complex.I
Proof uses: Trans.trans, Eq, id, add_le_add, le_refl, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero and 95 more
140 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma niceKernel_upperBound line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, And, LE.le, Real.pi, niceKernel, HAdd.hAdd, HDiv.hDiv, HMul.hMul, Nat, HPow.hPow
Proof uses: Ne, Complex, Complex.exp, Complex.I, Eq.mpr, Not, Eq, id, congrArg, propext, exp_I_mul_eq_one_iff_of_lt_of_lt, lt_of_not_ge, Neg.neg, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast and 71 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma niceKernel_lowerBound line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, And, LE.le, Real.pi, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Nat, Norm.norm, Complex, HSub.hSub, Complex.exp, HMul.hMul, Complex.I, niceKernel
Proof uses: Ne, Eq.mpr, Not, Eq, id, congrArg, propext, exp_I_mul_eq_one_iff_of_lt_of_lt, lt_of_not_ge, Neg.neg, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne and 128 more
173 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma niceKernel_lowerBound' line 167 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, And, LE.le, abs, Real.pi, HAdd.hAdd, HDiv.hDiv, HPow.hPow, Nat, Norm.norm, Complex, HSub.hSub, Complex.exp, HMul.hMul, Complex.I, niceKernel
Proof uses: Or, le_total, niceKernel_lowerBound, Eq.mp, congr, congrArg, abs_of_nonneg, congrFun', Eq.mpr, Neg.neg, id, Eq, Eq.symm, niceKernel_neg, le_trans, le_of_eq, of_eq_true, Eq.trans, True, Complex.ofReal_neg and 4 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma mean_zero_oscillation Lemma 11.1.8 line 178 source
Source documentation
Lemma 11.1.8

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Ne, OfNat.ofNat, Eq, Complex, intervalIntegral, Real, Complex.exp, HMul.hMul, Complex.I, Nat, Real.pi, MeasureTheory.MeasureSpace.volume
Proof uses: Eq.mpr, HDiv.hDiv, HSub.hSub, id, congrArg, integral_exp_mul_complex, of_eq_true, Not, Eq.trans, False, True, Or, congr, eq_false, or_self, not_false_eq_true, congrFun', mul_comm, Complex.ofReal_mul, mul_right_comm and 6 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma mean_zero_oscillation {n : ℤ} (hn : n ≠ 0) :
    ∫ x in (0)..2 * π, exp (I * n * x) = 0 := by
…
```
theorem AddCircle.haarAddCircle_eq_smul_volume line 184 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Fact, LT.lt, OfNat.ofNat, Eq, MeasureTheory.Measure, AddCircle, AddSubgroup.zmultiples, AddCircle.haarAddCircle, HSMul.hSMul, ENNReal, Inv.inv, ENNReal.ofReal, MeasureTheory.MeasureSpace.volume
Proof uses: Eq.mpr, id, congrArg, AddCircle.volume_eq_smul_haarAddCircle, Eq.symm, smul_assoc, HMul.hMul, smul_eq_mul, ENNReal.inv_mul_cancel, of_eq_true, Not, Eq.trans, True, LE.le, eq_true, Fact.out, ENNReal.ofReal_ne_top, one_smul, Eq.refl
60 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma spectral_projection_bound Lemma 11.1.10 line 198 source
Source documentation
Lemma 11.1.10.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Nat, AEMeasurable, MeasureTheory.MeasureSpace.volume, LE.le, ENNReal, MeasureTheory.eLpNorm, Set.indicator, Set.Ioc, OfNat.ofNat, HMul.hMul, Real.pi, partialFourierSum
Proof uses: dite, Eq, Top.top, Eq.mpr, id, congrArg, OrderTop.le_top, Not, MeasureTheory.MemLp, AddCircle, AddSubgroup.zmultiples, AddCircle.liftIoc, instFactLtRealOfNatHMulPi, AddCircle.haarAddCircle, And.intro, MeasureTheory.AEStronglyMeasurable, LT.lt, HSMul.hSMul, MeasureTheory.Measure, Inv.inv and 81 more
184 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma spectral_projection_bound {f : ℝ → ℂ} {n : ℕ} (hmf : AEMeasurable f) :
    eLpNorm ((Ioc 0 (2 * π)).indicator (partialFourierSum n f)) 2 ≤
    eLpNorm ((Ioc 0 (2 * π)).indicator f) 2 := by
…
```
Mentions: partialFourierSum
lemma norm_modulationOperator line 237 source
lemma indicator_modulationOperator line 242 source
lemma eLpNorm_modulationOperator line 246 source
lemma eLpNorm_indicator_modulationOperator line 250 source
lemma modulated_averaged_projection Lemma 11.3.1 line 256 source
Source documentation
Lemma 11.3.1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Nat, AEMeasurable, MeasureTheory.MeasureSpace.volume, LE.le, ENNReal, MeasureTheory.eLpNorm, Set.indicator, Set.Ioc, OfNat.ofNat, HMul.hMul, Real.pi, approxHilbertTransform
Proof uses: id, dite, Inv.inv, Finset.sum, Finset.Ico, modulationOperator, Int, partialFourierSum, Neg.neg, Eq, of_eq_true, Eq.trans, True, congrFun', congrArg, MeasureTheory.Measure, autoParam, funext, congr, CharP.cast_eq_zero and 56 more
223 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma modulated_averaged_projection {g : ℝ → ℂ} {n : ℕ} (hmg : AEMeasurable g) :
    eLpNorm ((Ioc 0 (2 * π)).indicator (approxHilbertTransform n g)) 2 ≤
    eLpNorm ((Ioc 0 (2 * π)).indicator g) 2 := by
…
```
Mentions: g, approxHilbertTransform
lemma modulated_averaged_projection' line 276 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Nat, AEMeasurable, MeasureTheory.MeasureSpace.volume, LE.le, ENNReal, MeasureTheory.eLpNorm, approxHilbertTransform, OfNat.ofNat, MeasureTheory.Measure.restrict, Set.Ioc, HMul.hMul, Real.pi
Proof uses: Eq.mpr, Set.indicator, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict, measurableSet_Ioc, modulated_averaged_projection
87 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma young_convolution Lemma 11.3.3 line 291 source
Source documentation
Lemma 11.3.3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, AEMeasurable, MeasureTheory.MeasureSpace.volume, Function.Periodic, HMul.hMul, OfNat.ofNat, Nat, Real.pi, LE.le, ENNReal, MeasureTheory.eLpNorm, intervalIntegral, HSub.hSub, MeasureTheory.Measure.restrict, Set.Ioc
Proof uses: one_le_two, Eq.mpr, id, Eq, Eq.mp, ContinuousLinearMap, RingHom.id, ContinuousLinearMap.mul, HAdd.hAdd, ENNReal.ofReal, congr, congrArg, MeasureTheory.Measure, congrFun', autoParam, funext, zero_add, Set, Eq.trans, ENNReal.ofReal_one and 15 more
177 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma young_convolution {f g : ℝ → ℝ} (hmf : AEMeasurable f)
    (hmg : AEMeasurable g) (periodic_g : g.Periodic (2 * π)) :
    eLpNorm (fun x ↦ ∫ y in (0)..2 * π, f y * g (x - y)) 2 (volume.restrict (Ioc 0 (2 * π))) ≤
      eLpNorm f 2 (volume.restrict (Ioc 0 (2 * π)))
      * eLpNorm g 1 (volume.restrict (Ioc 0 (2 * π))) := by
…
```
Mentions: g
lemma integrable_bump_convolution Lemma 11.3.4 line 305 source
Source documentation
Lemma 11.3.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, MeasureTheory.MemLp, Top.top, ENNReal, MeasureTheory.MeasureSpace.volume, Function.Periodic, HMul.hMul, OfNat.ofNat, Nat, Real.pi, Membership.mem, Set, Set.Ioo, LE.le, abs, niceKernel, MeasureTheory.eLpNorm, intervalIntegral, HSub.hSub, MeasureTheory.Measure.restrict and 1 more
Proof uses: LT.lt, IntervalIntegrable, niceKernel_intervalIntegrable, MeasureTheory.Integrable, MeasureTheory.IntegrableOn.integrable, Eq.mpr, MeasureTheory.IntegrableOn, id, Eq, congrArg, Eq.symm, propext, intervalIntegrable_iff_integrableOn_Ioc_of_le, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow and 228 more
329 instances, coercions and auxiliary constants left out.

Tactic trace: 70 steps
Open to load the checked before-and-after goal states.
```
lemma integrable_bump_convolution {f g : ℝ → ℝ}
    (hf : MemLp f ∞ volume) (hg : MemLp g ∞ volume) (periodic_g : g.Periodic (2 * π))
    {r : ℝ} (hr : r ∈ Ioo 0 π) (hle : ∀ x, |g x| ≤ niceKernel r x) :
    eLpNorm (fun x ↦ ∫ y in (0)..2 * π, f y * g (x - y)) 2 (volume.restrict (Ioc 0 (2 * π))) ≤
    17 * eLpNorm f 2 (volume.restrict (Ioc 0 (2 * π))) := by
…
```
Mentions: g, niceKernel
def dirichletApprox The function L', defined in the Proof of Lemma 11.3.5 line 371 source
Source documentation
The function L', defined in the Proof of Lemma 11.3.5.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex
Proof uses: HMul.hMul, Inv.inv, Finset.sum, Finset.Ico, OfNat.ofNat, dirichletKernel, Complex.exp, Complex.I
11 instances, coercions and auxiliary constants left out.
```
def dirichletApprox (n : ℕ) (x : ℝ) : ℂ :=
…
```
lemma continuous_dirichletApprox Lemma 11.3.5, part 1 line 375 source
Source documentation
Lemma 11.3.5, part 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Continuous, Real, Complex, dirichletApprox
Proof uses: id, Continuous.const_mul, Finset.sum, Finset.Ico, HMul.hMul, OfNat.ofNat, dirichletKernel, Complex.exp, Complex.I, continuous_finsetSum, Membership.mem, Finset, Continuous.comp', Prod, Prod.mk, Prod.fst, Prod.snd, continuous_mul, Continuous.prodMk, continuous_dirichletKernel and 3 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
@[fun_prop] lemma continuous_dirichletApprox {n : ℕ} : Continuous (dirichletApprox n) := by
…
```
Mentions: dirichletApprox
lemma norm_dirichletApprox_le line 380 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, LE.le, Norm.norm, Complex, dirichletApprox, HMul.hMul, OfNat.ofNat
Proof uses: Trans.trans, Inv.inv, Finset.sum, Finset.Ico, dirichletKernel, Complex.exp, Complex.I, Eq, rfl, Eq.mpr, id, congrFun', congrArg, norm_mul, mul_le_mul_of_nonneg_left, norm_sum_le, norm_nonneg, congr, Eq.trans, norm_inv and 44 more
140 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma periodic_dirichletApprox Lemma 11.3.5, part 2 line 411 source
Source documentation
Lemma 11.3.5, part 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Function.Periodic, Real, Complex, dirichletApprox, HMul.hMul, OfNat.ofNat, Real.pi
Proof uses: Eq.mpr, Eq, HAdd.hAdd, Or, Finset.sum, Finset.Ico, dirichletKernel, Complex.exp, Complex.I, id, Eq.trans, Inv.inv, congrFun', congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Complex.ofReal_add, Complex.ofReal_mul and 37 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma periodic_dirichletApprox (n : ℕ) : (dirichletApprox n).Periodic (2 * π) := by
…
```
Mentions: dirichletApprox
lemma approxHilbertTransform_eq_dirichletApprox Lemma 11.3.5, part 3 line 425 source
Source documentation
Lemma 11.3.5, part 3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, MeasureTheory.MemLp, Top.top, ENNReal, MeasureTheory.MeasureSpace.volume, Nat, Eq, approxHilbertTransform, HMul.hMul, Inv.inv, OfNat.ofNat, Real.pi, intervalIntegral, dirichletApprox, HSub.hSub
Proof uses: Eq.mpr, Finset.sum, Finset.Ico, modulationOperator, Int, partialFourierSum, Neg.neg, dirichletKernel, Complex.exp, Complex.I, id, congr, congrArg, Finset.mul_sum, Eq.trans, mul_inv_rev, Complex.ofReal_mul, Complex.ofReal_inv, congrFun', MeasureTheory.Measure and 84 more
211 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma approxHilbertTransform_eq_dirichletApprox {f : ℝ → ℂ} (hf : MemLp f ∞ volume)
    {n : ℕ} {x : ℝ} :
    approxHilbertTransform n f x =
      (2 * π)⁻¹ * ∫ y in (0)..2 * π, f y * dirichletApprox n (x - y) := by
…
```
Mentions: approxHilbertTransform, dirichletApprox
lemma eLpNorm_convolution_dirichletApprox The convolution with dirichletApprox is controlled on (0, 2π] in L^2 norm line 459 source
Source documentation
The convolution with dirichletApprox is controlled on (0, 2π] in L^2 norm. This follows from the fact that it coincides (up to a constant) with approxHilbertTransform, which is essentially an average of Fourier projections (which are all contractions in L^2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Nat, MeasureTheory.MemLp, Top.top, ENNReal, MeasureTheory.MeasureSpace.volume, LE.le, MeasureTheory.eLpNorm, intervalIntegral, HMul.hMul, dirichletApprox, HSub.hSub, OfNat.ofNat, Real.pi, MeasureTheory.Measure.restrict, Set.Ioc
Proof uses: Eq, HSMul.hSMul, approxHilbertTransform, funext, Eq.mpr, Inv.inv, id, congrArg, Eq.trans, congrFun', approxHilbertTransform_eq_dirichletApprox, Complex.ofReal_inv, Complex.ofReal_mul, mul_inv_cancel₀, of_eq_true, Not, False, True, Or, congr and 106 more
227 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma eLpNorm_convolution_dirichletApprox {g : ℝ → ℂ} {n : ℕ} (hg : MemLp g ∞ volume) :
    eLpNorm (fun x ↦ ∫ y in (0)..2 * π, g y * dirichletApprox n (x - y))
      2 (volume.restrict (Ioc 0 (2 * π))) ≤
    7 * eLpNorm g 2 (volume.restrict (Ioc 0 (2 * π))) := by
…
```
Mentions: g, dirichletApprox
def dirichletApproxAux The function L'', defined in the Proof of Lemma 11.3.5 line 496 source
Source documentation
The function L'', defined in the Proof of Lemma 11.3.5.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex
Proof uses: HMul.hMul, HDiv.hDiv, Inv.inv, Complex.exp, Complex.I, OfNat.ofNat, HSub.hSub, Neg.neg, Finset.sum, Finset.Ico
20 instances, coercions and auxiliary constants left out.
```
def dirichletApproxAux (n : ℕ) (x : ℝ) : ℂ :=
…
```
lemma dirichletApprox_eq_add_dirichletApproxAux line 499 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Ne, Complex, Complex.exp, HMul.hMul, Complex.I, OfNat.ofNat, Eq, dirichletApprox, HAdd.hAdd, Inv.inv, HSub.hSub, dirichletApproxAux
Proof uses: Finset, Finset.Ico, of_eq_true, Eq.trans, True, congr, congrArg, Nat.two_mul, congrFun', zero_add, eq_self, Eq.mpr, Finset.sum, dirichletKernel, id, Finset.sum_congr, Membership.mem, Eq.refl, dirichletKernel', dirichletKernel_eq and 85 more
151 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma norm_dirichletApproxAux_le_of_re_nonneg line 515 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Ne, Complex, Complex.exp, HMul.hMul, Complex.I, OfNat.ofNat, LE.le, Complex.re, Inv.inv, LT.lt, Norm.norm, dirichletApproxAux, HAdd.hAdd, HDiv.hDiv, HPow.hPow, HSub.hSub
Proof uses: Eq, Eq.mpr, id, congrArg, Eq.symm, Complex.exp_nat_mul, congr, Eq.trans, congrFun', mul_assoc, Complex.ofReal_mul, of_eq_true, True, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 114 more
223 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
lemma norm_dirichletApproxAux_le_of_re_nonpos line 562 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, LE.le, Complex.re, Complex.exp, HMul.hMul, Complex, Complex.I, OfNat.ofNat, LT.lt, Norm.norm, dirichletApproxAux, HAdd.hAdd, HDiv.hDiv, HPow.hPow, HSub.hSub
Proof uses: Trans.trans, Inv.inv, Finset.sum, Finset.range, Eq, rfl, Eq.mpr, id, congrArg, Eq.trans, Complex.ofReal_mul, congrFun', Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 64 more
171 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma norm_dirichletApproxAux_le line 585 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Ne, Complex, Complex.exp, HMul.hMul, Complex.I, OfNat.ofNat, LE.le, abs, Real.pi, Inv.inv, LT.lt, Norm.norm, dirichletApproxAux, niceKernel
Proof uses: HAdd.hAdd, HDiv.hDiv, HPow.hPow, HSub.hSub, Complex.re, Or, le_total, norm_dirichletApproxAux_le_of_re_nonpos, norm_dirichletApproxAux_le_of_re_nonneg, LE.le.trans, Eq.mpr, id, Eq, congrArg, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.isNat_mul, mul_assoc and 7 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma norm_sub_indicator_k line 598 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LE.le, abs, Real.pi, LT.lt, OfNat.ofNat, Norm.norm, Complex, HSub.hSub, Inv.inv, Complex.exp, HMul.hMul, Complex.I, Set.indicator, Set.ofPred, Membership.mem, Set, Set.Ico, k, Nat and 1 more
Proof uses: Or, lt_or_ge, Eq.mpr, id, Eq, congrArg, Set.indicator_of_mem, And.intro, Max.max, Eq.trans, LT.lt.le, congrFun', HDiv.hDiv, Complex.ofReal_sub, div_eq_inv_mul, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat.rawCast, Int.rawCast and 145 more
199 instances, coercions and auxiliary constants left out.

Tactic trace: 45 steps
Open to load the checked before-and-after goal states.
lemma dist_dirichletApprox_le Lemma 11.3.5, part 4 line 647 source
Source documentation
Lemma 11.3.5, part 4.
The kernel dirichletApprox approximates well the kernel of the Hilbert transform, on [-π, π], up to an error which is uniformly bounded in L^1 (as it is bounded by a constant multiple of niceKernel).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Nat, Eq, Nat.ceil, Inv.inv, Set.Icc, Neg.neg, Real.pi, LE.le, Dist.dist, Complex, dirichletApprox, Set.indicator, Set.ofPred, Set.Ico, abs and 3 more
Proof uses: LT.lt, And.left, HAdd.hAdd, Eq.mpr, id, congrArg, Nat.ceil_lt_add_one, LT.lt.le, Iff.mpr, one_le_inv₀, And.right, LE.le.trans, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, inferInstance, AddMonoidWithOne, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 134 more
192 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
```
lemma dist_dirichletApprox_le
    {r : ℝ} (hr : r ∈ Ioo 0 1) {n : ℕ} (hn : n = ⌈r⁻¹⌉₊) {x : ℝ} (hx : x ∈ Icc (-π) π) :
    dist (dirichletApprox n x) ({y : ℝ | |y| ∈ Ico r 1}.indicator k x) ≤ 12 * niceKernel r x := by
…
```
Mentions: dirichletApprox, k, niceKernel
lemma norm_czOperator_le_add As the kernel of the Hilbert transform is well approximated by dirichletApprox, up to an error controlled by 12 * niceKernel r, we may bound czOperator K in terms of these line 693 source
Source documentation
As the kernel of the Hilbert transform is well approximated by dirichletApprox, up to an error controlled by 12 * niceKernel r, we may bound czOperator K in terms of these. As the approximation only works in the interval [-π, π], this statement is only true for a point x in [2, 3] and a function supported in [1, 4], as this means all values of the approximation that will show up will be in [-2, 2] ⊆ [-π, π].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Nat, Eq, Nat.ceil, Inv.inv, MeasureTheory.MemLp, Top.top, ENNReal, MeasureTheory.MeasureSpace.volume, LE.le, Function.support, Set.Icc, Norm.norm, czOperator, K and 10 more
Proof uses: LT.lt, And.left, Real.pi_gt_three, Set.indicator, Set.ofPred, Set.Ico, abs, k, Eq.mpr, Compl.compl, Metric.ball, id, congr, congrArg, funext, mul_comm, congrFun', MeasureTheory.Measure, Eq.symm, MeasureTheory.integral_indicator and 172 more
313 instances, coercions and auxiliary constants left out.

Tactic trace: 73 steps
Open to load the checked before-and-after goal states.
```
lemma norm_czOperator_le_add
    {g : ℝ → ℂ} {r x : ℝ} (hr : r ∈ Ioo 0 1) {n : ℕ} (hn : n = ⌈r⁻¹⌉₊)
    (hg : MemLp g ∞ volume)
    (hx : 2 ≤ x) (h'x : x ≤ 3)
    (h'g : support g ⊆ Icc 1 4) :
    ‖czOperator K r g x‖ ≤ ‖∫ y in (0)..(2 * π), g y * dirichletApprox n (x - y)‖
      + 12 * ∫ y in Ioc 0 (2 * π), ‖g y‖ * niceKernel r (x - y) := by
…
```
Mentions: g, czOperator, K, dirichletApprox, niceKernel
lemma eLpNorm_czOperator_restrict_two_three_of_support_subset The operator czOperator K r is bounded from L^2 ([1, 4]) to L^2 ([2, 3]), uniformly in r line 769 source
Source documentation
The operator czOperator K r is bounded from L^2 ([1, 4]) to L^2 ([2, 3]), uniformly in r. This follows from the fact, proved in norm_czOperator_le_add, that it is bounded by the sum of two operators which are both bounded: one is the convolution with dirichletApprox, bounded as it is an average of Fourier projections, and the other one has a kernel uniformly bounded in L^1 and is therefore controlled by Young inequality.
In this version, we assume that the function is supported in [1, 4], but we will drop this assumption just after this lemma, in eLpNorm_czOperator_restrict_two_three.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Membership.mem, Set, Set.Ioo, OfNat.ofNat, MeasureTheory.MemLp, Top.top, ENNReal, MeasureTheory.MeasureSpace.volume, LE.le, Function.support, Set.Icc, Nat, MeasureTheory.eLpNorm, czOperator, K, MeasureTheory.Measure.restrict, Set.Ioc, HMul.hMul and 1 more
Proof uses: Real.pi, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 147 more
303 instances, coercions and auxiliary constants left out.

Tactic trace: 65 steps
Open to load the checked before-and-after goal states.
```
lemma eLpNorm_czOperator_restrict_two_three_of_support_subset {g : ℝ → ℂ} {r : ℝ}
    (hr : r ∈ Ioo 0 1) (hg : MemLp g ∞ volume) (h'g : support g ⊆ Icc 1 4) :
    eLpNorm (czOperator K r g) 2 (volume.restrict (Ioc 2 3)) ≤
      2 ^ 8 * eLpNorm g 2 (volume.restrict (Ioc 1 4)) := by
…
```
Mentions: g, czOperator, K
lemma eLpNorm_czOperator_restrict_two_three The operator czOperator K r is bounded from L^2 [1, 4] to L^2 [2, 3], uniformly in r line 847 source
Source documentation
The operator czOperator K r is bounded from L^2 [1, 4] to L^2 [2, 3], uniformly in r. This follows from the fact, proved in norm_czOperator_le_add, that it is bounded by the sum of two operators which are both bounded: one is the convolution with dirichletApprox, bounded as it is an average of Fourier projections, and the other one has a kernel uniformly bounded in L^1 and is therefore controlled by Young inequality.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Membership.mem, Set, Set.Ioo, OfNat.ofNat, MeasureTheory.MemLp, Top.top, ENNReal, MeasureTheory.MeasureSpace.volume, LE.le, MeasureTheory.eLpNorm, czOperator, K, Nat, MeasureTheory.Measure.restrict, Set.Ioc, HMul.hMul, HPow.hPow
Proof uses: Set.indicator, Set.Icc, Eq, MeasureTheory.eLpNorm_congr_ae, Filter.mp_mem, MeasureTheory.ae, MeasureTheory.Measure, Set.ofPred, MeasureTheory.self_mem_ae_restrict, measurableSet_Ioc, Filter.univ_mem', id, Eq.mpr, congrArg, Set.indicator_of_mem, And.intro, LT.lt.le, And.left, LT.lt, And.right and 80 more
157 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma eLpNorm_czOperator_restrict_two_three {g : ℝ → ℂ} {r : ℝ} (hr : r ∈ Ioo 0 1)
    (hg : MemLp g ∞ volume) :
    eLpNorm (czOperator K r g) 2 (volume.restrict (Ioc 2 3)) ≤
      2 ^ 8 * eLpNorm g 2 (volume.restrict (Ioc 1 4)) := by
…
```
Mentions: g, czOperator, K
lemma eLpNorm_czOperator_restrict The operator czOperator K r is bounded from L^2 [a - 1, a + 2] to L^2 [a, a + 1], uniformly in r and a line 879 source
Source documentation
The operator czOperator K r is bounded from L^2 [a - 1, a + 2] to L^2 [a, a + 1], uniformly in r and a. This follows from the same fact from L^2 [1, 4] to L^2 [2, 3] proved using Fourier series, and translation invariance.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Membership.mem, Set, Set.Ioo, OfNat.ofNat, MeasureTheory.MemLp, Top.top, ENNReal, MeasureTheory.MeasureSpace.volume, LE.le, MeasureTheory.eLpNorm, czOperator, K, Nat, MeasureTheory.Measure.restrict, Set.Ioc, HAdd.hAdd, HMul.hMul, HPow.hPow and 1 more
Proof uses: Function.comp, Eq, Eq.mpr, id, congrArg, MeasureTheory.eLpNorm_comp_measurePreserving, MeasureTheory.MemLp.aestronglyMeasurable, MeasureTheory.MemLp.restrict, MeasureTheory.MeasurePreserving, MeasureTheory.measurePreserving_add_right, Set.preimage, eq_of_heq, MeasurableSpace, autoParam, MeasureTheory.Measure, HEq, Eq.refl, HEq.refl, Eq.symm, heq_of_eq and 32 more
152 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma eLpNorm_czOperator_restrict {g : ℝ → ℂ} {r a : ℝ} (hr : r ∈ Ioo 0 1)
    (hg : MemLp g ∞ volume) :
    eLpNorm (czOperator K r g) 2 (volume.restrict (Ioc a (a + 1))) ≤
      2 ^ 8 * eLpNorm g 2 (volume.restrict (Ioc (a - 1) (a + 2))) := by
…
```
Mentions: g, czOperator, K
lemma eLpNorm_czOperator_sq line 907 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, Membership.mem, Set, Set.Ioo, OfNat.ofNat, MeasureTheory.MemLp, Top.top, ENNReal, MeasureTheory.MeasureSpace.volume, LE.le, HPow.hPow, Nat, MeasureTheory.eLpNorm, czOperator, K, HMul.hMul
Proof uses: Eq, MeasureTheory.Measure, MeasureTheory.Measure.sum, Int, MeasureTheory.Measure.restrict, Set.Ioc, HAdd.hAdd, Eq.mpr, Set.iUnion, id, congrArg, Eq.symm, MeasureTheory.Measure.restrict_iUnion, Set.pairwise_disjoint_Ioc_intCast, measurableSet_Ioc, Set.univ, iUnion_Ioc_intCast, MeasureTheory.Measure.restrict_univ, Eq.refl, Trans.trans and 125 more
203 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma eLpNorm_czOperator line 955 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Complex, LT.lt, OfNat.ofNat, MeasureTheory.MemLp, Top.top, ENNReal, MeasureTheory.MeasureSpace.volume, LE.le, MeasureTheory.eLpNorm, czOperator, K, Nat, HMul.hMul, HPow.hPow
Proof uses: Or, le_or_gt, Eq, funext, id, MeasureTheory.setIntegral_eq_zero_of_forall_eq_zero, k, HSub.hSub, Compl.compl, Set, Metric.ball, Membership.mem, k_of_one_le_abs, le_of_not_gt, abs, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, congrArg, Mathlib.Tactic.Ring.of_eq and 91 more
173 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma Hilbert_strong_2_2 Lemma 11.1.6 line 983 source
Source comment
Lemma 11.1.6. This verifies the assumption on the operators T_r in two-sided metric space Carleson. Note: we might be able to simplify the proof in the blueprint by using real interpolation `MeasureTheory.exists_hasStrongType_real_interpolation`.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, LT.lt, OfNat.ofNat, MeasureTheory.HasBoundedStrongType, Complex, czOperator, K, ENNReal, Nat, MeasureTheory.MeasureSpace.volume, C_Ts
Proof uses: BoundedFiniteSupport, And.intro, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.eLpNorm, HMul.hMul, czOperator_aestronglyMeasurable', Hilbert_kernel_measurable, BoundedFiniteSupport.aestronglyMeasurable, LE.le.trans, HPow.hPow, eLpNorm_czOperator, BoundedFiniteSupport.memLp_top, mul_le_mul', id, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo and 9 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma Hilbert_strong_2_2 ⦃r : ℝ⦄ (hr : 0 < r) :
    HasBoundedStrongType (czOperator K r) 2 2 volume volume (C_Ts 4) := by
…
```
Mentions: czOperator, K, C_Ts