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

40 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Carleson.FinitaryCarleson

Imported by 2 files

def T_S The operator T_{s₁, s₂} introduced in Lemma 3.0.3 line 16 source
Source documentation
The operator T_{s₁, s₂} introduced in Lemma 3.0.3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, Complex, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real, Int
Proof uses: Finset.sum, Finset.Icc, MeasureTheory.integral, MeasureTheory.MeasureSpace.volume, HMul.hMul, Ks, Complex.exp, Complex.I
52 instances, coercions and auxiliary constants left out.
```
def T_S (Q : SimpleFunc X (Θ X)) (s₁ s₂ : ℤ) (f : X → ℂ) (x : X) : ℂ :=
…
```
lemma measurable_T_inner_integral line 19 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, Complex, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real, Int, Measurable, MeasureTheory.integral, MeasureTheory.MeasureSpace.volume, HMul.hMul, Ks, Complex.exp, Complex.I
Proof uses: Eq.mpr, MeasureTheory.StronglyMeasurable, id, Eq, congrArg, Eq.symm, propext, stronglyMeasurable_iff_measurable, MeasureTheory.StronglyMeasurable.integral_prod_right, Prod, Function.uncurry, Measurable.mul, Prod.fst, Prod.snd, Function.comp, measurable_Ks, Measurable.comp, measurable_snd, Measurable.cexp, Measurable.const_mul and 2 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma measurable_T_S line 27 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, Complex, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real, Int, Measurable, T_S
Proof uses: Finset.measurable_sum, MeasureTheory.integral, MeasureTheory.MeasureSpace.volume, HMul.hMul, Ks, Complex.exp, Complex.I, Finset.Icc, Membership.mem, Finset, measurable_T_inner_integral
81 instances, coercions and auxiliary constants left out.
def T_lin The operator T_{2, σ₁, σ₂} introduced in Lemma 3.0.4 line 31 source
Source documentation
The operator T_{2, σ₁, σ₂} introduced in Lemma 3.0.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, Complex, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real, Int
Proof uses: T_S
34 instances, coercions and auxiliary constants left out.
```
def T_lin (Q : SimpleFunc X (Θ X)) (σ₁ σ₂ : X → ℤ) (f : X → ℂ) (x : X) : ℂ :=
…
```
lemma measurable_T_lin line 34 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, Complex, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real, Int, Measurable, Set.Finite, Set.range, T_lin
Proof uses: Membership.mem, Set, LE.le, Exists, Iff.mp, BddBelow, bddBelow_def, Set.Finite.bddBelow, BddAbove, bddAbove_def, Set.Finite.bddAbove, Eq, Finset.sum, Finset.Icc, Set.indicator, Set.ofPred, Set.Icc, MeasureTheory.integral, MeasureTheory.MeasureSpace.volume, HMul.hMul and 41 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
structure CP304 Convenience structure for the parameters that stay constant throughout the recursive calls to finitary Carleson in the proof of Lemma 3.0.4 line 64 source
Source documentation
Convenience structure for the parameters that stay constant throughout the recursive calls to finitary Carleson in the proof of Lemma 3.0.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, Int
1 instances, coercions and auxiliary constants left out.
```
structure CP304 where
…
```
theorem finitary_carleson_step line 81 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, Int, IsCancellative, defaultA, defaultτ, CP304, Bornology.IsBounded, MeasurableSet, Exists, And, LE.le, ENNReal, HMul.hMul, OfNat.ofNat, MeasureTheory.Measure and 11 more
Proof uses: MeasureTheory.SimpleFunc, FunctionDistances.Θ, MeasureTheory.HasBoundedStrongType, linearizedNontangentialOperator, C_Ts, Membership.mem, Set.Ioc, NNReal.HolderConjugate, Measurable, Norm.norm, Set.indicator, Set.Finite, Set.range, ProofData, ProofData.mk, Finset.sum, Set.toFinset, Set.Icc, MeasureTheory.integral, Ks and 50 more
163 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
structure P304 All the parameters needed to apply the recursion of Lemma 3.0.4 line 98 source
Source documentation
All the parameters needed to apply the recursion of Lemma 3.0.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, Int
1 instances, coercions and auxiliary constants left out.
```
structure P304 where
…
```
def P304.succ Construct G_{n+1} given G_n line 107 source
Source documentation
Construct G_{n+1} given G_n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, Int, IsCancellative, defaultA, defaultτ, P304
Proof uses: P304.mk, P304.CP, Exists.choose, And, LE.le, P304.G, Bornology.IsBounded, MeasurableSet, ENNReal, HMul.hMul, OfNat.ofNat, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, SDiff.sdiff, ENorm.enorm, T_lin, CP304.Q, C2_0_1 and 3 more
48 instances, coercions and auxiliary constants left out.
```
def P304.succ (P : P304 q q' F f σ₁ σ₂) : P304 q q' F f σ₁ σ₂ where
…
```
Mentions: P304
def slice slice CP bG mG n contains G_n and its associated data line 116 source
Source documentation
slice CP bG mG n contains G_n and its associated data.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, Int, IsCancellative, defaultA, defaultτ, CP304, Bornology.IsBounded, MeasurableSet, P304
Proof uses: Nat.iterate, P304.succ, P304.mk
24 instances, coercions and auxiliary constants left out.
```
def slice (n : ℕ) : P304 q q' F f σ₁ σ₂ := P304.succ^[n] ⟨CP, G, bG, mG⟩
…
```
Mentions: P304, P304.succ
lemma slice_CP line 121 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, Int, IsCancellative, defaultA, defaultτ, CP304, Bornology.IsBounded, MeasurableSet, Eq, P304.CP, slice
Proof uses: Nat.recAux, of_eq_true, eq_self, Eq.mpr, HAdd.hAdd, OfNat.ofNat, Nat.iterate, P304, P304.succ, P304.mk, id, congrArg, slice.eq_1, Nat.succ, Function.iterate_succ_apply', Eq.mp
27 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma slice_G_subset line 126 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, Int, IsCancellative, defaultA, defaultτ, CP304, Bornology.IsBounded, MeasurableSet, LE.le, P304.G, slice, HAdd.hAdd, OfNat.ofNat
Proof uses: Eq.mpr, Nat.iterate, P304, P304.succ, P304.mk, id, Eq, congrArg, slice.eq_1, Nat.succ, Function.iterate_succ_apply', rfl, And.left, Exists.choose, And, ENNReal, HMul.hMul, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, MeasureTheory.lintegral and 14 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma antitone_slice_G line 131 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, Int, IsCancellative, defaultA, defaultτ, CP304, Bornology.IsBounded, MeasurableSet, Antitone, P304.G, slice
Proof uses: antitone_nat_of_succ_le, slice_G_subset
37 instances, coercions and auxiliary constants left out.
lemma volume_slice line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, Int, IsCancellative, defaultA, defaultτ, CP304, Bornology.IsBounded, MeasurableSet, LE.le, ENNReal, HMul.hMul, OfNat.ofNat, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, P304.G and 2 more
Proof uses: Eq.mpr, Nat.iterate, P304, P304.succ, P304.mk, id, Eq, congrArg, slice.eq_1, Nat.succ, Function.iterate_succ_apply', rfl, And.left, Exists.choose, And, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, SDiff.sdiff, ENorm.enorm, T_lin and 11 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma volume_slice_le_inv_two_pow_mul line 139 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, Int, IsCancellative, defaultA, defaultτ, CP304, Bornology.IsBounded, MeasurableSet, LE.le, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, P304.G, slice, HMul.hMul and 3 more
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrArg, congrFun', pow_zero, one_mul, HAdd.hAdd, LE.le.trans, volume_slice, Eq.mp, Eq.symm, pow_succ', mul_assoc, propext, ENNReal.mul_le_iff_le_inv, two_ne_zero, ENNReal.ofNat_ne_top
82 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma exists_volume_slice_lt_eps The sets G_n become arbitrarily small line 147 source
Source documentation
The sets G_n become arbitrarily small.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, Int, IsCancellative, defaultA, defaultτ, CP304, Bornology.IsBounded, MeasurableSet, ENNReal, LT.lt, OfNat.ofNat, Exists, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, P304.G and 2 more
Proof uses: HMul.hMul, HPow.hPow, Inv.inv, Eq, Or, eq_zero_or_pos, Eq.mpr, id, Eq.trans, congrArg, funext, congrFun', MulZeroClass.mul_zero, Ne, Top.top, LT.lt.ne, Bornology.IsBounded.measure_lt_top, HDiv.hDiv, Eq.rec, Eq.refl and 19 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma exists_volume_slice_lt_eps {ε : ℝ≥0∞} (εpos : 0 < ε) :
    ∃ n, volume (slice CP bG mG (n + 1)).G < ε := by
