Carleson/MetricCarleson/Main.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

18 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 3 files
  1. def Θ' A countable dense subset of Θ X line 17 source

    Source documentation

    A countable dense subset of Θ X.

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Set, FunctionDistances.Θ, Real, defaultA

    Proof uses: Exists.choose, And, Set.Countable, Dense

    18 instances, coercions and auxiliary constants left out.

    def Θ' : Set (Θ X) := (TopologicalSpace.exists_countable_dense _).choose
  2. lemma countable_Θ' line 19 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Set.Countable, FunctionDistances.Θ, Real, defaultA, Θ'

    Proof uses: And.left, Exists.choose, Set, And, Dense, TopologicalSpace.exists_countable_dense, Exists.choose_spec

    19 instances, coercions and auxiliary constants left out.

  3. lemma dense_Θ' line 20 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Dense, FunctionDistances.Θ, Real, defaultA, Θ'

    Proof uses: And.right, Set.Countable, Exists.choose, Set, And, TopologicalSpace.exists_countable_dense, Exists.choose_spec

    20 instances, coercions and auxiliary constants left out.

  4. def J102 A countable dense subset of the range of R₁ and R₂ line 23 source

    Source documentation

    A countable dense subset of the range of R₁ and R₂.

    standard axioms: Quot.sound, propext what this means

    Statement uses: Set, Prod, Rat

    Proof uses: Set.ofPred, And, LT.lt, OfNat.ofNat, Prod.fst, Prod.snd

    2 instances, coercions and auxiliary constants left out.

    def J102 : Set (ℚ × ℚ) := {p | 0 < p.1 ∧ p.1 < p.2}
  5. lemma carlesonOperator_eq_biSup_Θ'_J102 line 25 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Measurable, NNReal, defaultA, LE.le, Real, Norm.norm, OfNat.ofNat, Eq, ENNReal, carlesonOperator, iSup, FunctionDistances.Θ, Membership.mem, Set, Θ', Prod and 6 more

    Proof uses: id, linearizedCarlesonOperator, le_antisymm, LT.lt, iSup_le, iSup₂_le, ENNReal.le_of_forall_pos_le_add, Top.top, Continuous, continuous_carlesonOperatorIntegrand, And, GT.gt, Dist.dist, HDiv.hDiv, Exists, HAdd.hAdd, Eq.mp, congrArg, propext, Metric.continuous_iff and 49 more

    218 instances, coercions and auxiliary constants left out.

    Tactic trace: 42 steps

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

  6. def enumΘ' An enumeration of Θ' X, assuming it is nonempty line 77 source

    Source documentation

    An enumeration of Θ' X, assuming it is nonempty. It may contain duplicates.

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Set.Nonempty, FunctionDistances.Θ, Real, defaultA, Θ'

    Proof uses: Exists.choose, Function.Surjective

    19 instances, coercions and auxiliary constants left out.

    def enumΘ' : ℕ → Θ' X :=
…

    Mentions: Θ'

  7. lemma surjective_enumΘ' line 80 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Set.Nonempty, FunctionDistances.Θ, Real, defaultA, Θ', Function.Surjective, enumΘ'

    Proof uses: Exists.choose_spec, Set.Countable.exists_surjective, countable_Θ'

    18 instances, coercions and auxiliary constants left out.

  8. lemma biSup_Θ'_eq_biSup_enumΘ' line 83 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Set.Nonempty, FunctionDistances.Θ, Real, defaultA, Θ', ENNReal, Eq, iSup, Membership.mem, Set, Finset, Finset.range, HAdd.hAdd, OfNat.ofNat, enumΘ'

    Proof uses: le_antisymm, iSup₂_le, Subtype.mk, Exists, LE.le, surjective_enumΘ', of_eq_true, Eq.trans, True, congrArg, congrFun', eq_self, Eq.mpr, id, Trans.trans, LT.lt, propext, Finset.mem_range, eq_of_heq, LE and 8 more

    63 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  9. def enumΘ'ArgMax The argmax of g (enumΘ' nΘ' i) x over i ≤ n with lower indices winning ties line 99 source

    Source documentation

    The argmax of g (enumΘ' nΘ' i) x over i ≤ n with lower indices winning ties.

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Set.Nonempty, FunctionDistances.Θ, Real, defaultA, Θ', ENNReal

    Proof uses: List.findIdx, Decidable.decide, LE.le, Membership.mem, Set, enumΘ', List.range, HAdd.hAdd, OfNat.ofNat

    26 instances, coercions and auxiliary constants left out.

    def enumΘ'ArgMax (n : ℕ) (x : X) : ℕ :=
