Carleson/TwoSidedCarleson/Basic.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

8 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 3 files
  1. def czOperator The Calderon Zygmund operator T_r in chapter Two-sided Metric Space Carleson line 15 source

    Source documentation

    The Calderon Zygmund operator T_r in chapter Two-sided Metric Space Carleson

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

    Statement uses: PseudoMetricSpace, MeasureTheory.MeasureSpace, Complex, Real

    Proof uses: MeasureTheory.integral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Compl.compl, Set, Metric.ball, HMul.hMul

    9 instances, coercions and auxiliary constants left out.

    noncomputable def czOperator {X : Type*} [PseudoMetricSpace X] [MeasureSpace X] (K : X → X → ℂ)
    (r : ℝ) (f : X → ℂ) (x : X) : ℂ := ∫ y in (ball x r)ᶜ, K x y * f y

    Mentions: K

  2. lemma czOperator_bound line 18 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsOneSidedKernel, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, LT.lt, OfNat.ofNat, Exists, Filter.Eventually, LE.le, Norm.norm, HMul.hMul, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.Measure.restrict and 3 more

    Proof uses: ENNReal.toNNReal, ENNReal, HDiv.hDiv, C_K, MeasureTheory.eLpNorm, Top.top, Exists.intro, Eq.mpr, Eq, Set.ofPred, Not, id, congrArg, propext, MeasureTheory.ae_iff, Inter.inter, MeasureTheory.Measure.restrict_apply₀', MeasurableSet.nullMeasurableSet, MeasurableSet.compl, measurableSet_ball and 44 more

    123 instances, coercions and auxiliary constants left out.

    Tactic trace: 42 steps

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

  3. lemma czOperator_aestronglyMeasurable' line 56 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, Measurable, Prod, Function.uncurry, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, czOperator

    Proof uses: id, Eq.mpr, MeasureTheory.integral, MeasureTheory.Measure.restrict, Compl.compl, Set, Metric.ball, HMul.hMul, Set.indicator, Eq, Eq.rec, MeasureTheory.Measure, Eq.refl, funext, Eq.trans, congrArg, Eq.symm, MeasureTheory.integral_indicator, MeasurableSet, measurableSet_ball and 21 more

    99 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

  4. lemma czOperator_aestronglyMeasurable line 72 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsOneSidedKernel, MeasureTheory.AEStronglyMeasurable, MeasureTheory.MeasureSpace.volume, czOperator

    Proof uses: czOperator_aestronglyMeasurable', IsOneSidedKernel.measurable_K

    32 instances, coercions and auxiliary constants left out.

  5. lemma czOperator_aestronglyMeasurable_aux Next lemma is useful for fun_prop in a context where it can not find the relevant measure to apply czOperator_aestronglyMeasurable line 81 source

    Source comment

    Next lemma is useful for fun_prop in a context where it can not find the relevant measure to apply `czOperator_aestronglyMeasurable`. TODO: investigate

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsOneSidedKernel, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, MeasureTheory.AEStronglyMeasurable, czOperator

    Proof uses: czOperator_aestronglyMeasurable, BoundedFiniteSupport.aestronglyMeasurable

    48 instances, coercions and auxiliary constants left out.

    lemma czOperator_aestronglyMeasurable_aux {g : X → ℂ} (hg : BoundedFiniteSupport g) :
    AEStronglyMeasurable (fun x ↦ czOperator K r g x) :=
…

    Mentions: g, BoundedFiniteSupport, czOperator, K

  6. lemma czOperator_welldefined line 85 source

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsOneSidedKernel, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, LT.lt, OfNat.ofNat, MeasureTheory.IntegrableOn, HMul.hMul, Compl.compl, Set, Metric.ball

    Proof uses: MeasureTheory.AEStronglyMeasurable, Measurable, measurable_K_right, MeasureTheory.AEStronglyMeasurable.fun_mul, Measurable.aestronglyMeasurable, BoundedFiniteSupport.aestronglyMeasurable, Not, LE.le, Norm.norm, Membership.mem, Function.support, Mathlib.Tactic.Contrapose.contrapose₂, Eq.mpr, Eq, id, congrArg, propext, Function.notMem_support, norm_zero, of_eq_true and 39 more

    117 instances, coercions and auxiliary constants left out.

    Tactic trace: 36 steps

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

  7. lemma czOperator_sub This could be adapted to state T_r is a linear operator but maybe it's not worth the effort line 122 source

    Source comment

    This could be adapted to state T_r is a linear operator but maybe it's not worth the effort

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

    Statement uses: Nat, MetricSpace, MeasureTheory.DoublingMeasure, NNReal, defaultA, Real, Complex, IsOneSidedKernel, BoundedFiniteSupport, MeasureTheory.MeasureSpace.volume, LT.lt, OfNat.ofNat, Eq, czOperator, HSub.hSub

    Proof uses: funext, id, MeasureTheory.integral, MeasureTheory.Measure.restrict, Compl.compl, Set, Metric.ball, HMul.hMul, Eq.mpr, congrFun', congrArg, mul_sub_left_distrib, of_eq_true, Eq.trans, True, MeasureTheory.integral_sub, czOperator_welldefined, eq_self

    79 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

    lemma czOperator_sub {f g : X → ℂ} (hf : BoundedFiniteSupport f) (hg : BoundedFiniteSupport g) (hr : 0 < r) :
    czOperator K r (f - g) = czOperator K r f - czOperator K r g := by
…

    Mentions: g, BoundedFiniteSupport, czOperator, K

  8. lemma geometric_series_estimate Lemma 10.1.1 line 130 source

    Source documentation

    Lemma 10.1.1

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

    Statement uses: Real, LE.le, OfNat.ofNat, Nat, ENNReal, tsum, HPow.hPow, HDiv.hDiv, Neg.neg, SummationFilter.unconditional

    Proof uses: Trans.trans, Eq, ENNReal.ofReal, HMul.hMul, Inv.inv, HSub.hSub, eq_of_heq, AddCommMonoid, TopologicalSpace, optParam, SummationFilter, HEq, Eq.refl, HEq.refl, Eq.symm, funext, Eq.mpr, id, congrArg, div_eq_mul_inv and 98 more

    160 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

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

    lemma geometric_series_estimate {x : ℝ} (hx : 2 ≤ x) :
    ∑' (n : ℕ), (2 : ℝ≥0∞) ^ (-n / x) ≤ 2 ^ x := by
…