…
```
Mentions: slice
lemma slice_integral_bound line 162 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, Int, IsCancellative, defaultA, defaultτ, CP304, Bornology.IsBounded, MeasurableSet, LE.le, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, SDiff.sdiff, P304.G and 12 more
Proof uses: P304, Eq.mpr, id, Eq, congrArg, rfl, Exists.choose, And, P304.CP, finitary_carleson_step, P304.bG, P304.mG, eq_of_heq, LE, HEq, Eq.refl, HEq.refl, Eq.symm, MeasurableSpace, SDiff and 17 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma slice_integral_bound_sum The slightly unusual way of writing the integrand is to facilitate applying the monotone convergence theorem line 172 source
Source documentation
The slightly unusual way of writing the integrand is to facilitate applying the monotone convergence theorem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, Int, IsCancellative, defaultA, defaultτ, CP304, Bornology.IsBounded, MeasurableSet, LE.le, ENNReal, MeasureTheory.lintegral, MeasureTheory.MeasureSpace.volume, Set.indicator, SDiff.sdiff, P304.G and 14 more
Proof uses: Eq.mpr, MeasureTheory.Measure.restrict, id, Eq, congrArg, MeasureTheory.lintegral_indicator, MeasurableSet.diff, P304.mG, Nat.recAux, zero_add, Singleton.singleton, Finset, Finset.range_one, Finset.sum_singleton, pow_zero, ENNReal.one_rpow, mul_one, eq_of_heq, LE, HEq and 35 more
160 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma slice_integral_bound_sum :
    ∫⁻ x, (G \ (slice CP bG mG (n + 1)).G).indicator (‖T_lin CP.Q σ₁ σ₂ f ·‖ₑ) x ≤
    C2_0_1 a q * (∑ i ∈ Finset.range (n + 1), (2⁻¹ ^ i) ^ (q' : ℝ)⁻¹) *
    volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ := by
…
```
Mentions: slice, T_lin, C2_0_1
lemma sum_le_four_div_q_sub_one line 192 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, Membership.mem, Set, Set.Ioc, OfNat.ofNat, Nat, NNReal.HolderConjugate, LE.le, ENNReal, Finset.sum, Finset.range, HPow.hPow, Real, Inv.inv, HDiv.hDiv, HSub.hSub
Proof uses: LT.lt, And.left, Eq, HAdd.hAdd, Iff.mp, And, NNReal.holderConjugate_iff, NNReal.HolderConjugate.symm, Trans.trans, HMul.hMul, ENNReal.ofReal, Neg.neg, tsum, SummationFilter.unconditional, Finset.sum_congr, Eq.refl, Finset, Eq.mpr, id, congr and 40 more
158 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
def C3_0_4 The constant used in linearized_truncation and S_truncation line 214 source
Source documentation
The constant used in linearized_truncation and S_truncation. Has value 2 ^ (442 * a ^ 3 + 2) in the blueprint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal
Proof uses: HDiv.hDiv, HPow.hPow, OfNat.ofNat, HAdd.hAdd, HMul.hMul, 𝕔, HSub.hSub
24 instances, coercions and auxiliary constants left out.
```
def C3_0_4 (a : ℕ) (q : ℝ≥0) : ℝ≥0 :=
…
```
lemma eq_C3_0_4 line 217 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal, Eq, HMul.hMul, C2_0_1, HDiv.hDiv, HPow.hPow, OfNat.ofNat, HSub.hSub, C3_0_4
Proof uses: Eq.mpr, C2_0_2, id, congrArg, C2_0_1.eq_1, HAdd.hAdd, 𝕔, C2_0_2.eq_1, congrFun', Eq.trans, div_mul_div_comm, HDiv, Eq.rec, Eq.refl
62 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma linearized_truncation Lemma 3.0.4 line 223 source
Source documentation
Lemma 3.0.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, MeasureTheory.SimpleFunc, defaultA, FunctionDistances.Θ, Real, Int, IsCancellative, defaultτ, Membership.mem, Set.Ioc, OfNat.ofNat, NNReal.HolderConjugate, Bornology.IsBounded, MeasurableSet, Measurable and 19 more
Proof uses: CP304, CP304.mk, Trans.trans, Eq, C2_0_1, HDiv.hDiv, HSub.hSub, iSup, SDiff.sdiff, P304.G, slice, HAdd.hAdd, CP304.Q, Set.iUnion, MeasureTheory.setLIntegral_congr, Eq.mpr, Filter.EventuallyEq, MeasureTheory.ae, Set.iInter, id and 56 more
257 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
```
lemma linearized_truncation
    [IsCancellative X (defaultτ a)] (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q')
    (bF : IsBounded F) (bG : IsBounded G) (mF : MeasurableSet F) (mG : MeasurableSet G)
    (mf : Measurable f) (nf : (‖f ·‖) ≤ F.indicator 1) (mσ₁ : Measurable σ₁) (mσ₂ : Measurable σ₂)
    (rσ₁ : (range σ₁).Finite) (rσ₂ : (range σ₂).Finite) (lσ : σ₁ ≤ σ₂)
    (BST_T_Q : ∀ θ : Θ X, HasBoundedStrongType (linearizedNontangentialOperator Q θ K · ·)
      2 2 volume volume (C_Ts a)) :
    ∫⁻ x in G, ‖T_lin Q σ₁ σ₂ f x‖ₑ ≤
    C3_0_4 a q * volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ := by
…
```
Mentions: IsCancellative, defaultτ, mf, linearizedNontangentialOperator, K, C_Ts, T_lin, C3_0_4
lemma S_truncation Lemma 3.0.3 line 261 source
Source documentation
Lemma 3.0.3. B is the blueprint's S.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, MeasureTheory.SimpleFunc, defaultA, FunctionDistances.Θ, Real, IsCancellative, defaultτ, Membership.mem, Set.Ioc, OfNat.ofNat, NNReal.HolderConjugate, Bornology.IsBounded, MeasurableSet, Measurable, LE.le and 21 more
Proof uses: Measurable.iSup, Measurable.enorm, measurable_T_S, Finset.filter, Eq, Finset.Nonempty, Eq.mpr, Exists, And, id, congrArg, propext, Finset.filter_nonempty_iff, Finset.exists_max_image, Exists.intro, of_eq_true, Eq.trans, True, congr, and_self and 51 more
244 instances, coercions and auxiliary constants left out.

