Carleson/ForestOperator/QuantativeEstimate.lean

GitHub source file

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

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

14 declarations, 0 contain sorry, 0 declared as axioms

Section 7.3 and Lemma 7.3.1

Imports (1)
Imported by 2 files
  1. lemma TileStructure.Forest.local_dens1_tree_bound_exists Part 1 of Lemma 7.3.2 line 29 source

    Source documentation

    Part 1 of Lemma 7.3.2.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, TileStructure.Forest.𝓛 and 17 more

    Proof uses: π“˜, Mathlib.Tactic.Contrapose.contraposeβ‚„, Disjoint.mono_left, E_subset_π“˜, Eq.mp, congrArg, propext, disjoint_comm, Eq, le_antisymm, TileStructure.Forest.le_of_mem_𝓛, Or.resolve_right, le_or_disjoint, Trans.trans, HPow.hPow, OfNat.ofNat, Eβ‚‚, MeasureTheory.measure_mono, And.intro, TileLike.fst and 120 more

    236 instances, coercions and auxiliary constants left out.

    Tactic trace: 44 steps

    Open to load the checked before-and-after goal states.

    lemma local_dens1_tree_bound_exists (hu : u ∈ t) (hL : L ∈ 𝓛 (t u))
    (hpβ‚‚ : βˆƒ p ∈ t u, Β¬Disjoint ↑L (E p) ∧ 𝔰 p ≀ s L) :
    volume (L ∩ G ∩ ⋃ p ∈ t u, E p) ≀ C7_3_2 a * dens₁ (t u) * volume (L : Set X) := by
…

    Mentions: TileStructure.Forest.𝓛, E, 𝔰, s, dens₁

  2. lemma TileStructure.Forest.volume_bound_of_Grid_lt line 67 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Grid, LE.le, Eq, s, HAdd.hAdd and 7 more

    Proof uses: Metric.ball, c, HDiv.hDiv, LT.lt, Dist.dist, Trans.trans, add_lt_add_left, Eq.mpr, Membership.mem, id, congrArg, Eq.symm, propext, Metric.mem_ball, LE.le.trans, GridStructure.c, GridStructure.s, Prod.fst, GridStructure.Grid, Prod.mk and 110 more

    234 instances, coercions and auxiliary constants left out.

    Tactic trace: 26 steps

    Open to load the checked before-and-after goal states.

  3. lemma TileStructure.Forest.local_dens1_tree_bound Lemma 7.3.2 line 91 source

    Source documentation

    Lemma 7.3.2.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, TileStructure.Forest.𝓛 and 11 more

    Proof uses: dite, Eq, EmptyCollection.emptyCollection, Eq.mpr, id, congrArg, Set.inter_comm, Set.inter_assoc, Set.inter_empty, OfNat.ofNat, MeasureTheory.measure_empty, zero_le, Not, Exists, And, Disjoint, 𝔰, s, Classical.propDecidable, TileStructure.Forest.local_dens1_tree_bound_exists and 180 more

    260 instances, coercions and auxiliary constants left out.

    Tactic trace: 128 steps

    Open to load the checked before-and-after goal states.

    lemma local_dens1_tree_bound (hu : u ∈ t) (hL : L ∈ 𝓛 (t u)) :
    volume (L ∩ G ∩ ⋃ p ∈ t u, E p) ≀ C7_3_2 a * dens₁ (t u) * volume (L : Set X) := by
…

    Mentions: TileStructure.Forest.𝓛, E, dens₁

  4. lemma TileStructure.Forest.le_C7_3_3_exponent line 183 source
  5. lemma TileStructure.Forest.local_dens2_tree_bound_aux Auxiliary result used to prove local_dens2_tree_bound line 188 source

    Source comment

    Auxiliary result used to prove `local_dens2_tree_bound`
    private lemma local_dens2_tree_bound_aux {p : 𝔓 X} (hpu : p ∈ t u) {r : ℝ}
    (hr : r β‰₯ 4 * (D : ℝ) ^ (𝔰 p)) (h₁ : (J : Set X) βŠ† ball (𝔠 p) r)
    (hβ‚‚ : volume (ball (𝔠 p) r) ≀ C7_3_3 a * volume (J : Set X)) :
    volume (F ∩ J) ≀ C7_3_3 a * densβ‚‚ (t u) * volume (J : Set X) := by
