`Carleson/HolderVanDerCorput.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

31 declarations, 0 contain sorry, 0 declared as axioms

This should roughly contain the contents of chapter 8.

Imports (2)

Imported by 3 files

def cutoff cutoff R t x y is L(x, y) in the proof of Lemma 8.0.1 line 20 source
Source documentation
cutoff R t x y is L(x, y) in the proof of Lemma 8.0.1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MetricSpace, Real
Proof uses: Max.max, OfNat.ofNat, HSub.hSub, HDiv.hDiv, Dist.dist, HMul.hMul
14 instances, coercions and auxiliary constants left out.
```
def cutoff (R t : ℝ) (x y : X) : ℝ :=
…
```
lemma cutoff_nonneg line 25 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MetricSpace, Real, LE.le, OfNat.ofNat, cutoff
Proof uses: of_eq_true, Max.max, HSub.hSub, HDiv.hDiv, Dist.dist, HMul.hMul, Eq.trans, Or, True, congr, congrArg, true_or
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma cutoff_comm line 27 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MetricSpace, Real, Eq, cutoff
Proof uses: id, of_eq_true, Max.max, OfNat.ofNat, HSub.hSub, HDiv.hDiv, Dist.dist, HMul.hMul, Eq.trans, True, congrFun', congrArg, dist_comm, eq_self
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma cutoff_Lipschitz line 31 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MetricSpace, Real, LT.lt, OfNat.ofNat, LipschitzWith, Subtype.mk, LE.le, HDiv.hDiv, HMul.hMul, cutoff
Proof uses: LipschitzWith.const_max, HSub.hSub, Dist.dist, LipschitzWith.of_le_add_mul, id, HAdd.hAdd, Eq.mpr, Inv.inv, Eq, Eq.trans, congr, congrArg, div_eq_inv_mul, congrFun', mul_one, mul_le_mul_of_nonneg_left, dist_triangle, le_of_lt, inv_pos_of_pos, mul_pos and 69 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma cutoff_continuous line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MetricSpace, Real, LT.lt, OfNat.ofNat, Continuous, cutoff
Proof uses: LipschitzWith.continuous, Subtype.mk, LE.le, HDiv.hDiv, HMul.hMul, cutoff_Lipschitz
22 instances, coercions and auxiliary constants left out.
lemma cutoff_measurable cutoff R t x is measurable in y line 49 source
Source documentation
cutoff R t x is measurable in y.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, Measurable, NNReal, defaultA, cutoff
Proof uses: Continuous.measurable, cutoff_continuous
36 instances, coercions and auxiliary constants left out.
```
lemma cutoff_measurable (hR : 0 < R) (ht : 0 < t) : Measurable (fun y ↦ cutoff R t x y) :=
…
```
Mentions: cutoff
lemma cutoff_eq_zero line 52 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MetricSpace, Real, LT.lt, OfNat.ofNat, Not, Membership.mem, Set, Metric.ball, HMul.hMul, Eq, cutoff
Proof uses: Eq.mpr, LE.le, HDiv.hDiv, Dist.dist, id, Eq.trans, Max.max, HSub.hSub, HAdd.hAdd, congrArg, zero_add, propext, one_le_div, mul_pos, Eq.mp, congrFun', dist_comm
64 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma hasCompactSupport_cutoff line 58 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MetricSpace, Real, ProperSpace, LT.lt, OfNat.ofNat, HasCompactSupport, cutoff
Proof uses: HasCompactSupport.intro, Metric.closedBall, HMul.hMul, ProperSpace.isCompact_closedBall, Not, Membership.mem, Set, cutoff_eq_zero, Mathlib.Tactic.Contrapose.contrapose₄, Metric.ball, Metric.ball_subset_closedBall
20 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma integrable_cutoff line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, MeasureTheory.Integrable, NNReal, defaultA, cutoff, MeasureTheory.MeasureSpace.volume
Proof uses: Continuous.integrable_of_hasCompactSupport, cutoff_continuous, hasCompactSupport_cutoff
53 instances, coercions and auxiliary constants left out.
lemma integrable_cutoff_mul line 71 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, Continuous, LE.le, Function.support, Metric.ball, MeasureTheory.Integrable, NNReal, defaultA, HMul.hMul, cutoff, MeasureTheory.MeasureSpace.volume
Proof uses: Continuous.integrable_of_hasCompactSupport, Continuous.mul, cutoff_continuous, Continuous.comp', Complex.continuous_ofReal, HasCompactSupport.mul_left, HasCompactSupport.of_support_subset_isCompact, Metric.closedBall, ProperSpace.isCompact_closedBall, LE.le.trans, Metric.ball_subset_closedBall
95 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma leq_of_max_neq_left Is this useful for mathlib? line 84 source
Source comment
Is this useful for mathlib? neither exact? nor aesop can prove this. Same for the next lemma.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Ne, Max.max, LT.lt
Proof uses: Decidable.byContradiction, Not, max_eq_left, Eq.mp, LE.le
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma leq_of_max_neq_left {a b : ℝ} (h : max a b ≠ a) : a < b := by
…
```
lemma leq_of_max_neq_right line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, Ne, Max.max, LT.lt
Proof uses: Decidable.byContradiction, Not, max_eq_right, Eq.mp, LE.le
10 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma aux_8_0_4 Equation 8.0.4 from the blueprint line 93 source
Source documentation
Equation 8.0.4 from the blueprint

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MetricSpace, Real, LT.lt, OfNat.ofNat, Ne, cutoff, Membership.mem, Set, Metric.ball, HMul.hMul
Proof uses: Mathlib.Tactic.Contrapose.contrapose₂, Eq, Not, cutoff_eq_zero
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma aux_8_0_4 (hR : 0 < R) (ht : 0 < t) (h : cutoff R t x y ≠ 0) : y ∈ ball x (t * R) := by
…
```
Mentions: cutoff
lemma aux_8_0_5 line 97 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MetricSpace, Real, LT.lt, OfNat.ofNat, Membership.mem, Set, Metric.ball, HMul.hMul, Inv.inv, Nat, LE.le, cutoff
Proof uses: HDiv.hDiv, Dist.dist, Iff.mpr, div_lt_iff₀, mul_pos, Eq.mp, congrArg, mul_assoc, propext, Metric.mem_ball', Trans.trans, HSub.hSub, Eq, rfl, Eq.mpr, Mathlib.Meta.NormNum.instAtLeastTwo, id, Eq.trans, congrFun', Mathlib.Meta.NormNum.IsNNRat.to_eq and 76 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma aux_8_0_6 line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, LE.le, HMul.hMul, Inv.inv, MeasureTheory.Measure.real, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, Metric.ball, MeasureTheory.integral, cutoff
Proof uses: Trans.trans, MeasureTheory.Measure.restrict, Eq, rfl, Eq.mpr, HSMul.hSMul, id, congrArg, MeasureTheory.setIntegral_const, mul_comm, Eq.refl, MeasureTheory.setIntegral_mono_on, MeasureTheory.integrableOn_const, MeasureTheory.measure_ball_ne_top, enorm_ne_top, MeasureTheory.Integrable.integrableOn, integrable_cutoff, measurableSet_ball, Membership.mem, aux_8_0_5 and 15 more
154 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma integral_cutoff_pos line 123 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, MeasureTheory.integral, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, cutoff
Proof uses: lt_of_lt_of_le, HMul.hMul, Inv.inv, MeasureTheory.Measure.real, Metric.ball, mul_pos, inv_pos_of_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, MeasureTheory.measureReal_ball_pos, aux_8_0_6
81 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
def C8_0_1 The constant occurring in Lemma 8.0.1 line 129 source
Source documentation
The constant occurring in Lemma 8.0.1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, NNReal
Proof uses: Subtype.mk, LE.le, OfNat.ofNat, HMul.hMul, HPow.hPow, Neg.neg, HAdd.hAdd
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
def C8_0_1 (a : ℝ) (t : ℝ≥0) : ℝ≥0 := ⟨2 ^ (4 * a) * t ^ (- (a + 1)), by positivity⟩
```
def holderApprox φ ↦ \tilde{φ} in the proof of Lemma 8.0.1 line 132 source
Source documentation
φ ↦ \tilde{φ} in the proof of Lemma 8.0.1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData
Proof uses: HDiv.hDiv, MeasureTheory.integral, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, HMul.hMul, cutoff
25 instances, coercions and auxiliary constants left out.
```
def holderApprox (R t : ℝ) (φ : X → ℂ) (x : X) : ℂ :=
…
```
lemma integral_mul_holderApprox line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, Eq, HMul.hMul, MeasureTheory.integral, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, cutoff, holderApprox
Proof uses: Eq.mpr, HDiv.hDiv, id, congrArg, holderApprox.eq_1, mul_div_cancel₀, Ne, Not, ne_of_gt, integral_cutoff_pos, Eq.refl
63 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma support_holderApprox_subset_aux line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, LE.le, Function.support, Metric.ball, Membership.mem, Set.Ioc, holderApprox, HAdd.hAdd
Proof uses: Exists, Ne, HMul.hMul, cutoff, MeasureTheory.integral, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, left_ne_zero_of_mul, Inv.inv, Classical.byContradiction, Not, of_eq_true, Eq, Eq.trans, True, congrFun', congrArg, funext, Eq.mp and 24 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma support_holderApprox_subset Part of Lemma 8.0.1 line 166 source
Source documentation
Part of Lemma 8.0.1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, LE.le, Function.support, Metric.ball, Membership.mem, Set.Ioc, holderApprox, HMul.hMul
Proof uses: Eq.mpr, HAdd.hAdd, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, PseudoMetricSpace, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.atom_pf, rfl, id and 16 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma support_holderApprox_subset {z : X} {R t : ℝ} (hR : 0 < R)
    {φ : X → ℂ} (hφ : φ.support ⊆ ball z R) (ht : t ∈ Ioc (0 : ℝ) 1) :
    support (holderApprox R t φ) ⊆ ball z (2 * R) := by
