Carleson/Discrete/Defs.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

81 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)
Imported by 4 files
  1. def aux𝓒 line 16 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Grid

    Proof uses: Set.ofPred, Exists, And, LE.le, LT.lt, ENNReal, HMul.hMul, HPow.hPow, OfNat.ofNat, Neg.neg, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Inter.inter

    53 instances, coercions and auxiliary constants left out.

  2. def 𝓒 The partition 𝓒(G, k) of Grid X by volume, given in (5.1.1) and (5.1.2) line 21 source

    Source documentation

    The partition 𝓒(G, k) of Grid X by volume, given in (5.1.1) and (5.1.2). Note: the G is fixed with properties in ProofData.

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Grid

    Proof uses: SDiff.sdiff, aux𝓒, HAdd.hAdd, OfNat.ofNat

    32 instances, coercions and auxiliary constants left out.

    def 𝓒 (k : β„•) : Set (Grid X) :=
…

    Mentions: k, Grid

  3. def TilesAt The definition 𝔓(k) given in (5.1.3) line 25 source

    Source documentation

    The definition 𝔓(k) given in (5.1.3).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.preimage, Grid, π“˜, 𝓒

    27 instances, coercions and auxiliary constants left out.

    def TilesAt (k : β„•) : Set (𝔓 X) := π“˜ ⁻¹' 𝓒 k

    Mentions: k, 𝔓, π“˜, 𝓒

  4. lemma disjoint_TilesAt_of_ne line 27 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Ne, Disjoint, 𝔓, TilesAt

    Proof uses: LT.lt, Not, Or, Classical.em, Classical.byContradiction, And, Membership.mem, Exists, False, Eq.mp, congrArg, propext, Set.not_disjoint_iff, absurd, Grid, LE.le, π“˜, ENNReal, HMul.hMul, HPow.hPow and 22 more

    104 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  5. lemma pairwiseDisjoint_TilesAt line 34 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Set.PairwiseDisjoint, 𝔓, Set.univ, TilesAt

    Proof uses: Membership.mem, disjoint_TilesAt_of_ne

    35 instances, coercions and auxiliary constants left out.

  6. def aux𝔐 line 37 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.ofPred, And, Membership.mem, TilesAt, LT.lt, ENNReal, HMul.hMul, HPow.hPow, OfNat.ofNat, Neg.neg, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, π“˜, E₁

    50 instances, coercions and auxiliary constants left out.

  7. def 𝔐 The definition 𝔐(k, n) given in (5.1.4) and (5.1.5) line 41 source

    Source documentation

    The definition 𝔐(k, n) given in (5.1.4) and (5.1.5).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.ofPred, Maximal, Membership.mem, aux𝔐

    30 instances, coercions and auxiliary constants left out.

    def 𝔐 (k n : β„•) : Set (𝔓 X) := {m | Maximal (Β· ∈ aux𝔐 k n) m}

    Mentions: k, 𝔓, aux𝔐

  8. def dens' The definition dens'_k(𝔓') given in (5.1.6) line 44 source

    Source documentation

    The definition dens'_k(𝔓') given in (5.1.6).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, ENNReal

    Proof uses: iSup, Membership.mem, LE.le, OfNat.ofNat, TilesAt, TileLike, smul, HDiv.hDiv, HMul.hMul, HPow.hPow, Neg.neg, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Eβ‚‚, π“˜

    61 instances, coercions and auxiliary constants left out.

    def dens' (k : β„•) (P' : Set (𝔓 X)) : ℝβ‰₯0∞ :=
…

    Mentions: k, 𝔓

  9. lemma dens'_iSup line 49 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Eq, ENNReal, dens', iSup and 2 more

    Proof uses: id, Eq.mpr, LE.le, OfNat.ofNat, TilesAt, TileLike, smul, HDiv.hDiv, HMul.hMul, HPow.hPow, Neg.neg, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Eβ‚‚, π“˜, congrArg, funext, iSup_congr_Prop, Iff.of_eq, Eq.refl and 5 more

    74 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  10. def auxβ„­ line 52 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.ofPred, And, Membership.mem, TilesAt, LT.lt, ENNReal, HPow.hPow, OfNat.ofNat, HSub.hSub, HMul.hMul, dens', Singleton.singleton

    45 instances, coercions and auxiliary constants left out.

  11. def β„­ The partition β„­(k, n) of 𝔓(k) by density, given in (5.1.7) line 56 source

    Source documentation

    The partition β„­(k, n) of 𝔓(k) by density, given in (5.1.7).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.ofPred, And, Membership.mem, TilesAt, ENNReal, Set.Ioc, HPow.hPow, OfNat.ofNat, HSub.hSub, HMul.hMul, HAdd.hAdd, dens', Singleton.singleton

    45 instances, coercions and auxiliary constants left out.

    def β„­ (k n : β„•) : Set (𝔓 X) :=
