Carleson/ForestOperator/L2Estimate.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

33 declarations, 0 contain sorry, 0 declared as axioms

Section 7.2 and Lemma 7.2.1

Imports (2)
Imported by 2 files
  1. lemma integrableOn_K_mul_f line 17 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, MeasureTheory.BoundedCompactSupport, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, ENNReal, LT.lt, OfNat.ofNat, MeasureTheory.IntegrableOn, HMul.hMul, Set.EAnnulus.ci

    Proof uses: dite, Set.Nonempty, Function.support, Classical.propDecidable, Eq, Top.top, of_eq_true, Eq.trans, EmptyCollection.emptyCollection, True, congrFun', MeasureTheory.Measure, congrArg, autoParam, Set.EAnnulus.ci_eq_empty, Not, Membership.mem, Exists, LE.le, Dist.dist and 68 more

    143 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

  2. def K' Truncated version of K used in proof of nontangential_pointwise_bound line 37 source

    Source comment

    Truncated version of `K` used in proof of `nontangential_pointwise_bound`
    private def K' (b : ℤ) (c : ℤ) (x y : X) := ∑ i ∈ (Icc b c).toFinset, Ks i x y
…

    Mentions: c, Ks

  3. lemma K'.eq_K line 41 source
  4. lemma K'.integrableOn_mul_f line 49 source
  5. lemma K'.support_subset line 60 source
  6. lemma K'.enorm_le_enorm_K line 90 source
  7. lemma annulus_integral_bound Documented declaration: annulus_integral_bound line 108 source

    Source comment

    Bound needed for proof of `nontangential_pointwise_bound`, splitting the annulus between radii `r₁` and `r₄` into annuli between `r₁` and `r₂`, between `r₂` and `r₃`, and between `r₃` and `r₄`. Note that we assume only `r₁ ≤ r₂` and `r₃ ≤ r₄`.
    private lemma annulus_integral_bound {x : X} {g : X → ℂ} {r₁ r₂ r₃ r₄ : ℝ} (h₁₂ : r₁ ≤ r₂)
    (h₃₄ : r₃ ≤ r₄) (hg : IntegrableOn g (Annulus.cc x r₁ r₄)) :
    ‖∫ y in Annulus.cc x r₁ r₄, g y‖ₑ ≤ ‖∫ y in Annulus.oc x r₂ r₃, g y‖ₑ +
    ((∫⁻ y in Annulus.cc x r₁ r₂, ‖g y‖ₑ) + ∫⁻ y in Annulus.cc x r₃ r₄, ‖g y‖ₑ) :=
