Carleson/Psi.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

76 declarations, 0 contain sorry, 0 declared as axioms

The function ψ

Imports (1)
Imported by 2 files
  1. lemma D0 line 23 source
  2. lemma D2 line 24 source
  3. lemma cDx0 line 25 source
  4. def ψ The function ψ used as a basis for a dyadic partition of unity line 29 source

    Source documentation

    The function ψ used as a basis for a dyadic partition of unity.

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

    Statement uses: Nat, Real

    Proof uses: Max.max, OfNat.ofNat, Min.min, HSub.hSub, HMul.hMul

    15 instances, coercions and auxiliary constants left out.

    def ψ (D : ℕ) (x : ℝ) : ℝ :=
…
  5. lemma zero_le_ψ line 36 source

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

    Statement uses: Nat, Real, LE.le, OfNat.ofNat, ψ

    Proof uses: le_max_left, Min.min, HSub.hSub, HMul.hMul

    18 instances, coercions and auxiliary constants left out.

  6. lemma ψ_le_one line 39 source

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

    Statement uses: Nat, Real, LE.le, ψ, OfNat.ofNat

    Proof uses: max_le, Min.min, HSub.hSub, HMul.hMul, LT.lt.le, one_pos, min_le_left

    29 instances, coercions and auxiliary constants left out.

  7. lemma abs_ψ_le_one line 42 source

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

    Statement uses: Nat, Real, LE.le, abs, ψ, OfNat.ofNat

    Proof uses: Iff.mpr, And, Neg.neg, abs_le, And.intro, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring and 43 more

    63 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  8. lemma enorm_ψ_le_one line 45 source

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

    Statement uses: Nat, Real, LE.le, ENNReal, ENorm.enorm, ψ, OfNat.ofNat

    Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, enorm_one, Real.enorm_le_enorm, zero_le_ψ, ψ_le_one

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  9. lemma ψ_formula₀ line 51 source

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

    Statement uses: Nat, Real, LE.le, HDiv.hDiv, OfNat.ofNat, HMul.hMul, Eq, ψ

    Proof uses: dite, of_eq_true, Eq.trans, True, congrFun', congrArg, Max.max, Min.min, HSub.hSub, Neg.neg, CharP.cast_eq_zero, MulZeroClass.mul_zero, MulZeroClass.zero_mul, zero_sub, inf_of_le_right, Or, HAdd.hAdd, congr, true_or, sup_of_le_left and 18 more

    112 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  10. lemma ψ_formula₁ line 59 source

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

    Statement uses: Nat, LT.lt, Real, OfNat.ofNat, And, LE.le, HDiv.hDiv, HMul.hMul, Eq, ψ, HSub.hSub

    Proof uses: GE.ge, le_trans, Iff.mpr, one_div_nonneg, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos and 72 more

    120 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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

  11. lemma ψ_formula₂ line 72 source

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

    Statement uses: Nat, LT.lt, Real, OfNat.ofNat, And, LE.le, HDiv.hDiv, HMul.hMul, Eq, ψ

    Proof uses: id, Min.min, HSub.hSub, Iff.mp, div_le_iff₀', lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr and 80 more

    113 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  12. lemma ψ_formula₃ line 79 source

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

    Statement uses: Nat, LT.lt, Real, OfNat.ofNat, And, LE.le, HDiv.hDiv, Eq, ψ, HSub.hSub, HMul.hMul

    Proof uses: le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 73 more

    125 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  13. lemma ψ_formula₄ line 85 source

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

    Statement uses: Nat, Real, GE.ge, HDiv.hDiv, OfNat.ofNat, Eq, ψ

    Proof uses: max_eq_left, Min.min, HSub.hSub, HMul.hMul, LE.le.trans, min_le_right, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, HPow.hPow, Int.rawCast and 67 more

    99 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  14. lemma psi_zero line 89 source

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

    Statement uses: Nat, Eq, Real, ψ, OfNat.ofNat

    Proof uses: ψ_formula₀, Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg, HMul.hMul, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, mul_nonneg, le_of_lt, Mathlib.Meta.NormNum.instAtLeastTwo, Nat.cast_nonneg'

    41 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  15. lemma continuous_ψ line 91 source

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

    Statement uses: Nat, Continuous, Real, ψ

    Proof uses: id, Continuous.sup, OfNat.ofNat, Min.min, HSub.hSub, HMul.hMul, continuous_const, Continuous.inf, Continuous.fun_sub, Continuous.const_mul, continuous_id'

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  16. lemma support_ψ line 95 source

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

    Statement uses: Nat, LT.lt, Real, OfNat.ofNat, Eq, Set, Function.support, ψ, Set.Ioo, Inv.inv, HMul.hMul

    Proof uses: Set.ext, dite, Iff, Membership.mem, LE.le, HDiv.hDiv, Eq.mp, congrArg, mul_inv_rev, one_div, of_eq_true, Eq.trans, Not, And, True, False, congr, Ne, congrFun', ψ_formula₀ and 120 more

    167 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

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

  17. lemma lipschitzWith_ψ line 114 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, LipschitzWith, Real, HMul.hMul, NNReal, ψ

    Proof uses: Eq, Max.max, max_eq_right, le_of_lt, mul_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, Iff.mpr, LT.lt, Nat.cast_pos', lt_of_lt_of_le, inferInstance, PartialOrder, Zero, max_eq_left, le_of_not_gt and 82 more

    161 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

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

  18. lemma lipschitzWith_ψ' Alternate version of lipschitzWith_ψ that avoids using ENNReal line 135 source

    Source comment

    Alternate version of `lipschitzWith_ψ` that avoids using `ENNReal`.

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

    Statement uses: Nat, LE.le, OfNat.ofNat, Real, Norm.norm, HSub.hSub, ψ, HMul.hMul, Dist.dist

    Proof uses: ENNReal, EDist.edist, NNReal, lipschitzWith_ψ, Eq.mpr, id, Eq, congrArg, congrFun', Eq.mp, ENNReal.toReal, ENNReal.ofReal, ENNReal.toReal_ofReal, mul_nonneg, le_of_lt, Iff.mpr, LT.lt, Nat.cast_pos', mul_pos, inferInstance and 18 more

    105 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

    lemma lipschitzWith_ψ' (hD : 1 ≤ D) (a b : ℝ) : ‖ψ D a - ψ D b‖ ≤ 4 * D * dist a b := by
