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

37 declarations, 0 contain sorry, 0 declared as axioms

The following two lemmas state that the distance could be equivalently given by any other cdist.

Imports (3)
Imported by 2 files
  1. instance MetricΘ.(instance at line 23) line 23 source

    Source documentation

    We choose as metric space instance on Θ one given by an arbitrary ball. The metric given by all other balls are equivalent.

    instance : PseudoMetricSpace (Θ X) :=
…
  2. lemma MetricΘ.dist_eq_cdist line 26 source

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

    Statement uses: Nat, MetricSpace, CompatibleFunctions, Real, defaultA, FunctionDistances.Θ, Eq, Dist.dist, WithFunctionDistance, cancelPt, OfNat.ofNat

    Proof uses: rfl

    21 instances, coercions and auxiliary constants left out.

  3. lemma MetricΘ.dist_le_cdist line 32 source

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

    Statement uses: Nat, MetricSpace, CompatibleFunctions, Real, defaultA, FunctionDistances.Θ, LT.lt, OfNat.ofNat, LE.le, Dist.dist, HMul.hMul, As, NNReal, HDiv.hDiv, HAdd.hAdd, cancelPt, WithFunctionDistance

    Proof uses: cdist_le_mul_cdist, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Nat.cast_one, Eq.refl, Bool, Bool.false

    53 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. lemma MetricΘ.cdist_le_dist line 36 source

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

    Statement uses: Nat, MetricSpace, CompatibleFunctions, Real, defaultA, FunctionDistances.Θ, LT.lt, OfNat.ofNat, LE.le, Dist.dist, WithFunctionDistance, HMul.hMul, As, NNReal, HAdd.hAdd, cancelPt

    Proof uses: Eq.mpr, HDiv.hDiv, id, Eq, congrArg, Eq.symm, div_one, dist_comm, cdist_le_mul_cdist, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Nat.cast_one, Eq.refl, Bool, Bool.false

    73 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  5. instance MetricΘ.(instance at line 41) line 41 source
  6. theorem carlesonOperator_zero line 51 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Eq, ENNReal, carlesonOperator, defaultA, Real, OfNat.ofNat

    Proof uses: id, iSup, FunctionDistances.Θ, linearizedCarlesonOperator, LT.lt, ENorm.enorm, carlesonOperatorIntegrand, Eq.mpr, MeasureTheory.integral, NNReal, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Annulus.oo, HMul.hMul, Complex.exp, Complex.I, congrFun', congrArg, funext, Eq.trans and 9 more

    73 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  7. theorem carlesonOperatorIntegrand_congr_ae line 56 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, FunctionDistances.Θ, Real, Eq, carlesonOperatorIntegrand

    Proof uses: id, MeasureTheory.integral_congr_ae, MeasureTheory.Measure.restrict, Set.Annulus.oo, HMul.hMul, Complex.exp, Complex.I, MeasureTheory.ae_restrict_le, Set.ofPred, Filter.mp_mem, Filter.univ_mem', Membership.mem, Set, HMul, Eq.rec, Eq.refl

    49 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  8. theorem linearizedCarlesonOperator_congr_ae line 65 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, FunctionDistances.Θ, Real, Eq, ENNReal, linearizedCarlesonOperator

    Proof uses: id, SupSet, Eq.rec, iSup, Eq.refl, LT.lt, OfNat.ofNat, ENorm.enorm, carlesonOperatorIntegrand, funext, ENorm, carlesonOperatorIntegrand_congr_ae

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  9. theorem carlesonOperator_congr_ae line 76 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, Eq, ENNReal, carlesonOperator, Real

    Proof uses: funext, id, SupSet, Eq.rec, iSup, Eq.refl, FunctionDistances.Θ, linearizedCarlesonOperator, linearizedCarlesonOperator_congr_ae

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  10. theorem carlesonOperator_zero_of_ae_zero line 83 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, Eq, ENNReal, carlesonOperator, Real

    Proof uses: Eq.mpr, id, congrArg, carlesonOperator_congr_ae, of_eq_true, Eq.trans, True, congrFun', carlesonOperator_zero, eq_self

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  11. lemma measurable_carlesonOperatorIntegrand line 89 source

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

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

    Proof uses: id, Eq.mpr, MeasureTheory.integral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Annulus.oo, HMul.hMul, Complex.exp, Complex.I, MeasureTheory.StronglyMeasurable, Eq, congrArg, Eq.symm, propext, stronglyMeasurable_iff_measurable, Set.indicator, Eq.rec, Eq.refl, funext, Eq.trans and 23 more

    107 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  12. lemma rightContinuous_integral_annulus Let f be integrable over an annulus with fixed radii R₁, R₂ line 102 source

    Source documentation

    Let f be integrable over an annulus with fixed radii R₁, R₂. Then fun R ↦ ∫ y in oo x R R₂, f y is right-continuous at R₁.

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Real, MeasureTheory.IntegrableOn, NNReal, defaultA, Set.Annulus.oo, MeasureTheory.MeasureSpace.volume, ContinuousWithinAt, MeasureTheory.integral, MeasureTheory.Measure.restrict, Set.Ici

    Proof uses: LE.le, LT.lt, Or, le_or_gt, Eq.mpr, GT.gt, OfNat.ofNat, Exists, And, Membership.mem, Set, Dist.dist, id, Eq, forall_congr, implies_congr, Eq.refl, congrArg, funext, Exists.intro and 173 more

    238 instances, coercions and auxiliary constants left out.

    Tactic trace: 107 steps

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

    lemma rightContinuous_integral_annulus (iof : IntegrableOn f (oo x R₁ R₂)) :
    ContinuousWithinAt (fun R ↦ ∫ y in oo x R R₂, f y) (Ici R₁) R₁ := by