…

    Mentions: 𝔓, 𝔰, 𝔠, densβ‚‚

  6. lemma TileStructure.Forest.local_dens2_tree_bound_aux' Special case of local_dens2_tree_bound_aux which is used twice line 201 source

    Source comment

    Special case of `local_dens2_tree_bound_aux` which is used twice
    private lemma local_dens2_tree_bound_aux' {p : 𝔓 X} (hpu : p ∈ t u)
    (h₁ : (J : Set X) βŠ† ball (𝔠 p) (4 * (D : ℝ) ^ (𝔰 p)))
    (hβ‚‚ : volume (π“˜ p : Set X) ≀ 2 ^ (2 * 𝕔 * a ^ 3 + 10 * a) * volume (J : Set X)) :
    volume (F ∩ J) ≀ C7_3_3 a * densβ‚‚ (t u) * volume (J : Set X) := by
…

    Mentions: 𝔓, 𝔠, 𝔰, π“˜, densβ‚‚

  7. lemma TileStructure.Forest.local_dens2_tree_bound Lemma 7.3.3 line 217 source

    Source documentation

    Lemma 7.3.3.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, TileStructure.Forest, 𝔓, Grid, Membership.mem, TileStructure.Forest.𝓙 and 9 more

    Proof uses: dite, Eq, GridStructure.topCube, Classical.propDecidable, Set.Nonempty, TileStructure.Forest.nonempty, OfNat.ofNat, TileStructure.Forest.S_eq_zero_of_topCube_mem_𝓙₀, TileStructure.Forest.𝓙_subset_𝓙₀, Eq.rec, π“˜, Eq.trans, Grid.eq_topCube_of_S_eq_zero, Eq.symm, Metric.ball, 𝔠, HPow.hPow, 𝔰, GridStructure.Grid_subset_ball, HAdd.hAdd and 197 more

    263 instances, coercions and auxiliary constants left out.

    Tactic trace: 58 steps

    Open to load the checked before-and-after goal states.

    lemma local_dens2_tree_bound (hu : u ∈ t) (hJ : J ∈ 𝓙 (t u)) :
    volume (F ∩ J) ≀ C7_3_3 a * densβ‚‚ (t u) * volume (J : Set X) := by
…

    Mentions: TileStructure.Forest.𝓙, densβ‚‚

  8. lemma TileStructure.Forest.eLpNorm_approxOnCube_two_le Main bound in the proof of Lemma 7.3.1 line 277 source

    Source comment

    Main bound in the proof of Lemma 7.3.1
    private lemma eLpNorm_approxOnCube_two_le {C : Set (Grid X)}
    (disj_C : C.PairwiseDisjoint (fun I ↦ (I : Set X)))
    {s : Set X} (hs : MeasurableSet s) {c : ℝβ‰₯0∞}
    (hc : βˆ€ J ∈ C, volume (J ∩ s) ≀ c * volume (J : Set X))
    {f : X β†’ β„‚} (hf : BoundedCompactSupport f) (h2f : βˆ€ x βˆ‰ s, f x = 0) :
    eLpNorm (approxOnCube C (β€–f Β·β€–)) 2 volume ≀ c ^ (2 : ℝ)⁻¹ * eLpNorm f 2 := by
…

    Mentions: Grid, s, c, TileStructure.Forest.approxOnCube

  9. lemma TileStructure.Forest.eLpNorm_approxOnCube_two_le_self line 386 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, Grid, Set.PairwiseDisjoint, LE.le and 5 more

    Proof uses: Membership.mem, MeasureTheory.Measure, Inter.inter, Set.univ, HMul.hMul, of_eq_true, Eq.trans, HPow.hPow, 𝕔, True, congr, congrArg, Set.inter_univ, one_mul, Inv.inv, MeasurableSet.univ, Not, False.elim, Eq, trivial and 2 more

    136 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

  10. lemma TileStructure.Forest.density_tree_bound_aux Generalization that implies both parts of Lemma 7.3.1 line 394 source

    Source comment

    Generalization that implies both parts of Lemma 7.3.1
    private lemma density_tree_bound_aux (hf : BoundedCompactSupport f)
    (hg : BoundedCompactSupport g) (h2g : support g βŠ† G) (hu : u ∈ t)
    {c : ℝβ‰₯0∞} (hc : eLpNorm (approxOnCube (𝓙 (t u)) (β€–f Β·β€–)) 2 volume ≀ c * eLpNorm f 2 volume) :
    β€–βˆ« x, conj (g x) * carlesonSum (t u) f xβ€–β‚‘ ≀
    C7_3_1_1 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * c * eLpNorm f 2 volume * eLpNorm g 2 volume := by