…

    Mentions: k, 𝔓

  12. lemma β„­_subset_TilesAt line 59 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, β„­, TilesAt

    Proof uses: Membership.mem, And.left, ENNReal, Set.Ioc, HPow.hPow, OfNat.ofNat, HSub.hSub, HMul.hMul, HAdd.hAdd, dens', Singleton.singleton, Eq.mp, Set.ofPred, And, congrArg, propext, Set.mem_ofPred, β„­.eq_1

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  13. lemma disjoint_β„­_of_ne line 62 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Ne, Disjoint, 𝔓, β„­

    Proof uses: LT.lt, Not, Or, Classical.em, Classical.byContradiction, And, Membership.mem, Exists, False, Eq.mp, congrArg, propext, Set.not_disjoint_iff, absurd, ENNReal, Set.Ioc, HPow.hPow, OfNat.ofNat, HSub.hSub, HMul.hMul and 23 more

    97 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

  14. lemma pairwiseDisjoint_β„­ line 69 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Set.PairwiseDisjoint, 𝔓, Prod, Set.univ, β„­ and 2 more

    Proof uses: Membership.mem, Ne, Function.onFun, Disjoint, Prod.mk, id, dite, Eq, Eq.rec, disjoint_β„­_of_ne, Eq.mp, Not, And, congrArg, propext, not_and, Prod.mk.injEq, ne_eq, Set.disjoint_of_subset, TilesAt and 2 more

    52 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  15. lemma exists_bound_β„­ line 77 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Exists, Prod, Membership.mem, Set.ofPred, Set.Nonempty and 5 more

    Proof uses: Set.exists_upper_bound_image, Set.Finite, Set.iUnion, Set.toFinite, And.right, Iff.mp, And, Set.finite_iUnion_iff, Ne, pairwiseDisjoint_β„­, Set.mem_univ

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  16. def maxβ„­ line 85 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt

    Proof uses: Prod.snd, Exists.choose, Prod, Membership.mem, Set.ofPred, Set.Nonempty, 𝔓, β„­, Prod.fst, LE.le, exists_bound_β„­

    27 instances, coercions and auxiliary constants left out.

  17. lemma le_maxβ„­_of_nonempty line 87 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Set.Nonempty, 𝔓, β„­, LE.le, maxβ„­

    Proof uses: Exists.choose_spec, Prod, Membership.mem, Set.ofPred, Prod.fst, Prod.snd, exists_bound_β„­, Prod.mk

    29 instances, coercions and auxiliary constants left out.

  18. lemma eq_empty_of_maxβ„­_lt line 90 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LT.lt, maxβ„­, Eq, 𝔓, β„­ and 1 more

    Proof uses: Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, Set.Nonempty, LE.le, id, implies_congr, Ne, Exists.choose_spec, Prod, Membership.mem, Set.ofPred, Prod.fst, Prod.snd, exists_bound_β„­, Prod.mk

    39 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  19. lemma dens1_le_dens' Lemma 5.3.11 line 95 source

    Source documentation

    Lemma 5.3.11

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, TilesAt, ENNReal, dens₁ and 1 more

    Proof uses: Eq.mpr, iSup, Membership.mem, GE.ge, OfNat.ofNat, HMul.hMul, HPow.hPow, Neg.neg, lowerCubes, TileLike, smul, HDiv.hDiv, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Eβ‚‚, π“˜, id, Eq, congrArg, dens₁.eq_1 and 46 more

    116 instances, coercions and auxiliary constants left out.

    Tactic trace: 23 steps

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

    lemma dens1_le_dens' {k : β„•} {P : Set (𝔓 X)} (hP : P βŠ† TilesAt k) : dens₁ P ≀ dens' k P := by
…

    Mentions: k, 𝔓, TilesAt, dens₁, dens'

  20. lemma dens1_le Lemma 5.3.12 line 112 source

    Source documentation

    Lemma 5.3.12

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, LE.le, β„­, ENNReal, dens₁ and 5 more

    Proof uses: Trans.trans, dens', dens1_le_dens', LE.le.trans, TilesAt, β„­_subset_TilesAt, iSup_le_iSup_of_subset, iSup, Membership.mem, TileLike, smul, HDiv.hDiv, Neg.neg, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Eβ‚‚, π“˜, Eq.mpr, Singleton.singleton, id and 21 more

    127 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

    lemma dens1_le {k n : β„•} {A : Set (𝔓 X)} (hA : A βŠ† β„­ k n) : dens₁ A ≀ 2 ^ (4 * (a : ℝ) - n + 1) :=