…

    Mentions: ψ

  19. def nonzeroS the one or two numbers s where ψ (D ^ (-s) * x) is possibly nonzero line 146 source

    Source documentation

    the one or two numbers s where ψ (D ^ (-s) * x) is possibly nonzero

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

    Statement uses: Nat, Real, Finset, Int

    Proof uses: Finset.Icc, Int.floor, HAdd.hAdd, OfNat.ofNat, Real.logb, HMul.hMul, Int.ceil

    21 instances, coercions and auxiliary constants left out.

    def nonzeroS (x : ℝ) : Finset ℤ :=
…
  20. lemma le_div_ceil_mul line 163 source
  21. lemma one_add_logb line 173 source
  22. lemma eq_endpoints If D ^ (-⌈logb D (4 * x)⌉) ≥ 1 / (2 * D * x), then the endpoints of nonzeroS x are equal line 178 source

    Source comment

    If `D ^ (-⌈logb D (4 * x)⌉) ≥ 1 / (2 * D * x)`, then the endpoints of `nonzeroS x` are equal.
    private lemma eq_endpoints (hx : 0 < x) (h : D ^ (-⌈logb D (4 * x)⌉) ≥ 1 / (2 * D * x)) :
    ⌊(1 + logb D (2 * x))⌋ = ⌈logb D (4 * x)⌉ := by
…
  23. lemma endpoint_sub_one If D ^ (-⌈logb D (4 * x)⌉) < 1 / (2 * D * x), then the endpoints of nonzeroS x differ by 1 line 195 source

    Source comment

    If `D ^ (-⌈logb D (4 * x)⌉) < 1 / (2 * D * x)`, then the endpoints of `nonzeroS x` differ by 1.
    private lemma endpoint_sub_one (hx : 0 < x) (h : D ^ (-⌈logb D (4 * x)⌉) < 1 / (2 * D * x)) :
    ⌊1 + logb D (2 * x)⌋ = ⌈logb D (4 * x)⌉ - 1 := by
…
  24. lemma sum_ψ₁ Special case of sum_ψ, for the case where nonzeroS D x has one element line 210 source

    Source comment

    Special case of `sum_ψ`, for the case where `nonzeroS D x` has one element.
    private lemma sum_ψ₁ (hx : 0 < x) (h : D ^ (-⌈logb D (4 * x)⌉) ≥ 1 / (2 * D * x)) :
    ∑ s ∈ nonzeroS D x, ψ D (D ^ (-s) * x) = 1 := by
…

    Mentions: s, nonzeroS, ψ

  25. lemma sum_ψ₂ Special case of sum_ψ, for the case where nonzeroS D x has two elements line 223 source

    Source comment

    Special case of `sum_ψ`, for the case where `nonzeroS D x` has two elements.
    private lemma sum_ψ₂ (hx : 0 < x)
    (h : D ^ (-⌈logb D (4 * x)⌉) < 1 / (2 * D * x)) :
    ∑ s ∈ nonzeroS D x, ψ D (D ^ (-s) * x) = 1 := by