…
  13. lemma leftContinuous_integral_annulus Let f be integrable over an annulus with fixed radii R₁, R₂ line 185 source

    Source documentation

    Let f be integrable over an annulus with fixed radii R₁, R₂. Then fun R ↦ ∫ y in oo x R₁ R, f y is left-continuous at R₂.

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Real, MeasureTheory.IntegrableOn, NNReal, defaultA, Set.Annulus.oo, MeasureTheory.MeasureSpace.volume, ContinuousWithinAt, MeasureTheory.integral, MeasureTheory.Measure.restrict, Set.Iic

    Proof uses: LE.le, LT.lt, Or, le_or_gt, Eq.mpr, GT.gt, OfNat.ofNat, Exists, And, Membership.mem, Set, Dist.dist, id, Eq, forall_congr, implies_congr, Eq.refl, congrArg, funext, Exists.intro and 172 more

    240 instances, coercions and auxiliary constants left out.

    Tactic trace: 108 steps

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

    lemma leftContinuous_integral_annulus (iof : IntegrableOn f (oo x R₁ R₂)) :
    ContinuousWithinAt (fun R ↦ ∫ y in oo x R₁ R, f y) (Iic R₂) R₂ := by
…
  14. lemma integrableOn_annulus_of_bounded line 265 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Real, MeasureTheory.AEStronglyMeasurable, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, LE.le, Norm.norm, OfNat.ofNat, MeasureTheory.IntegrableOn, Set.Annulus.oo

    Proof uses: Ne, ENNReal, MeasureTheory.Measure, Set, Top.top, MeasureTheory.Measure.integrableOn_of_bounded, Eq.mpr, LT.lt, id, Eq, congrArg, Eq.symm, propext, lt_top_iff_ne_top, Trans.trans, Metric.ball, MeasureTheory.measure_mono, Membership.mem, Dist.dist, Metric.mem_ball' and 12 more

    82 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  15. lemma integrableOn_coi_inner_annulus' The integrand of carlesonOperatorIntegrand is integrable over the R₁, R₂ annulus line 279 source

    Source documentation

    The integrand of carlesonOperatorIntegrand is integrable over the R₁, R₂ annulus.

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, FunctionDistances.Θ, Real, defaultA, MeasureTheory.IntegrableOn, NNReal, Set.Annulus.oo, MeasureTheory.MeasureSpace.volume, LT.lt, OfNat.ofNat, HMul.hMul, Complex.exp, Complex.I

    Proof uses: Eq.mpr, id, Eq, congrFun', MeasureTheory.Measure, Set, autoParam, congrArg, funext, mul_assoc, integrableOn_K_mul, MeasurableSpace, TopologicalSpace, ContinuousENorm, Eq.rec, Eq.refl, Eq.trans, mul_comm, MeasureTheory.Integrable, MeasureTheory.Measure.restrict and 33 more

    131 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

    lemma integrableOn_coi_inner_annulus' (nf : IntegrableOn f (Annulus.oo x R₁ R₂)) (hR₁ : 0 < R₁) :
    IntegrableOn (fun y ↦ K x y * f y * exp (I * θ y)) (Annulus.oo x R₁ R₂) := by