…

    Mentions: g

  8. lemma TileStructure.Forest.eLpNorm_MB_le line 146 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, RCLike, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, LE.le, ENNReal and 10 more

    Proof uses: And.right, MeasureTheory.AEStronglyMeasurable, hasStrongType_maximalFunction_one, HPow.hPow, Module.finrank, one_lt_two, MeasureTheory.BoundedCompactSupport.memLp

    166 instances, coercions and auxiliary constants left out.

  9. lemma TileStructure.Forest.nontangential_integral_bound₁ line 159 source
  10. lemma TileStructure.Forest.nontangential_integral_bound₂ Bound for (7.2.4) and (7.2.5) in the proof of nontangential_pointwise_bound line 207 source

    Source comment

    Bound for (7.2.4) and (7.2.5) in the proof of `nontangential_pointwise_bound`
    private lemma nontangential_integral_bound₂ (hf : BoundedCompactSupport f) {x x' : X}
    {I : Grid X} (hx : x ∈ I) (hx' : x' ∈ I) {R : ℝ} (h : R ≤ 8 * D ^ s I) :
    ∫⁻ y in Annulus.cc x' ((D : ℝ) ^ (s I - 1) / 4) R, ‖K x' y * f y‖ₑ ≤
    2 ^ (7 * a + (𝕔 + 1) * a ^ 3) * maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x := by
…

    Mentions: Grid, s, K, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑

  11. lemma TileStructure.Forest.nontangential_pointwise_bound Pointwise bound needed for Lemma 7.2.2 line 254 source

    Source comment

    Pointwise bound needed for Lemma 7.2.2
    private lemma nontangential_pointwise_bound (hf : BoundedCompactSupport f) (θ : Θ X) (x : X) :
    nontangentialMaximalFunction θ f x ≤
    2 * linearizedNontangentialOperator Q θ K f x +
    2 ^ (7 * a + (𝕔 + 1) * a ^ 3 + 1) * maximalFunction volume 𝓑 c𝓑 r𝓑 1 f x := by
…

    Mentions: TileStructure.Forest.nontangentialMaximalFunction, linearizedNontangentialOperator, K, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑

  12. lemma TileStructure.Forest.le_C7_2_2 line 335 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, HAdd.hAdd, HMul.hMul, C_Ts, HPow.hPow, 𝕔, CMB, defaultA, TileStructure.Forest.C7_2_2

    Proof uses: Eq.mpr, id, Eq, congrArg, C_Ts.eq_1, Real, HDiv.hDiv, CMB_defaultA_two_eq, Trans.trans, Eq.symm, pow_succ', add_le_add, le_refl, mul_le_mul', NNReal.rpow_natCast, Nat.cast_add, NNReal.rpow_le_rpow_of_exponent_le, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one and 64 more

    155 instances, coercions and auxiliary constants left out.

    Tactic trace: 35 steps

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

  13. lemma TileStructure.Forest.nontangential_operator_bound Lemma 7.2.2 line 358 source

    Source documentation

    Lemma 7.2.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, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, FunctionDistances.Θ, LE.le, ENNReal and 5 more

    Proof uses: AEMeasurable, maximalFunction, Prod, Grid, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑, Measurable.aemeasurable, measurable_maximalFunction, And, MeasureTheory.AEStronglyMeasurable, linearizedNontangentialOperator, MeasureTheory.SimpleFunc, C_Ts, ProofData.BST_T_Q, MeasureTheory.BoundedCompactSupport.boundedFiniteSupport, Trans.trans, HAdd.hAdd, HPow.hPow, 𝕔 and 61 more

    207 instances, coercions and auxiliary constants left out.

    Tactic trace: 22 steps

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

    lemma nontangential_operator_bound (hf : BoundedCompactSupport f) (θ : Θ X) :
    eLpNorm (nontangentialMaximalFunction θ f) 2 volume ≤ C7_2_2 a * eLpNorm f 2 volume := by
…

    Mentions: TileStructure.Forest.nontangentialMaximalFunction

  14. def TileStructure.Forest.kissing The set of cubes in Lemma 7.2.4 line 397 source

    Source documentation

    The set of cubes in Lemma 7.2.4.

    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, Finset

    Proof uses: Finset.filter, And, Eq, s, Not, Disjoint, Metric.ball, c, HMul.hMul, OfNat.ofNat, HPow.hPow, Classical.propDecidable, Finset.univ

    50 instances, coercions and auxiliary constants left out.

    def kissing (I : Grid X) : Finset (Grid X) :=
…

    Mentions: Grid

  15. lemma TileStructure.Forest.subset_of_kissing line 400 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, Membership.mem, Finset, TileStructure.Forest.kissing, LE.le and 7 more

    Proof uses: And, Exists, Iff.mp, Not, Disjoint, Set.not_disjoint_iff, And.right, Eq, Eq.mp, Finset.filter, Classical.propDecidable, Finset.univ, Metric.ball_subset_ball', Trans.trans, HAdd.hAdd, Dist.dist, Eq.mpr, id, congrArg, add_assoc and 28 more

    143 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  16. lemma TileStructure.Forest.volume_le_of_kissing line 417 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, Membership.mem, Finset, TileStructure.Forest.kissing, LE.le and 10 more

    Proof uses: And, Exists, Iff.mp, Not, Disjoint, Set.not_disjoint_iff, And.right, Eq, Eq.mp, Finset.filter, Classical.propDecidable, Finset.univ, Metric.ball_subset_ball', Trans.trans, HAdd.hAdd, Dist.dist, Eq.mpr, id, congrArg, add_assoc and 75 more

    176 instances, coercions and auxiliary constants left out.

    Tactic trace: 23 steps

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

  17. lemma TileStructure.Forest.pairwiseDisjoint_of_kissing line 439 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, Set.PairwiseDisjoint, Finset, TileStructure.Forest.kissing, Metric.ball and 5 more

    Proof uses: Membership.mem, Ne, Set.disjoint_of_subset, GridStructure.c, GridStructure.s, GridStructure.ball_subset_Grid, Or.resolve_left, Eq, Disjoint, eq_or_disjoint, Eq.trans, And.left, Not, HMul.hMul, And.right, Finset.univ, And, Eq.mp, Finset.filter, Classical.propDecidable and 1 more

    84 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  18. lemma TileStructure.Forest.boundary_overlap Lemma 7.2.4 line 447 source

    Source documentation

    Lemma 7.2.4.

    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, Finset.card, TileStructure.Forest.kissing, HPow.hPow and 2 more

    Proof uses: ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Metric.ball, c, s, Trans.trans, Set.iUnion, Membership.mem, Finset, HDiv.hDiv, Eq, Finset.sum, Eq.mpr, HSMul.hSMul, id, congrArg, Finset.sum_const, nsmul_eq_mul, Eq.refl and 36 more

    160 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

    lemma boundary_overlap (I : Grid X) : (kissing I).card ≤ 2 ^ (9 * a) := by
…

    Mentions: Grid, TileStructure.Forest.kissing

  19. lemma TileStructure.Forest.e728_push_toReal line 463 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, TileStructure.Forest, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, Eq and 10 more

    Proof uses: Eq.mpr, ENNReal, id, congrArg, TileStructure.Forest.boundaryOperator.eq_1, ENNReal.toReal_sum, LT.lt, Top.top, TileStructure.Forest.boundaryOperator_lt_top, Membership.mem, Finset, LT.lt.ne, Eq.mp, forall_congr, Finset.sum_congr, Eq.refl, dite, ite, Classical.decPred, OfNat.ofNat and 6 more

    81 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  20. lemma TileStructure.Forest.e728_rearrange line 476 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, TileStructure.Forest, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, Eq and 23 more

    Proof uses: Trans.trans, TileStructure.Forest.ijIntegral, Set.indicator, NormedAddCommGroup, NormedSpace, MeasurableSpace, Eq.rec, Eq.refl, funext, Eq.mpr, id, congrArg, TileStructure.Forest.e728_push_toReal, Complex.ofReal_sum, Finset.mul_sum, AddCommMonoid, Finset, Set.indicator_const_mul, HMul, dite and 58 more

    216 instances, coercions and auxiliary constants left out.

    Tactic trace: 43 steps

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

  21. lemma TileStructure.Forest.e728 Equation (7.2.8) in the proof of Lemma 7.2.3 line 531 source

    Source documentation

    Equation (7.2.8) in the proof of Lemma 7.2.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, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, LE.le and 32 more

    Proof uses: AEMeasurable, MeasureTheory.AEStronglyMeasurable.enorm, MeasureTheory.BoundedCompactSupport.aestronglyMeasurable, Trans.trans, Eq, MeasureTheory.laverage, TileStructure.Forest.𝓙', Inv.inv, MeasureTheory.Measure, Eq.mpr, id, congrArg, TileStructure.Forest.e728_rearrange, Eq.refl, NNNorm.nnnorm, congr, Finset.sum_congr, Finset, nnnorm_sum_le, congrFun' and 117 more

    321 instances, coercions and auxiliary constants left out.

    Tactic trace: 69 steps

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

    lemma e728 (hf : BoundedCompactSupport f) (hg : BoundedCompactSupport g) :
    ‖∫ x, conj (g x) * (t.boundaryOperator u f x).toReal‖ₑ ≤
    ∑ J ∈ 𝓙 (t u), ∫⁻ y in J, ‖f y‖ₑ * maximalFunction volume 𝓑 c𝓑 r𝓑 1 g y *
      ∑ I : Grid X, if (J : Set X) ⊆ ball (c I) (16 * D ^ s I) ∧ s J ≤ s I then
        (D : ℝ≥0∞) ^ ((s J - s I) / (a : ℝ)) else 0 := by
…

    Mentions: g, TileStructure.Forest.𝓙, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑, Grid, c, s

  22. lemma TileStructure.Forest.boundary_geometric_series Bound for the inner sum in Equation (7.2.8) line 608 source

    Source documentation

    Bound for the inner sum in Equation (7.2.8).

    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, ENNReal, Finset.sum, Finset.univ and 12 more

    Proof uses: Trans.trans, Eq, tsum, Neg.neg, SummationFilter.unconditional, Set.toFinset, Set.Icc, Int.toNat, Membership.mem, Finset.card, TileStructure.Forest.kissing, Exists.choose, Grid.exists_supercube, Subtype.property, Finset, Eq.mpr, id, congrArg, Finset.sum_comm, AddCommMonoid and 187 more

    326 instances, coercions and auxiliary constants left out.

    Tactic trace: 93 steps

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

    lemma boundary_geometric_series :
    (∑ I : Grid X, if (J : Set X) ⊆ ball (c I) (16 * D ^ s I) ∧ s J ≤ s I then
      (D : ℝ≥0∞) ^ ((s J - s I) / (a : ℝ)) else 0) ≤ 2 ^ (9 * a + 1) :=
…

    Mentions: Grid, c, s

  23. lemma TileStructure.Forest.boundary_operator_bound_aux line 693 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, TileStructure.Forest, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, LE.le and 11 more

    Proof uses: Trans.trans, HPow.hPow, HAdd.hAdd, HDiv.hDiv, Eq, maximalFunction, Prod, Grid, TileStructure.Forest.𝓑, TileStructure.Forest.c𝓑, TileStructure.Forest.r𝓑, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Set.iUnion, Finset.sum, Set.toFinset, TileStructure.Forest.𝓙, TileStructure.Forest.𝔗, Membership.mem, Classical.propDecidable and 183 more

    287 instances, coercions and auxiliary constants left out.

    Tactic trace: 37 steps

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

  24. lemma TileStructure.Forest.boundary_operator_bound Lemma 7.2.3 line 734 source

    Source documentation

    Lemma 7.2.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, 𝔓, MeasureTheory.BoundedCompactSupport, MeasureTheory.MeasureSpace.volume, LE.le and 6 more

    Proof uses: ENNReal.toReal, Eq.mpr, Finset.sum, Grid, Finset.univ, Set.indicator, TileStructure.Forest.𝓙', c, s, TileStructure.Forest.ijIntegral, id, Eq, congrFun', MeasureTheory.Measure, congrArg, autoParam, funext, TileStructure.Forest.e728_push_toReal, MeasureTheory.BoundedCompactSupport.finset_sum, Membership.mem and 74 more

    212 instances, coercions and auxiliary constants left out.

    Tactic trace: 33 steps

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

    lemma boundary_operator_bound (hf : BoundedCompactSupport f) :
    eLpNorm (t.boundaryOperator u f) 2 volume ≤ C7_2_3 a * eLpNorm f 2 volume := by
…
  25. def TileStructure.Forest.eI𝒬u_mul Auxiliary function used in the proof of Lemma 7.2.1 line 771 source

    Source comment

    Auxiliary function used in the proof of Lemma 7.2.1
    private def eI𝒬u_mul (u : 𝔓 X) (f : X → ℂ) : X → ℂ := fun y ↦ exp (.I * 𝒬 u y) * f y

    Mentions: 𝔓

  26. lemma TileStructure.Forest.boundedCompactSupport_eI𝒬u_mul line 773 source
  27. lemma TileStructure.Forest.norm_eI𝒬u_mul_eq line 779 source
  28. def TileStructure.Forest.cS_bound line 784 source
  29. lemma TileStructure.Forest.aeMeasurable_cS_bound line 789 source
  30. lemma TileStructure.Forest.le_C7_2_1 The natural constant for Lemma 7.2.1 is ≤ the simpler constant C7_2_1 we use instead line 795 source

    Source comment

    The natural constant for Lemma 7.2.1 is ≤ the simpler constant `C7_2_1` we use instead.
    private lemma le_C7_2_1 {a : ℕ} (ha : 4 ≤ a) :
    C7_1_3 a * CMB (defaultA a) 2 + C7_1_3 a * C7_2_3 a + C7_2_2 a ≤ (C7_2_1 a : ℝ≥0∞) := calc
…

    Mentions: defaultA

  31. lemma TileStructure.Forest.eLpNorm_two_cS_bound_le Main estimate used in the proof of tree_projection_estimate line 828 source

    Source comment

    Main estimate used in the proof of `tree_projection_estimate`
    private lemma eLpNorm_two_cS_bound_le : eLpNorm (cS_bound t u f) 2 volume ≤
    C7_2_1 a * eLpNorm (approxOnCube (𝓙 (t u)) (‖f ·‖)) 2 volume := by
…

    Mentions: TileStructure.Forest.cS_bound, TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙

  32. lemma TileStructure.Forest.Complex.enorm_real TODO: PR next to Complex.norm_real line 871 source

    Source comment

    TODO: PR next to `Complex.norm_real`

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

    Statement uses: Real, Eq, ENNReal, ENorm.enorm, Complex

    Proof uses: of_eq_true, NNNorm.nnnorm, Eq.trans, True, congrFun', congrArg, NNReal, Complex.nnnorm_real, eq_self

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

     protected lemma Complex.enorm_real (x : ℝ) : ‖(x : ℂ)‖ₑ = ‖x‖ₑ := by simp [enorm]
  33. lemma TileStructure.Forest.tree_projection_estimate Lemma 7.2.1 line 874 source

    Source documentation

    Lemma 7.2.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, Membership.mem and 16 more

    Proof uses: Eq.mpr, id, Eq, congrArg, rfl, ENNReal.ofReal, TileStructure.Forest.approxOnCube_nonneg, norm_nonneg, Trans.trans, MeasureTheory.lintegral, MeasureTheory.Measure.restrict, Set.iUnion, Grid, Finset.sum, Set.toFinset, Classical.propDecidable, iInf, 𝓘, MeasureTheory.enorm_integral_le_lintegral_enorm, Set.indicator and 137 more

    285 instances, coercions and auxiliary constants left out.

    Tactic trace: 62 steps

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

    lemma tree_projection_estimate
    (hf : BoundedCompactSupport f) (hg : BoundedCompactSupport g) (hu : u ∈ t) :
    ‖∫ x, conj (g x) * carlesonSum (t u) f x‖ₑ ≤
    C7_2_1 a * eLpNorm (approxOnCube (𝓙 (t u)) (‖f ·‖)) 2 volume *
    eLpNorm (approxOnCube (𝓛 (t u)) (‖g ·‖)) 2 volume := by
…

    Mentions: g, carlesonSum, TileStructure.Forest.approxOnCube, TileStructure.Forest.𝓙, TileStructure.Forest.𝓛