Tactic trace: 119 steps
Open to load the checked before-and-after goal states.
```
lemma S_truncation
    [IsCancellative X (defaultτ a)] {B : ℕ} (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q')
    (bF : IsBounded F) (bG : IsBounded G) (mF : MeasurableSet F) (mG : MeasurableSet G)
    (mf : Measurable f) (nf : (‖f ·‖) ≤ F.indicator 1)
    (BST_T_Q : ∀ θ : Θ X, HasBoundedStrongType (linearizedNontangentialOperator Q θ K · ·)
      2 2 volume volume (C_Ts a)) :
    ∫⁻ x in G, ⨆ s₁ ∈ Finset.Icc (-B : ℤ) B, ⨆ s₂ ∈ Finset.Icc s₁ B, ‖T_S Q s₁ s₂ f x‖ₑ ≤
    C3_0_4 a q * volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ := by
…
```
Mentions: IsCancellative, defaultτ, mf, linearizedNontangentialOperator, K, C_Ts, T_S, C3_0_4
def L302 The largest integer s₁ satisfying D ^ (-(s₁ - 2)) * R₁ > 1 / 2 line 370 source
Source documentation
The largest integer s₁ satisfying D ^ (-(s₁ - 2)) * R₁ > 1 / 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Int
Proof uses: HAdd.hAdd, Int.floor, Real.logb, defaultD, HMul.hMul, OfNat.ofNat
12 instances, coercions and auxiliary constants left out.
```
def L302 (a : ℕ) (R₁ : ℝ) : ℤ := ⌊Real.logb D (2 * R₁)⌋ + 3
```
def U302 The smallest integer s₂ satisfying D ^ (-(s₂ + 2)) * R₂ < 1 / (4 * D) line 373 source
Source documentation
The smallest integer s₂ satisfying D ^ (-(s₂ + 2)) * R₂ < 1 / (4 * D).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Int
Proof uses: HSub.hSub, Int.ceil, Real.logb, defaultD, HMul.hMul, OfNat.ofNat
12 instances, coercions and auxiliary constants left out.
```
def U302 (a : ℕ) (R₂ : ℝ) : ℤ := ⌈Real.logb D (4 * R₂)⌉ - 2
…
```
lemma R₁_le_D_zpow_div_four line 376 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, Complex, KernelProofData, Real, LE.le, HDiv.hDiv, HPow.hPow, Int, defaultD, HSub.hSub, L302, OfNat.ofNat
Proof uses: LT.lt, Or, le_or_gt, LE.le.trans, Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos, zpow_nonneg, Nat.cast_nonneg', Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, Eq.mpr, HMul.hMul, id, Eq, congrArg, propext, le_div_iff₀' and 90 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
lemma D_zpow_div_two_le_R₂ line 391 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, Complex, KernelProofData, Real, LT.lt, OfNat.ofNat, LE.le, HDiv.hDiv, HPow.hPow, Int, defaultD, U302
Proof uses: Eq.mpr, HMul.hMul, id, Eq, congrArg, propext, div_le_iff₀', zero_lt_two, HSub.hSub, Int.ceil, Real.logb, U302.eq_1, one_lt_realD, Trans.trans, Inv.inv, Eq.rec, Eq.refl, Eq.trans, mul_comm, Eq.symm and 95 more
148 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma monotoneOn_L302 line 408 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, Complex, KernelProofData, MonotoneOn, Real, Int, L302, Set.ofPred, LT.lt, OfNat.ofNat
Proof uses: Membership.mem, Set, LE.le, id, add_le_add, Int.floor, Real.logb, defaultD, HMul.hMul, Int.floor_mono, Real.logb_le_logb_of_le, one_lt_realD, mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, Eq.mp and 5 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma monotoneOn_U302 line 414 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, Complex, KernelProofData, MonotoneOn, Real, Int, U302, Set.ofPred, LT.lt, OfNat.ofNat
Proof uses: Membership.mem, Set, LE.le, id, sub_le_sub_right, Int.ceil, Real.logb, defaultD, HMul.hMul, Int.ceil_le_ceil, Real.logb_le_logb_of_le, one_lt_realD, mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, Eq.mp and 4 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma exists_uniform_annulus_bound There exists a uniform bound for all possible values of L302 and U302 over the annulus in R_truncation line 422 source
Source documentation
There exists a uniform bound for all possible values of L302 and U302 over the annulus in R_truncation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, Complex, KernelProofData, Real, LT.lt, OfNat.ofNat, Exists, Membership.mem, Set, Set.Ioo, Inv.inv, And, Int, Finset, Finset.Icc, Neg.neg, L302, U302
Proof uses: inv_pos_of_pos, Int.natAbs, Exists.intro, Max.max, LT.lt.trans, And.left, And.intro, Eq.mpr, LE.le, id, Eq, monotoneOn_L302, LT.lt.le, And.right, congrArg, propext, Finset.mem_Icc, Decidable.byContradiction, Not, Eq.mp and 1 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma exists_uniform_annulus_bound {R : ℝ} (hR : 0 < R) :
    ∃ B : ℕ, ∀ R₁ ∈ Ioo R⁻¹ R, ∀ R₂ ∈ Ioo R₁ R,
      L302 a R₁ ∈ Finset.Icc (-B : ℤ) B ∧ U302 a R₂ ∈ Finset.Icc (-B : ℤ) B := by