…
  10. lemma enumΘ'ArgMax_mem_range line 102 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Set.Nonempty, FunctionDistances.Θ, Real, defaultA, Θ', ENNReal, Membership.mem, Finset, Finset.range, HAdd.hAdd, OfNat.ofNat, enumΘ'ArgMax

    Proof uses: Eq.mpr, LT.lt, id, Eq, congrArg, propext, Finset.mem_range, List.length, List.range, Eq.symm, List.length_range, List.findIdx, Decidable.decide, LE.le, Set, enumΘ', enumΘ'ArgMax.eq_1, Exists, And, List and 22 more

    53 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  11. lemma enumΘ'ArgMax_eq_iff The characterising property of enumΘ'ArgMax line 110 source

    Source documentation

    The characterising property of enumΘ'ArgMax.

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Set.Nonempty, FunctionDistances.Θ, Real, defaultA, Θ', ENNReal, LE.le, Iff, Eq, enumΘ'ArgMax, And, Membership.mem, Set, enumΘ', LT.lt

    Proof uses: Eq.mpr, List.findIdx, Decidable.decide, List.range, HAdd.hAdd, OfNat.ofNat, id, congrArg, enumΘ'ArgMax.eq_1, Bool, GetElem.getElem, List, List.length, List.length_range, Bool.true, Nat.lt_trans, Bool.false, propext, List.findIdx_eq, congrFun' and 19 more

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

    lemma enumΘ'ArgMax_eq_iff {n i : ℕ} {x : X} (hi : i ≤ n) :
    enumΘ'ArgMax nΘ' g n x = i ↔
    (∀ j ≤ n, g (enumΘ' nΘ' j) x ≤ g (enumΘ' nΘ' i) x) ∧
    ∀ j < i, g (enumΘ' nΘ' j) x < g (enumΘ' nΘ' i) x := by
…

    Mentions: enumΘ'ArgMax, g, enumΘ'

  12. def QΘ' The simple function corresponding to the blueprint's Q_n line 123 source

    Source documentation

    The simple function corresponding to the blueprint's Q_n.

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Set.Nonempty, FunctionDistances.Θ, Real, defaultA, Θ', ENNReal, Measurable, NNReal, MeasureTheory.SimpleFunc

    Proof uses: MeasureTheory.SimpleFunc.mk, Membership.mem, Set, enumΘ', enumΘ'ArgMax

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 31 steps

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

    def QΘ' (n : ℕ) : SimpleFunc X (Θ X) where