…

    Mentions: K

  16. lemma integrableOn_coi_inner_annulus₀ The integrand of carlesonOperatorIntegrand is integrable over the R₁, R₂ annulus line 292 source

    Source documentation

    The integrand of carlesonOperatorIntegrand is integrable over the R₁, R₂ annulus.

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, FunctionDistances.Θ, Real, defaultA, MeasureTheory.AEStronglyMeasurable, NNReal, MeasureTheory.MeasureSpace.volume, LE.le, Norm.norm, OfNat.ofNat, LT.lt, MeasureTheory.IntegrableOn, HMul.hMul, Complex.exp, Complex.I, Set.Annulus.oo

    Proof uses: integrableOn_coi_inner_annulus', integrableOn_annulus_of_bounded

    72 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

    lemma integrableOn_coi_inner_annulus₀ (mf : AEStronglyMeasurable f volume) (nf : (‖f ·‖) ≤ 1) (hR₁ : 0 < R₁) :
    IntegrableOn (fun y ↦ K x y * f y * exp (I * θ y)) (Annulus.oo x R₁ R₂) := by
…

    Mentions: mf, K

  17. lemma integrableOn_coi_inner_annulus The integrand of carlesonOperatorIntegrand is integrable over the R₁, R₂ annulus line 300 source

    Source documentation

    The integrand of carlesonOperatorIntegrand is integrable over the R₁, R₂ annulus.

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, FunctionDistances.Θ, Real, defaultA, Measurable, NNReal, LE.le, Norm.norm, OfNat.ofNat, LT.lt, MeasureTheory.IntegrableOn, HMul.hMul, Complex.exp, Complex.I, Set.Annulus.oo, MeasureTheory.MeasureSpace.volume

    Proof uses: integrableOn_coi_inner_annulus₀, Measurable.aestronglyMeasurable

    82 instances, coercions and auxiliary constants left out.

    lemma integrableOn_coi_inner_annulus (mf : Measurable f) (nf : (‖f ·‖) ≤ 1) (hR₁ : 0 < R₁) :
    IntegrableOn (fun y ↦ K x y * f y * exp (I * θ y)) (Annulus.oo x R₁ R₂) :=