…
```
Mentions: L302, U302
lemma enorm_setIntegral_annulus_le line 445 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, Set, Complex, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real, Int, LE.le, Norm.norm, Set.indicator, OfNat.ofNat, ENNReal, ENorm.enorm, MeasureTheory.integral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume and 7 more
Proof uses: Trans.trans, MeasureTheory.laverage, Metric.ball, HPow.hPow, defaultD, Eq, MeasureTheory.lintegral, HDiv.hDiv, MeasureTheory.Measure, Inter.inter, Eq.mpr, id, congrArg, funext, Eq.trans, congrFun', MeasureTheory.enorm_integral_le_lintegral_enorm, Complex.enorm_exp_I_mul_ofReal, mul_one, HAdd.hAdd and 71 more
226 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
def edgeScales The fringes of the scale interval in Lemma 3.0.2's proof that require separate handling line 477 source
Source documentation
The fringes of the scale interval in Lemma 3.0.2's proof that require separate handling.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Finset, Int
Proof uses: Insert.insert, HSub.hSub, L302, OfNat.ofNat, HAdd.hAdd, U302, Singleton.singleton
8 instances, coercions and auxiliary constants left out.
```
def edgeScales (a : ℕ) (R₁ R₂ : ℝ) : Finset ℤ :=
…
```
lemma diff_subset_edgeScales line 480 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, LE.le, Finset, Int, SDiff.sdiff, Finset.Icc, HSub.hSub, L302, OfNat.ofNat, HAdd.hAdd, U302, edgeScales
Proof uses: Membership.mem, Eq.mpr, Or, Eq, id, Eq.trans, Insert.insert, Singleton.singleton, congrArg, Decidable.byContradiction, Not, Eq.mp, And, LT.lt, congr
46 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma enorm_carlesonOperatorIntegrand_le_T_S line 487 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, Set, Complex, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real, LT.lt, OfNat.ofNat, Measurable, LE.le, Norm.norm, Set.indicator, ENNReal, ENorm.enorm, carlesonOperatorIntegrand, HAdd.hAdd and 7 more
Proof uses: defaultD, one_lt_realD, Finset, Int, Finset.Icc, HSub.hSub, Trans.trans, Finset.sum, edgeScales, MeasureTheory.integral, MeasureTheory.Measure.restrict, Set.Annulus.oo, Ks, Complex.exp, Complex.I, SDiff.sdiff, Eq, id, ENorm, Eq.rec and 125 more
294 instances, coercions and auxiliary constants left out.

Tactic trace: 66 steps
Open to load the checked before-and-after goal states.
lemma lintegral_globalMaximalFunction_le line 541 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, Membership.mem, Set.Ioc, OfNat.ofNat, NNReal.HolderConjugate, Bornology.IsBounded, MeasurableSet, defaultA, LE.le, ENNReal, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, globalMaximalFunction, Real and 6 more
Proof uses: Trans.trans, MeasureTheory.eLpNorm, Eq, Eq.mpr, id, congrArg, funext, MeasureTheory.lintegral_indicator, Eq.refl, ENNReal.lintegral_mul_le_eLpNorm_mul_eLqNorm, ENNReal.HolderConjugate, propext, ENNReal.holderConjugate_coe_iff, NNReal.HolderConjugate.symm, AEMeasurable.indicator, Option.some, aemeasurable_const, Measurable.aemeasurable, maximalFunction, Prod and 36 more
176 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
def T_R The operator T_{R₁, R₂, R} introduced in Lemma 3.0.2 line 567 source
Source documentation
The operator T_{R₁, R₂, R} introduced in Lemma 3.0.2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, Complex, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real
Proof uses: Set.indicator, Metric.ball, cancelPt, carlesonOperatorIntegrand
37 instances, coercions and auxiliary constants left out.
```
def T_R (K : X → X → ℂ) (Q : SimpleFunc X (Θ X)) (R₁ R₂ R : ℝ) (f : X → ℂ) (x : X) : ℂ :=
…
```
Mentions: K
lemma C1_0_2_pos line 570 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal, LT.lt, OfNat.ofNat, C1_0_2
Proof uses: Eq.mpr, HDiv.hDiv, HPow.hPow, HMul.hMul, HAdd.hAdd, 𝕔, HSub.hSub, id, Eq, congrArg, C1_0_2.eq_1, div_pos, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, tsub_pos_of_lt
59 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma le_C1_0_2 line 576 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal, LE.le, OfNat.ofNat, Membership.mem, Set, Set.Ioc, HAdd.hAdd, C3_0_4, HMul.hMul, C2_1_3, C2_0_6, defaultA, C1_0_2
Proof uses: Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, le_imp_le_of_le_of_le, HPow.hPow, HDiv.hDiv, HSub.hSub, add_le_add, le_refl, mul_le_mul', C2_0_6_defaultA_one_le, And.left, LT.lt, div_le_div₀, le_of_lt, Mathlib.Meta.Positivity.pos_of_isNat and 106 more
184 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma R_truncation' line 603 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, MeasureTheory.SimpleFunc, defaultA, FunctionDistances.Θ, Real, IsCancellative, defaultτ, Membership.mem, Set.Ioc, OfNat.ofNat, NNReal.HolderConjugate, MeasurableSet, Measurable, LE.le, Norm.norm and 20 more
Proof uses: LT.lt, Eq.mpr, id, congrArg, pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, inv_pos_of_pos, And, Int, Finset, Finset.Icc, Neg.neg, L302, U302, Exists and 72 more
256 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
lemma R_truncation Lemma 3.0.2 line 662 source
Source documentation
Lemma 3.0.2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, MeasureTheory.SimpleFunc, defaultA, FunctionDistances.Θ, Real, IsCancellative, defaultτ, Membership.mem, Set.Ioc, OfNat.ofNat, NNReal.HolderConjugate, MeasurableSet, Measurable, LE.le, Norm.norm and 18 more
Proof uses: Metric.ball, cancelPt, Not, Or, Classical.em, R_truncation', Inter.inter, Eq.mpr, id, congrArg, Set.inter_comm, Eq.symm, Set.indicator_indicator, dite, Classical.propDecidable, congr, Zero, Set.indicator_of_mem, Set.indicator_of_notMem, of_eq_true and 57 more
226 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
```
lemma R_truncation (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q')
    (mF : MeasurableSet F) (mG : MeasurableSet G) (mf : Measurable f) (nf : (‖f ·‖) ≤ F.indicator 1)
    {n : ℕ} {R : ℝ} (hR : R = 2 ^ n)
    (BST_T_Q : ∀ θ : Θ X, HasBoundedStrongType (linearizedNontangentialOperator Q θ K · ·)
      2 2 volume volume (C_Ts a)) :
    ∫⁻ x in G, ⨆ R₁ ∈ Ioo R⁻¹ R, ⨆ R₂ ∈ Ioo R₁ R, ‖T_R K Q R₁ R₂ R f x‖ₑ ≤
    C1_0_2 a q * volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ := by
…
```
Mentions: mf, linearizedNontangentialOperator, K, C_Ts, T_R, C1_0_2