…

    Mentions: g, c, TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙, carlesonSum, dens₁

  11. lemma TileStructure.Forest.density_tree_bound1 First part of Lemma 7.3.1 line 462 source

    Source documentation

    First part of Lemma 7.3.1.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, TileStructure.Forest, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, LE.le and 16 more

    Proof uses: TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙, Norm.norm, Grid, MeasureTheory.Measure, Inter.inter, Set.univ, of_eq_true, Eq.trans, 𝕔, True, congr, congrArg, Set.inter_univ, one_mul, le_of_le_of_eq, TileStructure.Forest.pairwiseDisjoint_𝓙, MeasurableSet.univ, Not, False.elim and 9 more

    139 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

    Open to load the checked before-and-after goal states.

    lemma density_tree_bound1 (hf : BoundedCompactSupport f)
    (hg : BoundedCompactSupport g) (h2g : support g βŠ† G) (hu : u ∈ t) :
    β€–βˆ« x, conj (g x) * carlesonSum (t u) f xβ€–β‚‘ ≀
    C7_3_1_1 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * eLpNorm f 2 volume * eLpNorm g 2 volume := by
…

    Mentions: g, carlesonSum, dens₁

  12. lemma TileStructure.Forest.density_tree_bound2 Second part of Lemma 7.3.1 line 477 source

    Source documentation

    Second part of Lemma 7.3.1.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, TileStructure.Forest, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, LE.le and 17 more

    Proof uses: TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙, Norm.norm, TileStructure.Forest.C7_3_3, Not, Eq, Iff.mp, Function.notMem_support, Function.comp, False, Grid, MeasureTheory.Measure, Inter.inter, Eq.mpr, id, congrArg, Set.inter_comm, TileStructure.Forest.local_dens2_tree_bound, TileStructure.Forest.pairwiseDisjoint_𝓙, ProofData.measurableSet_F and 97 more

    248 instances, coercions and auxiliary constants left out.

    Tactic trace: 23 steps

    Open to load the checked before-and-after goal states.

    lemma density_tree_bound2
    (hf : BoundedCompactSupport f) (h2f : support f βŠ† F)
    (hg : BoundedCompactSupport g) (h2g : support g βŠ† G) (hu : u ∈ t) :
    β€–βˆ« x, conj (g x) * carlesonSum (t u) f xβ€–β‚‘ ≀
    C7_3_1_2 a * dens₁ (t u) ^ (2 : ℝ)⁻¹ * densβ‚‚ (t u) ^ (2 : ℝ)⁻¹ *
    eLpNorm f 2 volume * eLpNorm g 2 volume := by
…

    Mentions: g, carlesonSum, dens₁, densβ‚‚

  13. lemma _root_.MeasureTheory.BoundedCompactSupport.const_smul TODO: move somewhere else line 517 source

    Source comment

    TODO: move somewhere else
    lemma _root_.MeasureTheory.BoundedCompactSupport.const_smul (hf : BoundedCompactSupport f) (c : ℝ) :
    BoundedCompactSupport (c β€’ f) := by
…

    Mentions: c

  14. lemma smul_le_indicator rename, move somewhere else line 524 source

    Source comment

    rename, move somewhere else

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Complex, Set, LE.le, Function.support, Real, Norm.norm, LT.lt, OfNat.ofNat, HSMul.hSMul, Inv.inv, Set.indicator

    Proof uses: Eq.mpr, HMul.hMul, abs, id, Eq, congrFun', congrArg, Eq.trans, Complex.ofReal_inv, Complex.norm_mul, norm_inv, Complex.norm_real, propext, inv_mul_le_iffβ‚€, abs_pos_of_pos, mul_comm, Eq.symm, Set.indicator_mul_const, funext, one_mul and 13 more

    108 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

    Open to load the checked before-and-after goal states.

    lemma smul_le_indicator {A : Set X} (hf : f.support βŠ† A) {C : ℝ} (hC : βˆ€ x, β€–f xβ€– ≀ C)
    (hCpos : 0 < C) : βˆ€ x, β€–(C⁻¹ β€’ f) xβ€– ≀ A.indicator 1 x := by
…

    Mentions: A