…

    Mentions: mf, K

  18. lemma rightContinuous_carlesonOperatorIntegrand' line 304 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, FunctionDistances.Θ, Real, defaultA, MeasureTheory.IntegrableOn, NNReal, Set.Annulus.oo, MeasureTheory.MeasureSpace.volume, LT.lt, OfNat.ofNat, ContinuousWithinAt, carlesonOperatorIntegrand, Set.Ici

    Proof uses: rightContinuous_integral_annulus, HMul.hMul, Complex.exp, Complex.I, integrableOn_coi_inner_annulus'

    68 instances, coercions and auxiliary constants left out.

  19. lemma rightContinuous_carlesonOperatorIntegrand line 309 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, FunctionDistances.Θ, Real, defaultA, Measurable, NNReal, LE.le, Norm.norm, OfNat.ofNat, LT.lt, ContinuousWithinAt, carlesonOperatorIntegrand, Set.Ici

    Proof uses: rightContinuous_carlesonOperatorIntegrand', integrableOn_annulus_of_bounded, Measurable.aestronglyMeasurable, MeasureTheory.MeasureSpace.volume

    74 instances, coercions and auxiliary constants left out.

  20. lemma leftContinuous_carlesonOperatorIntegrand' line 315 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, FunctionDistances.Θ, Real, defaultA, MeasureTheory.IntegrableOn, NNReal, Set.Annulus.oo, MeasureTheory.MeasureSpace.volume, LT.lt, OfNat.ofNat, ContinuousWithinAt, carlesonOperatorIntegrand, Set.Iic

    Proof uses: leftContinuous_integral_annulus, HMul.hMul, Complex.exp, Complex.I, integrableOn_coi_inner_annulus'

    68 instances, coercions and auxiliary constants left out.

  21. lemma leftContinuous_carlesonOperatorIntegrand line 320 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, FunctionDistances.Θ, Real, defaultA, Measurable, NNReal, LE.le, Norm.norm, OfNat.ofNat, LT.lt, ContinuousWithinAt, carlesonOperatorIntegrand, Set.Iic

    Proof uses: leftContinuous_carlesonOperatorIntegrand', integrableOn_annulus_of_bounded, Measurable.aestronglyMeasurable, MeasureTheory.MeasureSpace.volume

    74 instances, coercions and auxiliary constants left out.

  22. lemma exists_rat_near_carlesonOperatorIntegrand' Given 0 < R₁ < R₂, move (R₁, R₂) to rational (q₁, q₂) where R₁ < q₁ < q₂ < R₂ and the norm of carlesonOperatorIntegrand changes by at most ε line 330 source

    Source documentation

    Given 0 < R₁ < R₂, move (R₁, R₂) to rational (q₁, q₂) where R₁ < q₁ < q₂ < R₂ and the norm of carlesonOperatorIntegrand changes by at most ε.

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, FunctionDistances.Θ, Real, defaultA, MeasureTheory.IntegrableOn, NNReal, Set.Annulus.oo, MeasureTheory.MeasureSpace.volume, LT.lt, OfNat.ofNat, Exists, Rat, And, Dist.dist, carlesonOperatorIntegrand

    Proof uses: ContinuousWithinAt, Set.Ici, rightContinuous_carlesonOperatorIntegrand', GT.gt, Membership.mem, Set, HDiv.hDiv, Eq.mp, congrArg, propext, Metric.continuousWithinAt_iff, half_pos, Min.min, HAdd.hAdd, Eq.mpr, id, Eq, lt_min_iff, And.intro, lt_of_not_ge and 71 more

    175 instances, coercions and auxiliary constants left out.

    Tactic trace: 33 steps

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

    lemma exists_rat_near_carlesonOperatorIntegrand'
    (mf : IntegrableOn f (Annulus.oo x R₁ R₂) volume) (hR₁ : 0 < R₁) (hR₂ : R₁ < R₂) {ε : ℝ} (εpos : 0 < ε) :
    ∃ q₁ q₂ : ℚ, R₁ < q₁ ∧ q₁ < q₂ ∧ q₂ < R₂ ∧
    dist (carlesonOperatorIntegrand K θ q₁ q₂ f x)
    (carlesonOperatorIntegrand K θ R₁ R₂ f x) < ε := by
…

    Mentions: mf, carlesonOperatorIntegrand, K

  23. lemma exists_rat_near_carlesonOperatorIntegrand Given 0 < R₁ < R₂, move (R₁, R₂) to rational (q₁, q₂) where R₁ < q₁ < q₂ < R₂ and the norm of carlesonOperatorIntegrand changes by at most ε line 363 source

    Source documentation

    Given 0 < R₁ < R₂, move (R₁, R₂) to rational (q₁, q₂) where R₁ < q₁ < q₂ < R₂ and the norm of carlesonOperatorIntegrand changes by at most ε.

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, FunctionDistances.Θ, Real, defaultA, Measurable, NNReal, LE.le, Norm.norm, OfNat.ofNat, LT.lt, Exists, Rat, And, Dist.dist, carlesonOperatorIntegrand

    Proof uses: exists_rat_near_carlesonOperatorIntegrand', integrableOn_annulus_of_bounded, Measurable.aestronglyMeasurable, MeasureTheory.MeasureSpace.volume

    76 instances, coercions and auxiliary constants left out.

    lemma exists_rat_near_carlesonOperatorIntegrand
    (mf : Measurable f) (nf : (‖f ·‖) ≤ 1) (hR₁ : 0 < R₁) (hR₂ : R₁ < R₂) {ε : ℝ} (εpos : 0 < ε) :
    ∃ q₁ q₂ : ℚ, R₁ < q₁ ∧ q₁ < q₂ ∧ q₂ < R₂ ∧
    dist (carlesonOperatorIntegrand K θ q₁ q₂ f x)
    (carlesonOperatorIntegrand K θ R₁ R₂ f x) < ε :=