…

    Mentions: k, A, 𝔓, β„­, dens₁

  21. def 𝔅 The subset 𝔅(p) of 𝔐(k, n), given in (5.1.8) line 121 source

    Source documentation

    The subset 𝔅(p) of 𝔐(k, n), given in (5.1.8).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.ofPred, And, Membership.mem, 𝔐, LE.le, TileLike, smul, OfNat.ofNat

    35 instances, coercions and auxiliary constants left out.

    def 𝔅 (k n : β„•) (p : 𝔓 X) : Set (𝔓 X) :=
…

    Mentions: k, 𝔓

  22. def preℭ₁ line 125 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.ofPred, And, Membership.mem, β„­, LE.le, HPow.hPow, OfNat.ofNat, Finset.card, Finset.filter, 𝔅, Classical.propDecidable, Finset.univ

    34 instances, coercions and auxiliary constants left out.

  23. def ℭ₁ The subset ℭ₁(k, n, j) of β„­(k, n), given in (5.1.9) line 130 source

    Source documentation

    The subset ℭ₁(k, n, j) of β„­(k, n), given in (5.1.9). Together with 𝔏₀(k, n) this forms a partition.

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: SDiff.sdiff, preℭ₁, HAdd.hAdd, OfNat.ofNat

    30 instances, coercions and auxiliary constants left out.

    def ℭ₁ (k n j : β„•) : Set (𝔓 X) :=
…

    Mentions: k, 𝔓

  24. lemma ℭ₁_subset_β„­ line 133 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, ℭ₁, β„­

    Proof uses: Membership.mem, And.left, HPow.hPow, OfNat.ofNat, Finset.card, Finset.filter, 𝔅, Classical.propDecidable, Finset.univ, And, Not, preℭ₁, HAdd.hAdd, Eq.mp, Set.ofPred, congrArg, propext, Set.mem_ofPred, SDiff.sdiff, Set.mem_sdiff and 2 more

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  25. lemma disjoint_ℭ₁_of_ne line 136 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Ne, Disjoint, 𝔓, ℭ₁

    Proof uses: LT.lt, Not, Or, Classical.em, Classical.byContradiction, And, Membership.mem, Exists, False, Eq.mp, congrArg, propext, Set.not_disjoint_iff, HPow.hPow, OfNat.ofNat, HAdd.hAdd, LE.le.trans_lt, Finset.card, Finset.filter, 𝔅 and 18 more

    94 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  26. lemma pairwiseDisjoint_ℭ₁ line 143 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Set.PairwiseDisjoint, 𝔓, Set.univ, ℭ₁

    Proof uses: Membership.mem, disjoint_ℭ₁_of_ne

    35 instances, coercions and auxiliary constants left out.

  27. lemma pairwiseDisjoint_ℭ₁' line 146 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Set.PairwiseDisjoint, 𝔓, Prod, Set.univ, ℭ₁ and 2 more

    Proof uses: Membership.mem, Ne, Function.onFun, Disjoint, Prod.mk, Eq, Or, ne_or_eq, β„­, pairwiseDisjoint_β„­, Set.mem_univ, of_eq_true, Not, Eq.trans, False, True, congrArg, And, Prod.mk.injEq, congrFun' and 12 more

    48 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

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

  28. lemma card_𝔅_of_mem_ℭ₁ line 157 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Membership.mem, ℭ₁, Fintype, 𝔅 and 6 more

    Proof uses: And.intro, LE.le, LT.lt, Eq.mpr, Finset.filter, Classical.propDecidable, Finset.univ, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, Finset, Finset.ext, of_eq_true, Iff, Eq.trans, True and 16 more

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  29. def 𝔏₀ The subset 𝔏₀(k, n) of β„­(k, n), given in (5.1.10) line 166 source

    Source documentation

    The subset 𝔏₀(k, n) of β„­(k, n), given in (5.1.10). Not to be confused with 𝔏₀(k, n, j) which is called 𝔏₀' in Lean.

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.ofPred, And, Membership.mem, β„­, Eq, 𝔅, EmptyCollection.emptyCollection

    28 instances, coercions and auxiliary constants left out.

    def 𝔏₀ (k n : β„•) : Set (𝔓 X) :=