…

    Mentions: s, nonzeroS, ψ

  26. lemma sum_ψ See finsum_ψ for the version that doesn't explicitly restrict to the support line 250 source

    Source comment

    See `finsum_ψ` for the version that doesn't explicitly restrict to the support.

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

    Statement uses: Nat, Real, LT.lt, OfNat.ofNat, Eq, Finset.sum, Int, nonzeroS, ψ, HMul.hMul, HPow.hPow, Neg.neg

    Proof uses: dite, GE.ge, Int.ceil, Real.logb, HDiv.hDiv, Not, lt_of_not_ge

    43 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

    lemma sum_ψ (hx : 0 < x) : ∑ s ∈ nonzeroS D x, ψ D (D ^ (-s) * x) = 1 := by
…

    Mentions: s, nonzeroS, ψ

  27. lemma mem_nonzeroS_iff line 259 source

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

    Statement uses: Nat, LT.lt, Real, OfNat.ofNat, Int, Iff, Membership.mem, Finset, nonzeroS, Set, Set.Ioo, Inv.inv, HMul.hMul, HPow.hPow, Neg.neg

    Proof uses: Eq.mpr, And, id, Eq, congrArg, propext, Set.mem_Ioo, Finset.Icc, Int.floor, HAdd.hAdd, Real.logb, Int.ceil, nonzeroS.eq_1, LE.le, Finset.mem_Icc, Int.floor_le_iff, HSub.hSub, Int.le_ceil_iff, mul_inv_rev, add_comm and 41 more

    159 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  28. lemma psi_ne_zero_iff line 269 source

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

    Statement uses: Nat, Int, LT.lt, Real, OfNat.ofNat, Iff, Ne, ψ, HMul.hMul, HPow.hPow, Neg.neg, Membership.mem, Finset, nonzeroS

    Proof uses: Eq.mpr, Set, Function.support, id, Eq, congrArg, Eq.symm, propext, Function.mem_support, Set.Ioo, Inv.inv, support_ψ, cast, Eq.trans, congrFun', Nat.cast_one, mem_nonzeroS_iff, Iff.rfl

    56 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  29. lemma psi_eq_zero_iff line 273 source

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

    Statement uses: Nat, Int, LT.lt, Real, OfNat.ofNat, Iff, Eq, ψ, HMul.hMul, HPow.hPow, Neg.neg, Not, Membership.mem, Finset, nonzeroS

    Proof uses: Eq.mpr, id, congrArg, Eq.symm, propext, iff_not_comm, Ne, psi_ne_zero_iff, Iff.rfl

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  30. lemma support_ψS line 276 source

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

    Statement uses: Nat, Real, LT.lt, OfNat.ofNat, Eq, Set, Int, Function.support, ψ, HMul.hMul, HPow.hPow, Neg.neg, Finset, nonzeroS

    Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Ne, id, congrArg, propext, Function.mem_support, psi_ne_zero_iff

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  31. lemma support_ψS_subset_Icc line 279 source

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

    Statement uses: Nat, LT.lt, Real, OfNat.ofNat, Int, Membership.mem, Set, Set.Icc, HDiv.hDiv, HPow.hPow, HSub.hSub, LE.le, Function.support, ψ, HMul.hMul, Neg.neg

    Proof uses: GT.gt, lt_of_lt_of_le, div_pos, zpow_pos, lt_trans, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, Mathlib.Meta.NormNum.instAtLeastTwo, And.left, Eq.mpr, And, id, Eq, And.intro, le_trans, Int.floor and 29 more

    139 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

  32. lemma finsum_ψ line 294 source

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

    Statement uses: Nat, Real, LT.lt, OfNat.ofNat, Eq, finsum, Int, ψ, HMul.hMul, HPow.hPow, Neg.neg

    Proof uses: Eq.trans, Finset.sum, nonzeroS, Function.HasFiniteSupport, Set.Finite, Finset, Finset.finite_toSet, Eq.mp, Function.support, congrArg, Set, Eq.symm, support_ψS, Set.Finite.toFinset, finsum_eq_sum, AddCommMonoid, Eq.rec, Eq.refl, Finset.ext, Eq.mpr and 8 more

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  33. lemma sum_ψ_le line 304 source

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

    Statement uses: Nat, Real, LT.lt, OfNat.ofNat, Finset, Int, LE.le, Finset.sum, ψ, HMul.hMul, HPow.hPow, Neg.neg

    Proof uses: Trans.trans, Eq, nonzeroS, Inter.inter, Eq.symm, Finset.sum_subset, Finset.inter_subset_left, Membership.mem, Not, Iff.mpr, psi_eq_zero_iff, And, Finset.mem_inter, And.intro, Finset.sum_le_sum_of_subset_of_nonneg, Finset.inter_subset_right, zero_le_ψ, sum_ψ

    41 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  34. lemma zpow_realD_pos line 326 source
  35. def Ks K_s in the blueprint line 330 source

    Source documentation

    K_s in the blueprint

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Int

    Proof uses: HMul.hMul, ψ, defaultD, Real, HPow.hPow, Neg.neg, Dist.dist

    12 instances, coercions and auxiliary constants left out.

    def Ks [KernelProofData a K] (s : ℤ) (x y : X) : ℂ :=