…

    Mentions: mf, carlesonOperatorIntegrand, K

  24. lemma lintegral_inv_vol_le line 375 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, NNReal, LT.lt, OfNat.ofNat, LE.le, ENNReal, MeasureTheory.lintegral, defaultA, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Annulus.oo, Inv.inv, vol, HPow.hPow, HDiv.hDiv, HMul.hMul

    Proof uses: Membership.mem, Set, MeasureTheory.Measure, Metric.ball, And, Real, Dist.dist, Exists, Eq.mpr, id, Eq, congrArg, propext, one_le_div, LT.lt.le, HAdd.hAdd, exists_nat_pow_near, one_lt_two, Exists.intro, And.intro and 64 more

    191 instances, coercions and auxiliary constants left out.

    Tactic trace: 38 steps

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

  25. lemma edist_carlesonOperatorIntegrand_le line 404 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, FunctionDistances.Θ, Real, defaultA, NNReal, Measurable, LE.le, Norm.norm, OfNat.ofNat, LT.lt, ENNReal, EDist.edist, carlesonOperatorIntegrand, HMul.hMul, C3_0_1, WithFunctionDistance, HAdd.hAdd and 2 more

    Proof uses: Or, le_or_gt, Eq.mpr, MeasureTheory.integral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Annulus.oo, Complex.exp, Complex.I, id, Eq, congrArg, carlesonOperatorIntegrand.eq_1, EmptyCollection.emptyCollection, Set, Set.Annulus.oo_eq_empty, of_eq_true, Eq.trans, True, eq_true and 89 more

    267 instances, coercions and auxiliary constants left out.

    Tactic trace: 47 steps

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

  26. lemma dist_carlesonOperatorIntegrand_le line 448 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, FunctionDistances.Θ, Real, defaultA, NNReal, Measurable, LE.le, Norm.norm, OfNat.ofNat, LT.lt, Dist.dist, carlesonOperatorIntegrand, HMul.hMul, C3_0_1, WithFunctionDistance, HAdd.hAdd, cancelPt

    Proof uses: Eq.mpr, ENNReal, ENNReal.ofReal, id, Eq, congrArg, Eq.symm, propext, ENNReal.ofReal_le_ofReal_iff, mul_nonneg, NNReal.coe_nonneg, dist_nonneg, EDist.edist, edist_dist, ENNReal.ofReal_mul, NNReal.zero_le_coe, ENNReal.ofReal_coe_nnreal, edist_carlesonOperatorIntegrand_le

    94 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  27. lemma continuous_carlesonOperatorIntegrand line 456 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Real, Measurable, NNReal, defaultA, LE.le, Norm.norm, OfNat.ofNat, LT.lt, Continuous, FunctionDistances.Θ, carlesonOperatorIntegrand

    Proof uses: Or, le_or_gt, id, Eq.mpr, MeasureTheory.integral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Annulus.oo, HMul.hMul, Complex.exp, Complex.I, EmptyCollection.emptyCollection, Set, Eq, congrArg, Set.Annulus.oo_eq_empty, funext, MeasureTheory.setIntegral_empty, continuous_const, Exists and 47 more

    186 instances, coercions and auxiliary constants left out.

    Tactic trace: 31 steps

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

  28. lemma enorm_carlesonOperatorIntegrand_le not sure if this is the best phrasing line 476 source

    Source comment

    not sure if this is the best phrasing

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, FunctionDistances.Θ, Real, defaultA, NNReal, LE.le, Norm.norm, OfNat.ofNat, LT.lt, ENNReal, ENorm.enorm, carlesonOperatorIntegrand, C3_0_1

    Proof uses: Or, le_or_gt, id, Eq.mpr, MeasureTheory.integral, MeasureTheory.Measure.restrict, MeasureTheory.MeasureSpace.volume, Set.Annulus.oo, HMul.hMul, Complex.exp, Complex.I, EmptyCollection.emptyCollection, Set, Eq, congrArg, Set.Annulus.oo_eq_empty, of_eq_true, Eq.trans, True, eq_true and 35 more

    177 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

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

    lemma enorm_carlesonOperatorIntegrand_le {R₁ R₂ : ℝ≥0} (nf : (‖f ·‖) ≤ 1) (hR₁ : 0 < R₁) :
    ‖carlesonOperatorIntegrand K θ R₁ R₂ f x‖ₑ ≤ C3_0_1 a R₁ R₂ := by