…
```
Mentions: holderApprox
lemma dist_holderApprox_le Part of Lemma 8.0.1: Equation (8.0.1) line 179 source
Source documentation
Part of Lemma 8.0.1: Equation (8.0.1). Note that the norm ||φ||_C^τ is normalized by definition, i.e., on the ball B (z, 2 * R), it is (2 * R) ^ τ times the best Hölder constant of φ, so the Lean statement corresponds to the blueprint statement.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, NNReal, LE.le, Function.support, Metric.ball, HolderOnWith, nnτ, HMul.hMul, Dist.dist, holderApprox, HPow.hPow, HDiv.hDiv and 1 more
Proof uses: Continuous, ContinuousOn.continuous_of_tsupport_subset, HolderOnWith.continuousOn, nnτ_pos, Metric.isOpen_ball, LE.le.trans, closure, closure_mono, Metric.closedBall, Metric.closure_ball_subset_closedBall, Metric.closedBall_subset_ball, lt_of_not_ge, 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 and 148 more
257 instances, coercions and auxiliary constants left out.

Tactic trace: 75 steps
Open to load the checked before-and-after goal states.
```
lemma dist_holderApprox_le {z : X} {R t : ℝ} (hR : 0 < R) {C : ℝ≥0} (ht : 0 < t) (h't : t ≤ 1)
    {φ : X → ℂ} (hφ : support φ ⊆ ball z R) (h2φ : HolderOnWith C nnτ φ (ball z (2 * R))) (x : X) :
    dist (φ x) (holderApprox R t φ x) ≤ (t/2) ^ τ * ((2 * R) ^ τ * C) := by
…
```
Mentions: nnτ, holderApprox
lemma enorm_holderApprox_sub_le line 246 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, LE.le, Function.support, Metric.ball, ENNReal, ENorm.enorm, HSub.hSub, holderApprox, HMul.hMul, HPow.hPow, ENNReal.ofReal, HDiv.hDiv and 2 more
Proof uses: Eq, Top.top, Ne, Or, eq_or_ne, LE.le.trans_eq, le_top, Eq.symm, of_eq_true, Eq.trans, And, Inv.inv, True, congrFun', congrArg, congr, Not, False, false_and, or_false and 137 more
218 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma holderApprox_le Part of Lemma 8.0.1: sup norm control in Equation (8.0.2) line 266 source
Source documentation
Part of Lemma 8.0.1: sup norm control in Equation (8.0.2). Note that it only uses the sup norm of φ, no need for a Hölder control.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, NNReal, LE.le, Norm.norm, holderApprox
Proof uses: Eq.mpr, HDiv.hDiv, MeasureTheory.integral, defaultA, MeasureTheory.MeasureSpace.volume, HMul.hMul, cutoff, id, Eq, congrArg, holderApprox.eq_1, norm_div, Complex.norm_real, abs, Real.norm_eq_abs, div_le_of_le_mul₀, abs_nonneg, NNReal.coe_nonneg, LE.le.trans, MeasureTheory.norm_integral_le_integral_norm and 20 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma holderApprox_le {R t : ℝ} (hR : 0 < R) {C : ℝ≥0} (ht : 0 < t)
    {φ : X → ℂ} (hC : ∀ x, ‖φ x‖ ≤ C) (x : X) :
    ‖holderApprox R t φ x‖ ≤ C := by
…
```
Mentions: holderApprox
lemma norm_holderApprox_sub_le_aux Auxiliary lemma: part of the Lipschitz control in Equation (8.0.2), when the distance between the points is at most R line 285 source
Source documentation
Auxiliary lemma: part of the Lipschitz control in Equation (8.0.2), when the distance between the points is at most R.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, LE.le, NNReal, Continuous, Function.support, Metric.ball, Norm.norm, Dist.dist, HSub.hSub, holderApprox, HDiv.hDiv, HMul.hMul and 3 more
Proof uses: MeasureTheory.Measure.real, defaultA, MeasureTheory.MeasureSpace.volume, MeasureTheory.integral, abs, cutoff, Trans.trans, Eq, HAdd.hAdd, rfl, mul_le_mul_of_nonneg_right, aux_8_0_6, norm_nonneg, Eq.mpr, id, congrArg, norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos and 231 more
337 instances, coercions and auxiliary constants left out.

Tactic trace: 99 steps
Open to load the checked before-and-after goal states.
```
lemma norm_holderApprox_sub_le_aux {z : X} {R t : ℝ} (hR : 0 < R) (ht : 0 < t) (h't : t ≤ 1)
    {C : ℝ≥0} {φ : X → ℂ} (hc : Continuous φ) (hφ : φ.support ⊆ ball z R)
    (hC : ∀ x, ‖φ x‖ ≤ C) {x x' : X} (h : dist x x' < R) :
    ‖holderApprox R t φ x' - holderApprox R t φ x‖ ≤
      2⁻¹ * 2 ^ (4 * a) * t ^ (-1 - a : ℝ) * C * dist x x' / (2 * R) := by
…
```
Mentions: holderApprox
lemma norm_holderApprox_sub_le Part of Lemma 8.0.1: Lipschitz norm control in Equation (8.0.2) line 406 source
Source documentation
Part of Lemma 8.0.1: Lipschitz norm control in Equation (8.0.2). Note that it only uses the sup norm of φ, no need for a Hölder control.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, LE.le, NNReal, Continuous, Function.support, Metric.ball, Norm.norm, HSub.hSub, holderApprox, HDiv.hDiv, HMul.hMul, Inv.inv and 3 more
Proof uses: Or, lt_or_ge, Eq.mpr, id, Eq, congrArg, norm_sub_rev, norm_holderApprox_sub_le_aux, Trans.trans, HAdd.hAdd, rfl, norm_sub_le, add_le_add, holderApprox_le, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.symm, Eq.refl and 109 more
210 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma norm_holderApprox_sub_le {z : X} {R t : ℝ} (hR : 0 < R) (ht : 0 < t) (h't : t ≤ 1)
    {C : ℝ≥0} {φ : X → ℂ} (hc : Continuous φ) (hφ : φ.support ⊆ ball z R)
    (hC : ∀ x, ‖φ x‖ ≤ C) {x x' : X} :
    ‖holderApprox R t φ x - holderApprox R t φ x'‖ ≤
    2⁻¹ * 2 ^ (4 * a) * t ^ (-1 - a : ℝ) * C * dist x x' / (2 * R) := by
…
```
Mentions: holderApprox
lemma lipschitzWith_holderApprox line 435 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, LE.le, NNReal, Continuous, Function.support, Metric.ball, Norm.norm, LipschitzWith, Real.toNNReal, HDiv.hDiv, HMul.hMul, Inv.inv and 4 more
Proof uses: LipschitzWith.of_dist_le', Eq.mpr, Dist.dist, id, Eq, congrArg, dist_eq_norm, eq_of_heq, LE, HEq, Eq.refl, HEq.refl, Eq.symm, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast, NNRat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.div_congr, Mathlib.Tactic.Ring.Common.inv_congr and 32 more
132 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma iLipENorm_holderApprox' line 445 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, LE.le, NNReal, Continuous, Function.support, Metric.ball, Norm.norm, ENNReal, iLipENorm, holderApprox, HMul.hMul, HPow.hPow and 3 more
Proof uses: Real.toNNReal, Eq, id, HMul, Eq.rec, Eq.refl, Eq.mpr, congrArg, ENNReal.coe_rpow_of_ne_zero, Ne, Eq.trans, Not, iLipENorm_le, Membership.mem, Metric.pos_of_mem_ball, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq and 107 more
211 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
lemma iLipENorm_holderApprox_le line 482 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LT.lt, OfNat.ofNat, LE.le, Function.support, Metric.ball, ENNReal, iLipENorm, holderApprox, HMul.hMul, HPow.hPow, ENNReal.ofReal, HSub.hSub, Neg.neg and 2 more
Proof uses: Eq, Top.top, Ne, Or, eq_or_ne, LE.le.trans_eq, le_top, Eq.mpr, id, congrArg, propext, eq_comm, of_eq_true, Eq.trans, True, congrFun', ENNReal.mul_top, Not, And, False and 72 more
168 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
def C2_0_5 The constant occurring in Proposition 2.0.5 line 503 source
Source documentation
The constant occurring in Proposition 2.0.5. Has value 2 ^ (7 * a) in the blueprint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real, NNReal
Proof uses: HPow.hPow, OfNat.ofNat, HMul.hMul
13 instances, coercions and auxiliary constants left out.
```
def C2_0_5 (a : ℝ) : ℝ≥0 := 2 ^ (7 * a)
…
```
theorem holder_van_der_corput Proposition 2.0.5 line 508 source
Source documentation
Proposition 2.0.5.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LE.le, Function.support, Metric.ball, FunctionDistances.Θ, defaultA, ENNReal, ENorm.enorm, MeasureTheory.integral, NNReal, MeasureTheory.MeasureSpace.volume, HMul.hMul, Complex.exp, Complex.I and 12 more
Proof uses: KernelProofData.four_le_a, cast, Eq.symm, LT.lt, Or, le_or_gt, of_eq_true, Eq.trans, True, congr, congrArg, funext, congrFun', Eq.mp, Eq, EmptyCollection.emptyCollection, PseudoMetricSpace, Iff.mpr, Metric.ball_eq_empty, MulZeroClass.mul_zero and 279 more
437 instances, coercions and auxiliary constants left out.

Tactic trace: 148 steps
Open to load the checked before-and-after goal states.
```
theorem holder_van_der_corput {z : X} {R : ℝ} {φ : X → ℂ}
    (φ_supp : support φ ⊆ ball z R) {f g : Θ X} :
    ‖∫ x, exp (I * (f x - g x)) * φ x‖ₑ ≤
    (C2_0_5 a : ℝ≥0∞) * volume (ball z R) * iHolENorm φ z (2 * R) τ *
      (1 + edist_{z, R} f g) ^ (- (2 * a^2 + a^3 : ℝ)⁻¹) := by
…
```
Mentions: g, C2_0_5, iHolENorm