…

    Mentions: KernelProofData, K, s

  36. lemma Ks_def line 335 source

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Int, Eq, Ks, HMul.hMul, ψ, defaultD, Real, HPow.hPow, Neg.neg, Dist.dist

    Proof uses: rfl

    12 instances, coercions and auxiliary constants left out.

  37. lemma sum_Ks line 337 source

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Finset, Int, LE.le, nonzeroS, defaultD, Dist.dist, LT.lt, Real, OfNat.ofNat, Eq, Finset.sum, Ks

    Proof uses: id, Eq.mpr, HMul.hMul, ψ, HPow.hPow, Neg.neg, congrFun', congrArg, Eq.symm, Finset.sum_subset, Membership.mem, Not, propext, psi_eq_zero_iff, sum_ψ, Eq.refl, Complex.ofReal_one, mul_one

    56 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  38. lemma dist_mem_Ioo_of_Ks_ne_zero line 346 source

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Int, Ne, Ks, OfNat.ofNat, Membership.mem, Real, Set, Set.Ioo, HDiv.hDiv, HPow.hPow, defaultD, HSub.hSub, Dist.dist

    Proof uses: Inv.inv, HMul.hMul, Eq.rec, Function.support, ψ, Eq, Iff.mpr, Function.mem_support, And.right, Not, Iff.mp, Or, And, not_or, Eq.mp, Eq.trans, congrFun', congrArg, Neg.neg, zpow_neg and 19 more

    104 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  39. lemma dist_mem_Icc_of_Ks_ne_zero Lemma 2.1.3 part 1, equation (2.1.2) line 355 source

    Source documentation

    Lemma 2.1.3 part 1, equation (2.1.2)

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Int, Ne, Ks, OfNat.ofNat, Membership.mem, Real, Set, Set.Icc, HDiv.hDiv, HPow.hPow, defaultD, HSub.hSub, Dist.dist

    Proof uses: Set.Ioo_subset_Icc_self, dist_mem_Ioo_of_Ks_ne_zero

    39 instances, coercions and auxiliary constants left out.

    lemma dist_mem_Icc_of_Ks_ne_zero {s : ℤ} {x y : X} (h : Ks s x y ≠ 0) :
    dist x y ∈ Icc ((D ^ (s - 1) : ℝ) / 4) (D ^ s / 2) :=
…

    Mentions: s, Ks

  40. lemma dist_mem_Icc_of_mem_tsupport_Ks line 359 source

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Int, Prod, Membership.mem, Set, tsupport, Ks, Prod.fst, Prod.snd, Real, Set.Icc, HDiv.hDiv, HPow.hPow, defaultD, HSub.hSub, OfNat.ofNat, Dist.dist

    Proof uses: Function.support, Continuous, Prod.mk, continuous_dist, LE.le, Set.image, And, Ne, Eq, Exists, Eq.mp, Eq.trans, congrArg, funext, congrFun', dist_mem_Icc_of_Ks_ne_zero, subset_trans, closure, image_closure_subset_closure_image, Iff.mpr and 3 more

    65 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  41. lemma lowerBound_edist_of_Ks_ne_zero line 375 source
  42. def C2_1_3 The constant appearing in part 2 of Lemma 2.1.3 line 387 source

    Source documentation

    The constant appearing in part 2 of Lemma 2.1.3. Equal to 2 ^ (102 * a ^ 3) in the blueprint.

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

    Statement uses: Nat, NNReal

    Proof uses: HPow.hPow, OfNat.ofNat, HMul.hMul, HAdd.hAdd, 𝕔

    17 instances, coercions and auxiliary constants left out.

    def C2_1_3 (a : ℕ) : ℝ≥0 := 2 ^ ((𝕔 + 2) * a ^ 3)
  43. def D2_1_3 The constant appearing in part 3 of Lemma 2.1.3 line 391 source

    Source documentation

    The constant appearing in part 3 of Lemma 2.1.3. Equal to 2 ^ (127 * a ^ 3) in the blueprint.

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

    Statement uses: Nat, NNReal

    Proof uses: HPow.hPow, OfNat.ofNat, HMul.hMul, HAdd.hAdd, 𝕔, HDiv.hDiv

    19 instances, coercions and auxiliary constants left out.

    def D2_1_3 (a : ℕ) : ℝ≥0 := 2 ^ ((𝕔 + 2 + 𝕔 / 4) * a ^ 3)
  44. lemma kernel_bound Equation (1.1.11) in the blueprint line 394 source

    Source documentation

    Equation (1.1.11) in the blueprint

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Int, LE.le, ENNReal, ENorm.enorm, Ks, HDiv.hDiv, C_K, Real, vol, NNReal, defaultA

    Proof uses: id, HMul.hMul, ψ, defaultD, HPow.hPow, Neg.neg, Dist.dist, Trans.trans, OfNat.ofNat, Eq, rfl, enorm_mul, mul_le_mul', le_refl, Eq.mpr, ENNReal.ofReal, Norm.norm, congrArg, Eq.symm, ofReal_norm and 9 more

    114 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

    lemma kernel_bound {s : ℤ} {x y : X} : ‖Ks s x y‖ₑ ≤ C_K a / vol x y := by