…

    Mentions: carlesonOperatorIntegrand, K

  29. theorem carlesonOperatorIntegrand_measurable line 494 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Real, FunctionDistances.Θ, defaultA, MeasureTheory.AEStronglyMeasurable, NNReal, MeasureTheory.MeasureSpace.volume, Measurable, carlesonOperatorIntegrand

    Proof uses: id, MeasureTheory.AEStronglyMeasurable.induction, MeasureTheory.integral, MeasureTheory.Measure.restrict, Set.Annulus.oo, HMul.hMul, Complex.exp, Complex.I, MeasureTheory.StronglyMeasurable, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure, Eq, MeasureTheory.integral_congr_ae, MeasureTheory.ae_restrict_le, Set.ofPred, Eq.mpr, Membership.mem, Set, Filter and 41 more

    126 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

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

  30. theorem linearizedCarlesonOperator_measurable line 517 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, FunctionDistances.Θ, Real, defaultA, MeasureTheory.LocallyIntegrable, NNReal, MeasureTheory.MeasureSpace.volume, Measurable, ENNReal, linearizedCarlesonOperator

    Proof uses: id, Eq, iSup, LT.lt, OfNat.ofNat, ENorm.enorm, carlesonOperatorIntegrand, Rat, le_antisymm, le_of_forall_lt_imp_le_of_dense, Exists, LE.le, Eq.mp, congrArg, propext, lt_iSup_iff, HSub.hSub, Norm.norm, ENNReal.toReal, sub_pos_of_lt and 51 more

    163 instances, coercions and auxiliary constants left out.

    Tactic trace: 61 steps

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

  31. theorem carlesonOperator_measurable TODO: get rid of the countability assumption line 580 source

    Source comment

    TODO: get rid of the countability assumption

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, MeasureTheory.LocallyIntegrable, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, Countable, FunctionDistances.Θ, Real, Measurable, ENNReal, carlesonOperator

    Proof uses: id, Measurable.iSup, linearizedCarlesonOperator, linearizedCarlesonOperator_measurable

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

    theorem carlesonOperator_measurable (hf : LocallyIntegrable f) [Countable (Θ X)] :
    Measurable (carlesonOperator K f) := by
…

    Mentions: carlesonOperator, K

  32. theorem enorm_carlesonOperatorIntegrand_add_le_add_enorm_carlesonOperatorIntegrand line 585 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, MeasureTheory.LocallyIntegrable, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, FunctionDistances.Θ, Real, LT.lt, OfNat.ofNat, LE.le, ENNReal, ENorm.enorm, carlesonOperatorIntegrand, HAdd.hAdd

    Proof uses: id, le_trans, MeasureTheory.integral, MeasureTheory.Measure.restrict, Set.Annulus.oo, HMul.hMul, Complex.exp, Complex.I, Eq.mpr, Eq, congrArg, Eq.symm, MeasureTheory.integral_add, integrableOn_coi_inner_annulus', MeasureTheory.IntegrableOn.mono_set, Metric.ball, Metric.closedBall, MeasureTheory.LocallyIntegrable.integrableOn_isCompact, ProperSpace.isCompact_closedBall, Metric.ball_subset_closedBall and 30 more

    117 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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

  33. theorem linearizedCarlesonOperator_add_le_add_linearizedCarlesonOperator TODO: this proof is a good target for automation line 607 source

    Source comment

    TODO: this proof is a good target for automation

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, MeasureTheory.LocallyIntegrable, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, FunctionDistances.Θ, Real, LE.le, ENNReal, linearizedCarlesonOperator, HAdd.hAdd

    Proof uses: id, le_trans, iSup, LT.lt, OfNat.ofNat, ENorm.enorm, carlesonOperatorIntegrand, iSup_mono, enorm_carlesonOperatorIntegrand_add_le_add_enorm_carlesonOperatorIntegrand, iSup_add_le

    90 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

    theorem linearizedCarlesonOperator_add_le_add_linearizedCarlesonOperator
  {f g : X → ℂ} (hf : LocallyIntegrable f) (hg : LocallyIntegrable g) {θ : Θ X} :
  linearizedCarlesonOperator (fun _ ↦ θ) K (f + g) x ≤
    linearizedCarlesonOperator (fun _ ↦ θ) K f x + linearizedCarlesonOperator (fun _ ↦ θ) K g x := by