…

    Mentions: k, 𝔓

  30. def 𝔏₁ 𝔏₁(k, n, j, l) consists of the minimal elements in ℭ₁(k, n, j) not in 𝔏₁(k, n, j, l') for some l' < l line 171 source

    Source documentation

    𝔏₁(k, n, j, l) consists of the minimal elements in ℭ₁(k, n, j) not in 𝔏₁(k, n, j, l') for some l' < l. Defined near (5.1.11).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.minLayer, ℭ₁

    27 instances, coercions and auxiliary constants left out.

    def 𝔏₁ (k n j l : β„•) : Set (𝔓 X) :=
…

    Mentions: k, 𝔓

  31. def β„­β‚‚ The subset β„­β‚‚(k, n, j) of ℭ₁(k, n, j), given in (5.1.13) line 175 source

    Source documentation

    The subset β„­β‚‚(k, n, j) of ℭ₁(k, n, j), given in (5.1.13).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.layersAbove, ℭ₁, HMul.hMul, defaultZ, HAdd.hAdd, OfNat.ofNat

    32 instances, coercions and auxiliary constants left out.

    def β„­β‚‚ (k n j : β„•) : Set (𝔓 X) :=
…

    Mentions: k, 𝔓

  32. lemma β„­β‚‚_subset_ℭ₁ line 178 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, β„­β‚‚, ℭ₁

    Proof uses: Set.layersAbove_subset, HMul.hMul, defaultZ, HAdd.hAdd, OfNat.ofNat

    33 instances, coercions and auxiliary constants left out.

  33. def π”˜β‚ The subset π”˜β‚(k, n, j) of ℭ₁(k, n, j), given in (5.1.14) line 181 source

    Source documentation

    The subset π”˜β‚(k, n, j) of ℭ₁(k, n, j), given in (5.1.14).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.ofPred, And, Membership.mem, ℭ₁, LT.lt, Grid, π“˜, Disjoint, WithFunctionDistance, 𝔠, HDiv.hDiv, HPow.hPow, 𝔰, OfNat.ofNat, Metric.ball, PreTileStructure.𝒬

    51 instances, coercions and auxiliary constants left out.

    def π”˜β‚ (k n j : β„•) : Set (𝔓 X) :=
…

    Mentions: k, 𝔓

  34. lemma π”˜β‚_subset_ℭ₁ line 184 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, π”˜β‚, ℭ₁

    Proof uses: Membership.mem, And.left, LT.lt, Grid, π“˜, Disjoint, WithFunctionDistance, 𝔠, HDiv.hDiv, HPow.hPow, 𝔰, OfNat.ofNat, Metric.ball, PreTileStructure.𝒬

    52 instances, coercions and auxiliary constants left out.

  35. def 𝔏₂ The subset 𝔏₂(k, n, j) of β„­β‚‚(k, n, j), given in (5.1.15) line 187 source

    Source documentation

    The subset 𝔏₂(k, n, j) of β„­β‚‚(k, n, j), given in (5.1.15).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.ofPred, And, Membership.mem, β„­β‚‚, Not, Exists, π”˜β‚, Ne, Grid, π“˜, LE.le, TileLike, smul, OfNat.ofNat

    36 instances, coercions and auxiliary constants left out.

    def 𝔏₂ (k n j : β„•) : Set (𝔓 X) :=
…

    Mentions: k, 𝔓

  36. lemma 𝔏₂_subset_β„­β‚‚ line 190 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, 𝔏₂, β„­β‚‚

    Proof uses: Membership.mem, And.left, Not, Exists, And, π”˜β‚, Ne, Grid, π“˜, TileLike, smul, OfNat.ofNat

    37 instances, coercions and auxiliary constants left out.

  37. def ℭ₃ The subset ℭ₃(k, n, j) of β„­β‚‚(k, n, j), given in (5.1.16) line 193 source

    Source documentation

    The subset ℭ₃(k, n, j) of β„­β‚‚(k, n, j), given in (5.1.16).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: SDiff.sdiff, β„­β‚‚, 𝔏₂

    27 instances, coercions and auxiliary constants left out.

    def ℭ₃ (k n j : β„•) : Set (𝔓 X) :=
…

    Mentions: k, 𝔓

  38. lemma ℭ₃_def line 196 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Iff, Membership.mem, ℭ₃, And and 10 more

    Proof uses: Eq.mpr, SDiff.sdiff, 𝔏₂, id, Eq, congrArg, ℭ₃.eq_1, Not, propext, Set.mem_sdiff, Set.ofPred, 𝔏₂.eq_1, Set.mem_ofPred, not_and, and_congr_right_iff, True, congrFun', implies_congr, eq_true, Eq.refl and 4 more

    53 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  39. lemma ℭ₃_subset_β„­β‚‚ line 201 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, ℭ₃, β„­β‚‚

    Proof uses: Membership.mem, And.left, Not, 𝔏₂, Eq.mp, SDiff.sdiff, And, congrArg, propext, Set.mem_sdiff, ℭ₃.eq_1

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  40. def 𝔏₃ 𝔏₃(k, n, j, l) consists of the maximal elements in ℭ₃(k, n, j) not in 𝔏₃(k, n, j, l') for some l' < l line 206 source

    Source documentation

    𝔏₃(k, n, j, l) consists of the maximal elements in ℭ₃(k, n, j) not in 𝔏₃(k, n, j, l') for some l' < l. Defined near (5.1.17).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.maxLayer, ℭ₃

    27 instances, coercions and auxiliary constants left out.

    def 𝔏₃ (k n j l : β„•) : Set (𝔓 X) :=
…

    Mentions: k, 𝔓

  41. def β„­β‚„ The subset β„­β‚„(k, n, j) of ℭ₃(k, n, j), given in (5.1.19) line 210 source

    Source documentation

    The subset β„­β‚„(k, n, j) of ℭ₃(k, n, j), given in (5.1.19).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.layersBelow, ℭ₃, HMul.hMul, defaultZ, HAdd.hAdd, OfNat.ofNat

    32 instances, coercions and auxiliary constants left out.

    def β„­β‚„ (k n j : β„•) : Set (𝔓 X) :=
…

    Mentions: k, 𝔓

  42. lemma β„­β‚„_subset_ℭ₃ line 213 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, β„­β‚„, ℭ₃

    Proof uses: Set.layersBelow_subset, HMul.hMul, defaultZ, HAdd.hAdd, OfNat.ofNat

    33 instances, coercions and auxiliary constants left out.

  43. def 𝓛 The subset 𝓛(u) of Grid X, given near (5.1.20) line 217 source

    Source documentation

    The subset 𝓛(u) of Grid X, given near (5.1.20). Note: It seems to also depend on n.

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Grid

    Proof uses: Set.ofPred, And, LE.le, π“˜, Eq, HAdd.hAdd, s, HMul.hMul, defaultZ, OfNat.ofNat, 𝔰, Not, Metric.ball, c, HPow.hPow

    49 instances, coercions and auxiliary constants left out.

    def 𝓛 (n : β„•) (u : 𝔓 X) : Set (Grid X) :=
…

    Mentions: 𝔓, Grid

  44. def 𝔏₄ The subset 𝔏₄(k, n, j) of β„­β‚„(k, n, j), given near (5.1.22) line 223 source

    Source documentation

    The subset 𝔏₄(k, n, j) of β„­β‚„(k, n, j), given near (5.1.22). Todo: we may need to change the definition to say that p is at most the least upper bound of 𝓛 n u in Grid X.

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.ofPred, And, Membership.mem, β„­β‚„, Exists, π”˜β‚, LE.le, π“˜, Set.iUnion, Grid, 𝓛

    30 instances, coercions and auxiliary constants left out.

    def 𝔏₄ (k n j : β„•) : Set (𝔓 X) :=
…

    Mentions: k, 𝔓

  45. lemma 𝔏₄_subset_β„­β‚„ line 226 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, 𝔏₄, β„­β‚„

    Proof uses: Membership.mem, And.left, Exists, And, π”˜β‚, π“˜, Set.iUnion, Grid, 𝓛

    31 instances, coercions and auxiliary constants left out.

  46. def β„­β‚… The subset β„­β‚…(k, n, j) of β„­β‚„(k, n, j), given in (5.1.23) line 229 source

    Source documentation

    The subset β„­β‚…(k, n, j) of β„­β‚„(k, n, j), given in (5.1.23).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: SDiff.sdiff, β„­β‚„, 𝔏₄

    27 instances, coercions and auxiliary constants left out.

    def β„­β‚… (k n j : β„•) : Set (𝔓 X) :=
…

    Mentions: k, 𝔓

  47. lemma β„­β‚…_def line 232 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓, Iff, Membership.mem, β„­β‚…, And and 8 more

    Proof uses: Eq.mpr, SDiff.sdiff, 𝔏₄, id, Eq, congrArg, β„­β‚….eq_1, propext, Set.mem_sdiff, Set.ofPred, Exists, 𝔏₄.eq_1, Set.mem_ofPred, not_and, and_congr_right_iff, True, congrFun', implies_congr, eq_true, Eq.refl and 6 more

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  48. lemma β„­β‚…_subset_β„­β‚„ line 237 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, β„­β‚…, β„­β‚„

    Proof uses: Membership.mem, And.left, Not, 𝔏₄, Eq.mp, SDiff.sdiff, And, congrArg, propext, Set.mem_sdiff, β„­β‚….eq_1

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  49. lemma β„­β‚…_subset_ℭ₁ line 240 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, β„­β‚…, ℭ₁

    Proof uses: LE.le.trans, β„­β‚„, β„­β‚…_subset_β„­β‚„, ℭ₃, β„­β‚„_subset_ℭ₃, β„­β‚‚, ℭ₃_subset_β„­β‚‚, β„­β‚‚_subset_ℭ₁

    33 instances, coercions and auxiliary constants left out.

  50. lemma pairwiseDisjoint_β„­β‚… line 243 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Set.PairwiseDisjoint, 𝔓, Prod, Set.univ, β„­β‚… and 2 more

    Proof uses: Set.PairwiseDisjoint.mono, ℭ₁, pairwiseDisjoint_ℭ₁', β„­β‚…_subset_ℭ₁

    44 instances, coercions and auxiliary constants left out.

  51. lemma 𝔏₀_subset_β„­ line 252 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, 𝔏₀, β„­

    Proof uses: Membership.mem, And.left, Eq, 𝔅, EmptyCollection.emptyCollection

    29 instances, coercions and auxiliary constants left out.

  52. lemma 𝔏₀_disjoint_ℭ₁ line 253 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Disjoint, 𝔓, 𝔏₀, ℭ₁

    Proof uses: Classical.byContradiction, Not, And, Membership.mem, Exists, False, Eq.mp, congrArg, propext, Set.not_disjoint_iff, β„­, Eq, 𝔅, EmptyCollection.emptyCollection, preℭ₁, HAdd.hAdd, OfNat.ofNat, LE.le, HPow.hPow, Finset.card and 72 more

    131 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  53. lemma 𝔏₁_subset_ℭ₁ line 258 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, 𝔏₁, ℭ₁

    Proof uses: Set.minLayer_subset

    28 instances, coercions and auxiliary constants left out.

  54. lemma 𝔏₁_subset_β„­ line 259 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, 𝔏₁, β„­

    Proof uses: LE.le.trans, Set.minLayer, ℭ₁, Set.minLayer_subset, ℭ₁_subset_β„­

    34 instances, coercions and auxiliary constants left out.

  55. lemma 𝔏₂_subset_ℭ₁ line 261 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, 𝔏₂, ℭ₁

    Proof uses: LE.le.trans, β„­β‚‚, 𝔏₂_subset_β„­β‚‚, β„­β‚‚_subset_ℭ₁

    33 instances, coercions and auxiliary constants left out.

  56. lemma 𝔏₂_subset_β„­ line 262 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, 𝔏₂, β„­

    Proof uses: LE.le.trans, ℭ₁, 𝔏₂_subset_ℭ₁, ℭ₁_subset_β„­

    33 instances, coercions and auxiliary constants left out.

  57. lemma 𝔏₂_disjoint_ℭ₃ line 263 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Disjoint, 𝔓, 𝔏₂, ℭ₃

    Proof uses: Set.disjoint_sdiff_right, β„­β‚‚

    35 instances, coercions and auxiliary constants left out.

  58. lemma 𝔏₃_subset_ℭ₁ line 265 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, 𝔏₃, ℭ₁

    Proof uses: LE.le.trans, Set.maxLayer, ℭ₃, β„­β‚‚, Set.maxLayer_subset, ℭ₃_subset_β„­β‚‚, β„­β‚‚_subset_ℭ₁

    34 instances, coercions and auxiliary constants left out.

  59. lemma 𝔏₃_subset_β„­ line 267 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, 𝔏₃, β„­

    Proof uses: LE.le.trans, ℭ₁, 𝔏₃_subset_ℭ₁, ℭ₁_subset_β„­

    33 instances, coercions and auxiliary constants left out.

  60. lemma 𝔏₄_subset_ℭ₁ line 269 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, 𝔏₄, ℭ₁

    Proof uses: LE.le.trans, β„­β‚‚, ℭ₃, β„­β‚„, 𝔏₄_subset_β„­β‚„, β„­β‚„_subset_ℭ₃, ℭ₃_subset_β„­β‚‚, β„­β‚‚_subset_ℭ₁

    33 instances, coercions and auxiliary constants left out.

  61. lemma 𝔏₄_subset_β„­ line 271 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, 𝔏₄, β„­

    Proof uses: LE.le.trans, ℭ₁, 𝔏₄_subset_ℭ₁, ℭ₁_subset_β„­

    33 instances, coercions and auxiliary constants left out.

  62. lemma β„­β‚…_subset_β„­ line 273 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, 𝔓, β„­β‚…, β„­

    Proof uses: LE.le.trans, ℭ₁, β„­β‚…_subset_ℭ₁, ℭ₁_subset_β„­

    33 instances, coercions and auxiliary constants left out.

  63. def highDensityTiles The set $\mathcal{P}_{F,G}$, defined in (5.1.24) line 278 source

    Source documentation

    The set $\mathcal{P}_{F,G}$, defined in (5.1.24).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.ofPred, LT.lt, ENNReal, HDiv.hDiv, HMul.hMul, HPow.hPow, OfNat.ofNat, HAdd.hAdd, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, densβ‚‚, Singleton.singleton

    53 instances, coercions and auxiliary constants left out.

    def highDensityTiles : Set (𝔓 X) :=
…

    Mentions: 𝔓

  64. lemma highDensityTiles_empty line 282 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Eq, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, OfNat.ofNat and 3 more

    Proof uses: densβ‚‚, Singleton.singleton, id, Eq.mpr, iSup, Membership.mem, GE.ge, HMul.hMul, HPow.hPow, 𝔰, HDiv.hDiv, Inter.inter, Metric.ball, 𝔠, forall_congr, Eq.trans, implies_congr, Eq.refl, Or, Top.top and 10 more

    89 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  65. lemma highDensityTiles_empty' line 287 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Eq, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, OfNat.ofNat and 3 more

    Proof uses: dite, highDensityTiles_empty, Not, HDiv.hDiv, HMul.hMul, HPow.hPow, HAdd.hAdd, Top.top, Eq.rec, ENNReal.div_zero, mul_ne_zero, of_eq_true, Eq.trans, False, True, congrArg, And, congr, Or, congrFun' and 13 more

    96 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  66. def G₁ The exceptional set G₁, defined in (5.1.25) line 295 source

    Source documentation

    The exceptional set G₁, defined in (5.1.25).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt

    Proof uses: Set.iUnion, 𝔓, Membership.mem, highDensityTiles, π“˜

    28 instances, coercions and auxiliary constants left out.

    def G₁ : Set X := ⋃ (p : 𝔓 X) (_ : p ∈ highDensityTiles), π“˜ p

    Mentions: 𝔓, highDensityTiles, π“˜

  67. lemma G₁_empty line 297 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Eq, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, OfNat.ofNat and 2 more

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Set.iUnion, 𝔓, Membership.mem, highDensityTiles, π“˜, funext, Set.iUnion_congr_Prop, Iff.of_eq, highDensityTiles_empty, Eq.refl, Set.biUnion_empty, eq_self

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  68. lemma G₁_empty' line 300 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Eq, ENNReal, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, OfNat.ofNat and 2 more

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Set.iUnion, 𝔓, Membership.mem, highDensityTiles, π“˜, funext, Set.iUnion_congr_Prop, Iff.of_eq, highDensityTiles_empty', Eq.refl, Set.biUnion_empty, eq_self

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  69. lemma measurable_G₁ line 303 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, MeasurableSet, G₁

    Proof uses: Set.Finite.measurableSet_biUnion, 𝔓, π“˜, highDensityTiles, Set.toFinite, Membership.mem, GridStructure.coeGrid_measurable

    35 instances, coercions and auxiliary constants left out.

  70. def setA The set A(Ξ», k, n), defined in (5.1.26) line 307 source

    Source documentation

    The set A(Ξ», k, n), defined in (5.1.26).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt

    Proof uses: Set.ofPred, LT.lt, HMul.hMul, HPow.hPow, OfNat.ofNat, HAdd.hAdd, stackSize, 𝔐

    34 instances, coercions and auxiliary constants left out.

    def setA (l k n : β„•) : Set X :=
…

    Mentions: k

  71. lemma setA_subset_iUnion_𝓒 line 310 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, setA, Set.iUnion, Grid, Membership.mem and 1 more

    Proof uses: LT.lt, OfNat.ofNat, Finset.card, 𝔓, Finset.filter, And, 𝔐, π“˜, Classical.propDecidable, Finset.univ, LE.le.trans_lt, HMul.hMul, HPow.hPow, HAdd.hAdd, zero_le, Eq.mp, congrArg, Finset, Finset.filter_filter, Finset.sum and 34 more

    84 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

  72. lemma setA_subset_setA line 323 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, LE.le, setA, HAdd.hAdd, OfNat.ofNat

    Proof uses: Iff.mpr, Set.ofPred, LT.lt, HMul.hMul, HPow.hPow, stackSize, 𝔐, Set.ofPred_subset_ofPred, Trans.trans, mul_le_mul', le_refl

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  73. lemma measurable_setA line 329 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, MeasurableSet, setA

    Proof uses: measurableSet_lt, HMul.hMul, HPow.hPow, OfNat.ofNat, HAdd.hAdd, stackSize, 𝔐, measurable_const, Finset.measurable_sum, 𝔓, Set.indicator, π“˜, Finset.filter, Membership.mem, Classical.propDecidable, Finset.univ, Finset, Measurable.indicator, measurable_one, GridStructure.coeGrid_measurable

    84 instances, coercions and auxiliary constants left out.

  74. def MsetA Finset of cubes in setA line 334 source

    Source documentation

    Finset of cubes in setA. Appears in the proof of Lemma 5.2.5.

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, Finset, Grid

    Proof uses: Finset.filter, LE.le, setA, Classical.propDecidable, Finset.univ

    31 instances, coercions and auxiliary constants left out.

    def MsetA (l k n : β„•) : Finset (Grid X) := { j | (j : Set X) βŠ† setA l k n }

    Mentions: k, Grid, setA

  75. def Gβ‚‚ The set Gβ‚‚, defined in (5.1.27) line 337 source

    Source documentation

    The set Gβ‚‚, defined in (5.1.27).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt

    Proof uses: Set.iUnion, LE.le, setA, HAdd.hAdd, HMul.hMul, OfNat.ofNat

    30 instances, coercions and auxiliary constants left out.

    def Gβ‚‚ : Set X := ⋃ (n : β„•) (k ≀ n), setA (2 * n + 6) k n

    Mentions: k, setA

  76. lemma measurable_Gβ‚‚ line 339 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, MeasurableSet, Gβ‚‚

    Proof uses: MeasurableSet.iUnion, Set.iUnion, LE.le, setA, HAdd.hAdd, HMul.hMul, OfNat.ofNat, measurable_setA

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  77. def G₃ The set G₃, defined in (5.1.28) line 344 source

    Source documentation

    The set G₃, defined in (5.1.28).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt

    Proof uses: Set.iUnion, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, 𝔓, Membership.mem, 𝔏₄, π“˜

    34 instances, coercions and auxiliary constants left out.

    def G₃ : Set X := ⋃ (n : β„•) (k ≀ n) (j ≀ 2 * n + 3) (p ∈ 𝔏₄ (X := X) k n j), π“˜ p

    Mentions: k, 𝔏₄, π“˜

  78. lemma measurable_G₃ line 346 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, MeasurableSet, G₃

    Proof uses: MeasurableSet.iUnion, Set.iUnion, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, 𝔓, Membership.mem, 𝔏₄, π“˜, GridStructure.coeGrid_measurable

    43 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  79. def G' The set G', defined below (5.1.28) line 351 source

    Source documentation

    The set G', defined below (5.1.28).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt

    Proof uses: Union.union, G₁, Gβ‚‚, G₃

    25 instances, coercions and auxiliary constants left out.

    def G' : Set X := G₁ βˆͺ Gβ‚‚ βˆͺ G₃

    Mentions: G₁, Gβ‚‚, G₃

  80. lemma measurable_G' line 353 source

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, MeasurableSet, G'

    Proof uses: MeasurableSet.union, Union.union, G₁, Gβ‚‚, G₃, measurable_G₁, measurable_Gβ‚‚, measurable_G₃

    29 instances, coercions and auxiliary constants left out.

  81. def 𝔓₁ The set 𝔓₁, defined in (5.1.30) line 357 source

    Source documentation

    The set 𝔓₁, defined in (5.1.30).

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

    Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultΞΊ, defaultS, cancelPt, 𝔓

    Proof uses: Set.iUnion, LE.le, HAdd.hAdd, HMul.hMul, OfNat.ofNat, β„­β‚…

    32 instances, coercions and auxiliary constants left out.

    def 𝔓₁ : Set (𝔓 X) := ⋃ (n : β„•) (k ≀ n) (j ≀ 2 * n + 3), β„­β‚… k n j

    Mentions: 𝔓, k, β„­β‚