…

    Mentions: s, Ks, C_K, vol

  45. lemma DoublingMeasure.volume_real_ball_two_le_same_repeat Apply volume_ball_two_le_same n times line 406 source

    Source documentation

    Apply volume_ball_two_le_same n times.

    private lemma DoublingMeasure.volume_real_ball_two_le_same_repeat (x : X) (r : ℝ) (n : ℕ) :
    volume.real (ball x (2 ^ n * r)) ≤ (defaultA a) ^ n * volume.real (ball x r) := by
…

    Mentions: defaultA

  46. lemma DoublingMeasure.volume_real_ball_two_le_same_repeat' Special case of DoublingMeasure.volume_ball_two_le_same_repeat used to prove div_vol_le line 417 source

    Source comment

    Special case of `DoublingMeasure.volume_ball_two_le_same_repeat` used to prove `div_vol_le`
    private lemma DoublingMeasure.volume_real_ball_two_le_same_repeat' (x : X) (n : ℕ) :
    volume.real (ball x (2 ^ n * D ^ s)) ≤
    (defaultA a) ^ (2 + n + 𝕔 * a ^ 2) * volume.real (ball x (D ^ (s - 1) / 4)) := by
…

    Mentions: s, defaultA

  47. lemma DoublingMeasure.volume_ball_two_le_same_repeat Apply volume_ball_two_le_same n times line 426 source

    Source documentation

    Apply volume_ball_two_le_same n times.

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Real, LE.le, ENNReal, MeasureTheory.Measure, NNReal, defaultA, Set, MeasureTheory.MeasureSpace.volume, Metric.ball, HMul.hMul, HPow.hPow, OfNat.ofNat

    Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', pow_zero, one_mul, Nat.cast_pow, Eq.mpr, HAdd.hAdd, id, Eq, add_comm, pow_add, pow_one, mul_assoc, LE.le.trans, MeasureTheory.Measure.IsDoubling.measure_ball_two_le_same and 3 more

    89 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

    lemma DoublingMeasure.volume_ball_two_le_same_repeat (x : X) (r : ℝ) (n : ℕ) :
    volume (ball x (2 ^ n * r)) ≤ (defaultA a) ^ n * volume (ball x r) := by
…

    Mentions: defaultA

  48. lemma DoublingMeasure.volume_ball_two_le_same_repeat' Special case of DoublingMeasure.volume_ball_two_le_same_repeat used to prove div_vol_le' line 438 source

    Source comment

    Special case of `DoublingMeasure.volume_ball_two_le_same_repeat` used to prove `div_vol_le'`
    private lemma DoublingMeasure.volume_ball_two_le_same_repeat' (x : X) (n : ℕ) :
    volume (ball x (2 ^ n * D ^ s)) ≤
    (defaultA a) ^ (2 + n + 𝕔 * a ^ 2) * volume (ball x (D ^ (s - 1) / 4)) := by