…
  13. lemma biSup_enumΘ'_le_QΘ' line 149 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Set.Nonempty, FunctionDistances.Θ, Real, defaultA, Θ', ENNReal, Measurable, NNReal, LE.le, iSup, Membership.mem, Finset, Finset.range, HAdd.hAdd, OfNat.ofNat, Set and 3 more

    Proof uses: Eq.mpr, MeasureTheory.SimpleFunc.mk, enumΘ'ArgMax, id, Eq, congrArg, QΘ'.eq_1, MeasureTheory.SimpleFunc.coe_mk, iSup₂_le, enumΘ'ArgMax_mem_range, Iff, And, LT.lt, enumΘ'ArgMax_eq_iff, Eq.mp, propext, Nat.lt_add_one_iff, Finset.mem_range, And.left, Eq.trans and 4 more

    79 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  14. lemma lowerSemicontinuous_LNT line 159 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real, LowerSemicontinuous, ENNReal, linearizedNontangentialOperator

    Proof uses: id, Eq.mpr, iSup, Membership.mem, Set, Set.Ioo, OfNat.ofNat, Metric.ball, ENorm.enorm, MeasureTheory.integral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.EAnnulus.oo, ENNReal.ofReal, Min.min, upperRadius, HMul.hMul, IsOpen, Set.preimage, Set.Ioi and 29 more

    90 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  15. lemma BST_LNT_of_BST_NT line 170 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real, MeasureTheory.HasBoundedStrongType, ENNReal, nontangentialOperator, OfNat.ofNat, MeasureTheory.MeasureSpace.volume, C_Ts, linearizedNontangentialOperator

    Proof uses: BoundedFiniteSupport, And.intro, MeasureTheory.AEStronglyMeasurable, LE.le, MeasureTheory.eLpNorm, HMul.hMul, Measurable.aestronglyMeasurable, LowerSemicontinuous.measurable, lowerSemicontinuous_LNT, LE.le.trans, MeasureTheory.eLpNorm_mono_enorm, id, ENorm.enorm, iSup_le, iSup, Membership.mem, Set, Set.Ioo, Metric.ball, MeasureTheory.integral and 52 more

    152 instances, coercions and auxiliary constants left out.

    Tactic trace: 46 steps

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

  16. theorem metric_carleson Metric Carleson theorem (Theorem 1.1.1) line 203 source

    Source documentation

    Theorem 1.1.1

    L4DEL explanation

    The sup over phases is reduced to a countable dense set of phases and rational radii, then to finitely many phases, where the linearized theorem applies, and a monotone limit passes the bound to the supremum.

    1. Rewrite carlesonOperator as a supremum over a countable dense subset of phases and over rational radii in J102.
    2. Enumerate the countable phase set and take increasing finite maxima, then use monotone convergence of lintegral to move the supremum outside the integral.
    3. At each finite stage build a simple-function phase choice Q that realises the maximum, and apply linearized_metric_carleson to it.
    4. Caveat: the Carleson project has sorry in some helper files under ToMathlib (rearrangement, layer cake, Lorentz interpolation); I did not trace which theorems depend on them.

    Prerequisites: carlesonOperator_eq_biSup_Θ'_J102, linearized_metric_carleson

    See also: MetricSpaceCarleson

    Sources and attribution: Pinned Lean source (8972acdfd953)

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

    Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, IsCancellative, defaultA, defaultτ, Membership.mem, Set.Ioc, OfNat.ofNat, NNReal.HolderConjugate, MeasurableSet, Measurable, LE.le, Real, Norm.norm, Set.indicator, MeasureTheory.HasBoundedStrongType and 12 more

    Proof uses: LE.le.trans, Set.indicator_le_self', of_eq_true, Not, Eq.trans, True, forall_congr, implies_congr, Eq.refl, implies_true, Trans.trans, Eq, iSup, FunctionDistances.Θ, Θ', Prod, Rat, J102, ENorm.enorm, carlesonOperatorIntegrand and 58 more

    204 instances, coercions and auxiliary constants left out.

    Tactic trace: 37 steps

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

    theorem metric_carleson [IsCancellative X (defaultτ a)]
    (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q') (mF : MeasurableSet F) (mG : MeasurableSet G)
    (mf : Measurable f) (nf : (‖f ·‖) ≤ F.indicator 1)
    (hT : HasBoundedStrongType (nontangentialOperator K · ·) 2 2 volume volume (C_Ts a)) :
    ∫⁻ x in G, carlesonOperator K f x ≤
    C1_0_2 a q * volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ := by
…

    Mentions: IsCancellative, defaultτ, mf, nontangentialOperator, K, C_Ts, carlesonOperator, C1_0_2

  17. theorem metric_carleson_check line 242 source

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

    Statement uses: MetricSpaceCarleson

    Proof uses: metric_carleson

  18. theorem metric_carleson' Theorem 1.1.1, with an explicit value for the constant, corresponding to 𝕔 = 100 and following the blueprint line 246 source

    Source comment

    Theorem 1.1.1, with an explicit value for the constant, corresponding to `𝕔 = 100` and following the blueprint. If one takes `𝕔 = 7`, one gets `2 ^ (44 * a ^ 3)` instead.

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

    Statement uses: Nat, MetricSpace, NNReal, Set, Complex, KernelProofData, IsCancellative, defaultA, defaultτ, Membership.mem, Set.Ioc, OfNat.ofNat, NNReal.HolderConjugate, MeasurableSet, Measurable, LE.le, Real, Norm.norm, Set.indicator, MeasureTheory.HasBoundedStrongType and 13 more

    Proof uses: Eq.mpr, C1_0_2, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, HMul, id, congrArg, congrFun', HAdd.hAdd, 𝕔, congr, 𝕔_def, ENNReal.coe_div, Ne and 9 more

    172 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

    theorem metric_carleson' [IsCancellative X (defaultτ a)]
    (hq : q ∈ Ioc 1 2) (hqq' : q.HolderConjugate q') (mF : MeasurableSet F) (mG : MeasurableSet G)
    (mf : Measurable f) (nf : (‖f ·‖) ≤ F.indicator 1)
    (hT : HasBoundedStrongType (nontangentialOperator K · ·) 2 2 volume volume (C_Ts a)) :
    ∫⁻ x in G, carlesonOperator K f x ≤
    (2 ^ (443 * a ^ 3) / (q - 1) ^ 6) * volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ := by
…

    Mentions: IsCancellative, defaultτ, mf, nontangentialOperator, K, C_Ts, carlesonOperator