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

6 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 2 files
  1. def lcoConvergent A monotone sequence of functions converging to linearizedCarlesonOperator line 19 source

    Source documentation

    A monotone sequence of functions converging to linearizedCarlesonOperator.

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

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

    Proof uses: iSup, Membership.mem, Set, Set.Ioo, Inv.inv, HPow.hPow, OfNat.ofNat, ENorm.enorm, T_R

    61 instances, coercions and auxiliary constants left out.

    def lcoConvergent (n : ℕ) (x : X) : ℝ≥0∞ :=
…
  2. lemma monotone_lcoConvergent line 22 source

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

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

    Proof uses: LE.le, iSup₂_le, Membership.mem, Set, Set.Ioo, Inv.inv, HPow.hPow, OfNat.ofNat, iSup, ENorm.enorm, T_R, inv_pow_le_inv_pow_of_le, one_le_two, pow_le_pow_right₀, Set.Ioo_subset_Ioo, le_rfl, Trans.trans, id, Eq.mpr, Set.indicator and 11 more

    121 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  3. lemma iSup_lcoConvergent line 35 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real, Eq, ENNReal, iSup, lcoConvergent, linearizedCarlesonOperator

    Proof uses: funext, Eq.mpr, id, congrArg, iSup_apply, Membership.mem, Set, Set.Ioo, Inv.inv, HPow.hPow, OfNat.ofNat, ENorm.enorm, T_R, le_antisymm, LT.lt, carlesonOperatorIntegrand, iSup_le, iSup₂_le, LE.le, Set.indicator and 42 more

    163 instances, coercions and auxiliary constants left out.

    Tactic trace: 37 steps

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

  4. lemma measurable_lcoConvergent line 71 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, MeasureTheory.SimpleFunc, NNReal, defaultA, FunctionDistances.Θ, Real, Measurable, LE.le, Norm.norm, OfNat.ofNat, ENNReal, lcoConvergent

    Proof uses: measurable_of_Ioi, Set, Prod, Rat, Set.ofPred, And, LT.lt, Inv.inv, HPow.hPow, Prod.fst, Prod.snd, Eq, Set.preimage, Set.Ioi, Set.iUnion, Membership.mem, ENorm.enorm, T_R, Set.ext, Eq.mpr and 109 more

    231 instances, coercions and auxiliary constants left out.

    Tactic trace: 45 steps

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

  5. theorem linearized_metric_carleson Linearized metric Carleson theorem (Theorem 1.1.2) line 109 source

    Source documentation

    Theorem 1.1.2

    L4DEL explanation

    For a fixed phase choice Q, truncate the radii in an increasing family, bound each truncation, and pass to the limit by monotone convergence.

    1. Write the integral over G of the linearized operator as an increasing supremum over n of the integrals of the n-th truncation lcoConvergent.
    2. Exchange the integral and the supremum by monotone convergence (lintegral_iSup).
    3. Bound each truncated integral by the lemma R_truncation, using the L2 bound for the nontangential operators.

    Prerequisites: lcoConvergent, R_truncation

    See also: LinearizedMetricCarleson, metric_carleson

    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, MeasureTheory.SimpleFunc, defaultA, FunctionDistances.Θ, Real, IsCancellative, defaultτ, Membership.mem, Set.Ioc, OfNat.ofNat, NNReal.HolderConjugate, MeasurableSet, Measurable, LE.le, Norm.norm and 14 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, lcoConvergent, Eq.mpr, id, congrArg, Eq.symm, MeasureTheory.lintegral_indicator, eq_of_heq and 22 more

    177 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

    theorem linearized_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 : ∀ θ : Θ X, HasBoundedStrongType (linearizedNontangentialOperator Q θ K · ·)
      2 2 volume volume (C_Ts a)) :
    ∫⁻ x in G, linearizedCarlesonOperator Q K f x ≤
    C1_0_2 a q * volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ := by
…

    Mentions: IsCancellative, defaultτ, mf, linearizedNontangentialOperator, K, C_Ts, linearizedCarlesonOperator, C1_0_2

  6. theorem linearized_metric_carleson_check line 130 source

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

    Statement uses: LinearizedMetricCarleson

    Proof uses: linearized_metric_carleson