…

    Mentions: s, defaultA

  49. lemma Metric.measure_ball_pos_nnreal line 446 source

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Real, GT.gt, OfNat.ofNat, NNReal, ENNReal.toNNReal, MeasureTheory.Measure, defaultA, Set, ENNReal, MeasureTheory.MeasureSpace.volume, Metric.ball

    Proof uses: ENNReal.toNNReal_pos, ne_of_gt, Metric.measure_ball_pos, MeasureTheory.measure_ball_ne_top

    48 instances, coercions and auxiliary constants left out.

  50. lemma Metric.measure_ball_pos_real line 450 source

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Real, GT.gt, OfNat.ofNat, MeasureTheory.Measure.real, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, Metric.ball

    Proof uses: Metric.measure_ball_pos_nnreal

    15 instances, coercions and auxiliary constants left out.

  51. lemma div_vol_le line 455 source
  52. lemma div_vol_le' line 473 source
  53. lemma div_vol_le₀ Useful special case of div_vol_le line 486 source

    Source comment

    Useful special case of `div_vol_le`
    private lemma div_vol_le₀ {x y : X} {c : ℝ≥0∞} (hK : Ks s x y ≠ 0) :
    c / vol x y ≤ (2 ^ (2 * a + 𝕔 * a ^ 3)) * c / volume (ball x (D ^ s)) := by
…

    Mentions: c, Ks, s, vol

  54. lemma norm_K_le preferably use enorm_K_le line 498 source

    Source comment

    preferably use `enorm_K_le`
    private lemma norm_K_le {s : ℤ} {x y : X} (n : ℕ) (hxy : dist x y ≥ D ^ (s - 1) / 4) :
    ‖K x y‖ ≤ 2 ^ ((2 + n) * a + (𝕔 + 1) * a ^ 3) / volume.real (ball x (2 ^ n * D ^ s)) := by
…

    Mentions: s, K

  55. lemma enorm_K_le line 506 source

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Int, GE.ge, Real, Dist.dist, HDiv.hDiv, HPow.hPow, defaultD, HSub.hSub, OfNat.ofNat, LE.le, ENNReal, ENorm.enorm, HAdd.hAdd, HMul.hMul, 𝕔, MeasureTheory.Measure and 5 more

    Proof uses: le_trans, C_K, vol, enorm_K_le_vol_inv, id, ENNReal.div_le_div, cast, Eq.symm, Eq.trans, congr, congrArg, NNReal.rpow_natCast, Nat.cast_pow, Nat.cast_mul, le_of_eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.cast_pos and 28 more

    148 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  56. lemma norm_Ks_le Lemma 2.1.3 part 2 (Real version) line 515 source

    Source documentation

    Lemma 2.1.3 part 2 (Real version). Prefer enorm_Ks_le

    private lemma norm_Ks_le {s : ℤ} {x y : X} :
    ‖Ks s x y‖ ≤ C2_1_3 a / volume.real (ball x (D ^ s)) := by
…

    Mentions: s, Ks, C2_1_3

  57. lemma enorm_Ks_le Lemma 2.1.3 part 2, equation (2.1.3) line 531 source

    Source documentation

    Lemma 2.1.3 part 2, equation (2.1.3)

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Int, LE.le, ENNReal, ENorm.enorm, Ks, HDiv.hDiv, C2_1_3, MeasureTheory.Measure, NNReal, defaultA, Set, MeasureTheory.MeasureSpace.volume, Metric.ball, HPow.hPow, Real, defaultD

    Proof uses: Trans.trans, Eq, MeasureTheory.Measure.real, Eq.mpr, Norm.norm, id, congrArg, Eq.symm, enorm_norm, Real.enorm_le_enorm, norm_nonneg, HMul.hMul, Inv.inv, div_eq_mul_inv, enorm_mul, enorm_inv, Iff.mpr, Ne, ENNReal.toReal, OfNat.ofNat and 16 more

    116 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

    lemma enorm_Ks_le {s : ℤ} {x y : X} :
    ‖Ks s x y‖ₑ ≤ C2_1_3 a / volume (ball x (D ^ s)) := by
…

    Mentions: s, Ks, C2_1_3

  58. lemma enorm_Ks_le' Needed for Lemma 7.5.5 line 544 source

    Source documentation

    Needed for Lemma 7.5.5.

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Int, LE.le, ENNReal, ENorm.enorm, Ks, HMul.hMul, HDiv.hDiv, C2_1_3, MeasureTheory.Measure, NNReal, defaultA, Set, MeasureTheory.MeasureSpace.volume, Metric.ball, HPow.hPow, Real and 4 more

    Proof uses: dite, Eq, OfNat.ofNat, Eq.mpr, id, congrArg, enorm_zero, zero_le, Not, Ks.eq_1, enorm_mul, Norm.norm, Eq.symm, enorm_norm, Complex.norm_real, mul_le_mul', le_trans, HAdd.hAdd, 𝕔, enorm_K_le and 93 more

    238 instances, coercions and auxiliary constants left out.

    Tactic trace: 19 steps

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

    lemma enorm_Ks_le' {s : ℤ} {x y : X} :
    ‖Ks s x y‖ₑ ≤ C2_1_3 a / volume (ball x (D ^ s)) * ‖ψ (D ^ (-s) * dist x y)‖ₑ := by