…

    Mentions: g, linearizedCarlesonOperator, K

  34. theorem carlesonOperator_add_le_add_carlesonOperator line 623 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, MeasureTheory.LocallyIntegrable, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, LE.le, ENNReal, carlesonOperator, Real, HAdd.hAdd

    Proof uses: id, le_trans, iSup, FunctionDistances.Θ, linearizedCarlesonOperator, iSup_mono, linearizedCarlesonOperator_add_le_add_linearizedCarlesonOperator, iSup_add_le

    82 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  35. lemma tendsto_carlesonOperatorIntegrand_of_dominated_convergence line 631 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, FunctionDistances.Θ, Real, defaultA, LT.lt, OfNat.ofNat, Filter, Filter.IsCountablyGenerated, Filter.Eventually, MeasureTheory.AEStronglyMeasurable, NNReal, MeasureTheory.MeasureSpace.volume, LE.le, Norm.norm, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.IntegrableOn and 4 more

    Proof uses: id, HMul.hMul, Complex.exp, Complex.I, MeasureTheory.tendsto_integral_filter_of_dominated_convergence, MeasureTheory.Measure.restrict, Filter.Eventually.mp, Measurable, measurable_K_right, Filter.univ_mem', Set.ofPred, Membership.mem, Set, MeasureTheory.AEStronglyMeasurable.fun_mul, Measurable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.restrict, Continuous.comp_aestronglyMeasurable, Continuous.cexp, continuous_id', MeasureTheory.AEStronglyMeasurable.const_mul and 26 more

    128 instances, coercions and auxiliary constants left out.

    Tactic trace: 25 steps

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

  36. lemma linearizedCarlesonOperator_le_liminf_linearizedCarlesonOperator_of_tendsto line 664 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, FunctionDistances.Θ, Real, defaultA, Filter, Filter.IsCountablyGenerated, Filter.NeBot, Filter.Eventually, MeasureTheory.AEStronglyMeasurable, NNReal, MeasureTheory.MeasureSpace.volume, LE.le, Norm.norm, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.LocallyIntegrable, Filter.Tendsto and 4 more

    Proof uses: id, le_trans, iSup, LT.lt, OfNat.ofNat, ENorm.enorm, carlesonOperatorIntegrand, iSup_mono, Eq.mpr, Eq, Eq.trans, implies_congr, Eq.refl, congrArg, congrFun', funext, CompleteLattice, iSup_pos, le_of_eq, Eq.symm and 12 more

    104 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

  37. lemma carlesonOperator_le_liminf_carlesonOperator_of_tendsto line 691 source

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

    Statement uses: Nat, MetricSpace, Complex, KernelProofData, Filter, Filter.IsCountablyGenerated, Filter.NeBot, Real, Filter.Eventually, MeasureTheory.AEStronglyMeasurable, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, LE.le, Norm.norm, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.LocallyIntegrable, Filter.Tendsto, nhds and 3 more

    Proof uses: id, le_trans, iSup, FunctionDistances.Θ, linearizedCarlesonOperator, iSup_mono, linearizedCarlesonOperator_le_liminf_linearizedCarlesonOperator_of_tendsto, Filter.iSup_liminf_le_liminf_iSup

    82 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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