…

    Mentions: s, Ks, C2_1_3, ψ

  59. lemma norm_Ks_le_of_dist_le Ks is bounded uniformly in x, y assuming x is in a fixed closed ball line 556 source

    Source documentation

    Ks is bounded uniformly in x, y assuming x is in a fixed closed ball.

    private lemma norm_Ks_le_of_dist_le {x y x₀ : X} {r₀ : ℝ} (hr₀ : 0 < r₀) (hx : dist x x₀ ≤ r₀) (s : ℤ) :
    ‖Ks s x y‖ ≤ C2_1_3 a * (As (defaultA a) (2 * r₀ / D ^ s)) / volume.real (ball x₀ r₀) := by
…

    Mentions: s, Ks, C2_1_3, As, defaultA

  60. lemma _root_.Bornology.IsBounded.exists_bound_of_norm_Ks ‖Ks x y‖ is bounded if x is in a bounded set line 577 source

    Source documentation

    ‖Ks x y‖ is bounded if x is in a bounded set

    lemma _root_.Bornology.IsBounded.exists_bound_of_norm_Ks
    {A : Set X} (hA : IsBounded A) (s : ℤ) :
    ∃ C, 0 ≤ C ∧ ∀ x y, x ∈ A → ‖Ks s x y‖ ≤ C := by
…

    Mentions: A, s, Ks

  61. lemma enorm_ψ_sub_ψ_le_two Needed to prove ψ_ineq line 588 source

    Source comment

    Needed to prove `ψ_ineq`
    private lemma enorm_ψ_sub_ψ_le_two {r s : ℝ} : ‖ψ r - ψ s‖ₑ ≤ 2 := by
…

    Mentions: s, ψ

  62. lemma ψ_ineq line 596 source
  63. lemma D_pow_a_inv line 624 source
  64. lemma four_D_rpow_a_inv line 632 source
  65. lemma enorm_Ks_sub_Ks_le_close_pt1 line 652 source
  66. lemma enorm_Ks_sub_Ks_le_close_pt2 line 700 source
  67. lemma enorm_Ks_sub_Ks_le_close Second case of norm_Ks_sub_Ks_le in blueprint line 713 source

    Source comment

    Second case of `norm_Ks_sub_Ks_le` in blueprint
    private lemma enorm_Ks_sub_Ks_le_close {s : ℤ} {x y y' : X} (hK : Ks s x y ≠ 0)
    (h : 2 * edist y y' ≤ edist x y) : ‖Ks s x y - Ks s x y'‖ₑ ≤
    D2_1_3 a / volume (ball x (D ^ s)) * (edist y y' / D ^ s) ^ (a : ℝ)⁻¹ := by
…

    Mentions: s, Ks, D2_1_3

  68. lemma enorm_Ks_sub_Ks_le_far First case of norm_Ks_sub_Ks_le in blueprint line 750 source

    Source comment

    First case of `norm_Ks_sub_Ks_le` in blueprint
    private lemma enorm_Ks_sub_Ks_le_far {s : ℤ} {x y y' : X} (hK : Ks s x y ≠ 0)
    (h : ¬ 2 * edist y y' ≤ edist x y) : ‖Ks s x y - Ks s x y'‖ₑ ≤
      D2_1_3 a / volume (ball x (D ^ s)) * (edist y y' / D ^ s) ^ (a : ℝ)⁻¹ := by
…

    Mentions: s, Ks, D2_1_3

  69. lemma enorm_Ks_sub_Ks_le_of_nonzero line 813 source

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Int, Ne, Ks, OfNat.ofNat, LE.le, ENNReal, ENorm.enorm, HSub.hSub, HMul.hMul, HDiv.hDiv, D2_1_3, MeasureTheory.Measure, NNReal, defaultA, Set, MeasureTheory.MeasureSpace.volume and 6 more

    Proof uses: dite, Not

    106 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  70. lemma enorm_Ks_sub_Ks_le Lemma 2.1.3 part 3, equation (2.1.4) line 821 source

    Source documentation

    Lemma 2.1.3 part 3, equation (2.1.4)

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Int, LE.le, ENNReal, ENorm.enorm, HSub.hSub, Ks, HMul.hMul, HDiv.hDiv, D2_1_3, MeasureTheory.Measure, NNReal, defaultA, Set, MeasureTheory.MeasureSpace.volume, Metric.ball, HPow.hPow and 4 more

    Proof uses: dite, Or, Ne, OfNat.ofNat, Eq, enorm_Ks_sub_Ks_le_of_nonzero, Eq.mpr, Neg.neg, id, congrArg, Eq.symm, neg_sub, enorm_neg, WeakPseudoEMetricSpace.edist_comm, Not, And.left, Eq.mp, And, Eq.trans, congr and 5 more

    138 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

    lemma enorm_Ks_sub_Ks_le {s : ℤ} {x y y' : X} :
    ‖Ks s x y - Ks s x y'‖ₑ ≤
      D2_1_3 a / volume (ball x (D ^ s)) * (edist y y' / D ^ s) ^ (a : ℝ)⁻¹ := by
…

    Mentions: s, Ks, D2_1_3

  71. lemma stronglyMeasurable_Ks line 833 source

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Int, MeasureTheory.StronglyMeasurable, Prod, NNReal, defaultA, Ks, Prod.fst, Prod.snd

    Proof uses: id, HMul.hMul, ψ, defaultD, Real, HPow.hPow, Neg.neg, Dist.dist, MeasureTheory.StronglyMeasurable.mul, Function.uncurry, Max.max, OfNat.ofNat, Min.min, HSub.hSub, MeasureTheory.stronglyMeasurable_K, Continuous.stronglyMeasurable, Continuous.comp', Complex.continuous_ofReal, Continuous.sup, continuous_const and 7 more

    97 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  72. lemma measurable_Ks line 840 source

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Int, Measurable, Prod, NNReal, defaultA, Ks, Prod.fst, Prod.snd

    Proof uses: id, HMul.hMul, ψ, defaultD, Real, HPow.hPow, Neg.neg, Dist.dist, Measurable.mul, Function.uncurry, Max.max, OfNat.ofNat, Min.min, HSub.hSub, IsOneSidedKernel.measurable_K, Measurable.complex_ofReal, Measurable.const_sup, Measurable.const_inf, Measurable.min, Measurable.sub_const and 6 more

    96 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  73. lemma aestronglyMeasurable_Ks line 845 source

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Int, MeasureTheory.AEStronglyMeasurable, Prod, NNReal, defaultA, Ks, Prod.fst, Prod.snd, MeasureTheory.MeasureSpace.volume

    Proof uses: Measurable.aestronglyMeasurable, measurable_Ks

    45 instances, coercions and auxiliary constants left out.

  74. lemma integrable_Ks_x The function y ↦ Ks s x y is integrable line 849 source

    Source documentation

    The function y ↦ Ks s x y is integrable.

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

    Statement uses: Nat, Complex, PseudoMetricSpace, KernelProofData, Int, LT.lt, Real, OfNat.ofNat, defaultD, MeasureTheory.Integrable, NNReal, defaultA, Ks, MeasureTheory.MeasureSpace.volume

    Proof uses: HMul.hMul, HPow.hPow, Inv.inv, mul_pos, zpow_pos, lt_trans, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, inv_pos_of_pos, Mathlib.Meta.NormNum.instAtLeastTwo, Eq.mpr, MeasureTheory.IntegrableOn, Compl.compl, Set, Metric.ball, id and 68 more

    205 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

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

    lemma integrable_Ks_x {s : ℤ} {x : X} (hD : 1 < (D : ℝ)) : Integrable (Ks s x) := by
…

    Mentions: s, Ks

  75. lemma Ks_eq_zero_of_dist_le line 875 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, Ne, LE.le, Dist.dist, HDiv.hDiv, HPow.hPow, defaultD, HSub.hSub, OfNat.ofNat, Eq, Ks

    Proof uses: Eq.mpr, HMul.hMul, ψ, Neg.neg, id, congrArg, Ks_def, Or, Eq.trans, Or.inr, Not, Membership.mem, Finset, nonzeroS, propext, psi_eq_zero_iff, one_lt_realD, Iff.mpr, LT.lt, dist_pos and 88 more

    191 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

  76. lemma Ks_eq_zero_of_le_dist line 893 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, LE.le, HDiv.hDiv, HPow.hPow, defaultD, OfNat.ofNat, Dist.dist, Eq, Ks

    Proof uses: Ne, Eq.mpr, LT.lt, id, congrArg, Eq.symm, propext, dist_pos, lt_of_lt_of_le, of_eq_true, defaultD_pow_pos, HMul.hMul, ψ, Neg.neg, Ks_def, Or, Eq.trans, Or.inr, Not, Membership.mem and 12 more

    98 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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