`Carleson/TileExistence.lean`

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

Annotation provenance. This overlay contains 10 curated AI-written annotations and 981 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

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

94 declarations, 0 contain sorry, 0 declared as axioms

Proof that there exists a tile structure on a grid structure.

Imports (1)

Carleson.TileStructure

Imported by 2 files

lemma ball_bound line 16 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Metric.ball, cancelPt, defaultA, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow, defaultD, Membership.mem
Proof uses: Trans.trans, Eq, Eq.mpr, HAdd.hAdd, id, congrArg, two_mul, Metric.ball_subset, Dist.dist, add_sub_cancel_right, LE.le.trans, LT.lt.le, Eq.mp, LT.lt, dist_comm, propext, Metric.mem_ball, tsub_le_iff_right, le_add_iff_nonneg_right, zpow_nonneg and 71 more
161 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma twopow_J line 41 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Eq, HPow.hPow, OfNat.ofNat, J', HMul.hMul, defaultD, defaultS
Proof uses: id, Eq.mpr, HAdd.hAdd, 𝕔, congrArg, pow_add, mul_assoc, mul_comm, pow_mul, of_eq_true, Eq.trans, True, congrFun', Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit1, eq_self and 2 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma twopow_J' line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Eq, NNReal, HPow.hPow, OfNat.ofNat, J', HMul.hMul, nnD, defaultS
Proof uses: id, NNReal.eq, Subtype.mk, LE.le, defaultD, Eq.mpr, congrFun', congrArg, twopow_J, Eq.trans, Nat.cast_mul, Nat.cast_pow, Eq.refl
48 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def C4_1_1 line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, NNReal
Proof uses: As, HPow.hPow, OfNat.ofNat, J'
13 instances, coercions and auxiliary constants left out.
lemma counting_balls line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Metric.ball, cancelPt, defaultA, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow, defaultD, Set.PairwiseDisjoint, ENNReal and 2 more
Proof uses: MeasureTheory.Measure, NNReal, MeasureTheory.MeasureSpace.volume, As, J', Ne, cast, Eq.trans, Not, Eq, congrArg, Eq.symm, Nat.cast_zero, congrFun', congr, Ne.symm, LT.lt.ne, MeasureTheory.As_pos', Trans.trans, Set.iUnion and 55 more
217 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
def property_set line 106 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData
Proof uses: Set.ofPred, And, LE.le, Metric.ball, cancelPt, defaultA, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow, defaultD, defaultS, Set.PairwiseDisjoint, Eq, Membership.mem
30 instances, coercions and auxiliary constants left out.
lemma property_set_nonempty line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Membership.mem, property_set, ite, Eq, defaultS, Singleton.singleton, cancelPt, defaultA, EmptyCollection.emptyCollection
Proof uses: id, Decidable, Set.ofPred, And, LE.le, Metric.ball, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow, defaultD, Set.PairwiseDisjoint, Not, Eq.mpr, congrArg, ite_eq_right, Eq.trans, 𝕔, congrFun', funext and 31 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma chain_property_set_has_bound line 123 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, property_set, IsChain, Exists, And, Membership.mem
Proof uses: Exists.intro, Union.union, Set.iUnion, ite, Eq, defaultS, Singleton.singleton, cancelPt, defaultA, EmptyCollection.emptyCollection, dite, Eq.mpr, HPow.hPow, OfNat.ofNat, id, Eq.trans, True, congr, congrArg, funext and 42 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 56 steps
Open to load the checked before-and-after goal states.
lemma zorn_apply_maximal_set line 173 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Exists, And, Membership.mem, property_set, LE.le, Eq
Proof uses: Maximal, zorn_subset, chain_property_set_has_bound, Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, funext, pi_congr, propext, of_eq_true, Iff, Eq.trans, True, congrFun', congrArg, iff_self, Eq.mp
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Yk line 180 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData
Proof uses: Exists.choose, And, Membership.mem, property_set, LE.le, Eq, zorn_apply_maximal_set
2 instances, coercions and auxiliary constants left out.
lemma Yk_pairwise line 182 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Set.PairwiseDisjoint, Yk, Metric.ball, HPow.hPow, defaultD
Proof uses: And.left, Exists.choose, And, Membership.mem, property_set, LE.le, Eq, zorn_apply_maximal_set, defaultS, cancelPt, defaultA, And.right, HSub.hSub, HMul.hMul, OfNat.ofNat, Exists.choose_spec
45 instances, coercions and auxiliary constants left out.
lemma Yk_subset line 185 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Yk, Metric.ball, cancelPt, defaultA, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow, defaultD, defaultS
Proof uses: And.left, Exists.choose, And, Membership.mem, property_set, Eq, zorn_apply_maximal_set, Set.PairwiseDisjoint, Exists.choose_spec
51 instances, coercions and auxiliary constants left out.
lemma Yk_maximal line 188 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Metric.ball, cancelPt, defaultA, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow, defaultD, defaultS, Set.PairwiseDisjoint, Yk, Eq and 1 more
Proof uses: And.right, property_set, Exists.choose, And, zorn_apply_maximal_set, Exists.choose_spec, And.intro
65 instances, coercions and auxiliary constants left out.
lemma o_mem_Yk_S line 194 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Membership.mem, Yk, defaultS, cancelPt, defaultA
Proof uses: And.right, Set.PairwiseDisjoint, Exists.choose, And, property_set, LE.le, Eq, zorn_apply_maximal_set, Metric.ball, HPow.hPow, defaultD, HSub.hSub, HMul.hMul, OfNat.ofNat, And.left, Exists.choose_spec, rfl
36 instances, coercions and auxiliary constants left out.
lemma cover_big_ball line 197 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Metric.ball, cancelPt, defaultA, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow, defaultD, defaultS, Set.iUnion, Membership.mem, Yk
Proof uses: Exists, And, Not, Disjoint, Classical.byContradiction, Eq, Union.union, Singleton.singleton, Yk_maximal, Eq.mpr, id, congrArg, propext, Set.union_subset_iff, Set.singleton_subset_iff, And.intro, Yk_subset, Set.PairwiseDisjoint, Ne, Set.pairwiseDisjoint_union and 46 more
145 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma Yk_nonempty line 230 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LT.lt, OfNat.ofNat, HSub.hSub, HMul.hMul, HPow.hPow, defaultD, defaultS, Set.Nonempty, Yk
Proof uses: LE.le, Singleton.singleton, cancelPt, defaultA, Metric.ball, Iff.mpr, Membership.mem, Set.singleton_subset_iff, Metric.mem_ball_self, Set.PairwiseDisjoint, Set.pairwiseDisjoint_singleton, Classical.byContradiction, Not, Exists.intro, Eq.rec, EmptyCollection.emptyCollection, Eq, Set.empty_subset, Eq.symm, Eq.mp and 8 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Yk_finite not sure if we actually need this; just countability seems quite good enough line 242 source
Source comment
not sure if we actually need this; just countability seems quite good enough

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Set.Finite, Yk
Proof uses: Eq.mpr, Ne, ENat, Set.encard, Top.top, id, Eq, congrArg, Eq.symm, propext, Set.encard_ne_top_iff, LT.lt.ne, LT.lt, ENNReal, ENat.toENNReal_lt, ENat.toENNReal_top, Trans.trans, C4_1_1, counting_balls, Yk_subset and 3 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma Yk_finite {k : ℤ} (hk_lower : -S ≤ k) : (Yk X k).Finite := by
…
```
Mentions: k, Yk
lemma Yk_countable line 252 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Set.Countable, Yk
Proof uses: Set.PairwiseDisjoint.countable_of_isOpen, NNReal, defaultA, Metric.ball, HPow.hPow, defaultD, Yk_pairwise, Membership.mem, Metric.isOpen_ball, Eq.mpr, Set.Nonempty, LT.lt, OfNat.ofNat, id, Eq, forall_congr, implies_congr, Eq.refl, realD_pos, zpow_pos
38 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def Yk_encodable line 260 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Encodable, Yk
Proof uses: Set.Countable.toEncodable, Yk_countable
1 instances, coercions and auxiliary constants left out.
def Encodable.linearOrder line 263 source
standard axioms: propext what this means
Statement uses: Encodable, LinearOrder
Proof uses: LinearOrder.lift', Nat, Encodable.encode, Encodable.encode_injective
1 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
instance (instance at line 266) line 266 source
instance (instance at line 267) line 267 source
lemma I_induction_proof line 278 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Not, Eq, HSub.hSub, OfNat.ofNat
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 33 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem aux Auxiliary lemma used in subsequent mutual blocks line 282 source
Source comment
Auxiliary lemma used in subsequent mutual blocks.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, LE.le, OfNat.ofNat, HAdd.hAdd, HSub.hSub, LT.lt, Nat, Int.toNat
Proof uses: Eq.mpr, id, Eq, congrArg, propext, Int.lt_toNat, Int.toNat_of_nonneg, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.neg_congr and 33 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem aux {s k : ℤ} (h1 : 0 ≤ s + (k - 1)) :
    (s + (k - 1)).toNat < (s + k).toNat := by
…
```
Mentions: s, k
lemma I3_apply line 314 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Yk, Eq, I3, Union.union, I1, SDiff.sdiff, I2, Xk, Set.iUnion, LT.lt
Proof uses: Eq.mpr, id, congrArg, I3.eq_1, Eq.refl
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma I1_subset_I3 line 318 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Yk, I1, I3
Proof uses: Membership.mem, Eq.mpr, Union.union, SDiff.sdiff, I2, Xk, Set.iUnion, LT.lt, id, Eq, congrArg, I3.eq_1, Or.inl
21 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma I1_subset_I2 line 325 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Yk, I1, I2
Proof uses: Eq.mpr, dite, Eq, Metric.ball, Membership.mem, HPow.hPow, defaultD, Not, LT.lt, OfNat.ofNat, HAdd.hAdd, HSub.hSub, Set.iUnion, Set.preimage, I3, I_induction_proof, id, congrArg, I1.eq_1, HMul.hMul and 25 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma I3_subset_I2 line 344 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Yk, I3, I2
Proof uses: Membership.mem, I1, And, Not, Or, Xk, Exists, LT.lt, Eq.mp, Union.union, SDiff.sdiff, Set.iUnion, Eq.trans, congrArg, funext, I3.eq_1, I1_subset_I2, And.left
25 instances, coercions and auxiliary constants left out.

Tactic trace: 87 steps
Open to load the checked before-and-after goal states.
lemma I3_prop_3_2 line 448 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Yk, I3, Metric.ball, Membership.mem, HMul.hMul, OfNat.ofNat, HPow.hPow, defaultD
Proof uses: PSigma.mk, PSigma
26 instances, coercions and auxiliary constants left out.

Tactic trace: 105 steps
Open to load the checked before-and-after goal states.
lemma I3_prop_3_1 line 576 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Yk, Metric.ball, Membership.mem, HMul.hMul, Inv.inv, OfNat.ofNat, HPow.hPow, defaultD, I3
Proof uses: Eq.mpr, Union.union, I1, SDiff.sdiff, I2, Xk, Set.iUnion, LT.lt, id, Eq, congrArg, I3.eq_1, dite, Not, HAdd.hAdd, HSub.hSub, Set.preimage, I_induction_proof, I1.eq_1, subset_trans and 148 more
202 instances, coercions and auxiliary constants left out.

Tactic trace: 56 steps
Open to load the checked before-and-after goal states.
lemma I3_nonempty line 645 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Yk, Set.Nonempty, I3
Proof uses: Exists.intro, Membership.mem, I3_prop_3_1, Eq.mpr, Metric.ball, HMul.hMul, Inv.inv, OfNat.ofNat, HPow.hPow, defaultD, LT.lt, Dist.dist, id, Eq, congrArg, propext, Metric.mem_ball, dist_self, of_eq_true, Eq.trans and 3 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma cover_by_cubes the additional argument hk to get decent equality theorems line 653 source
Source comment
the additional argument `hk` to get decent equality theorems

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Yk, I3, Set.iUnion
Proof uses: Int.leInduction, Membership.mem, Eq.mpr, Exists, id, Eq, congrArg, propext, Set.mem_iUnion, Exists.intro, HAdd.hAdd, OfNat.ofNat, LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast and 55 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma cover_by_cubes {l : ℤ} (hl : -S ≤ l) :
    ∀ {k : ℤ}, l ≤ k → (hk : -S ≤ k) → ∀ y, I3 hk y ⊆ ⋃ (yl : Yk X l), I3 hl yl := by
…
```
Mentions: k, Yk
lemma dyadic_property line 670 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Yk, Not, Disjoint, I3
Proof uses: PSigma.mk
20 instances, coercions and auxiliary constants left out.

Tactic trace: 135 steps
Open to load the checked before-and-after goal states.
structure ClosenessProperty line 801 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Yk
5 instances, coercions and auxiliary constants left out.
lemma transitive_boundary' line 809 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, LT.lt, Yk, Membership.mem, Inter.inter, I3, ClosenessProperty, And
Proof uses: ENNReal, Metric.infEDist, Compl.compl, HMul.hMul, OfNat.ofNat, HPow.hPow, defaultD, dyadic_property, LT.lt.le, Eq.mpr, Not, Disjoint, Exists, id, Eq, congrArg, propext, Set.not_disjoint_iff, Exists.intro, And.intro and 123 more
171 instances, coercions and auxiliary constants left out.

Tactic trace: 69 steps
Open to load the checked before-and-after goal states.
lemma transitive_boundary line 885 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Yk, Membership.mem, Inter.inter, I3, ClosenessProperty, And
Proof uses: dite, Eq, I3_prop_1, And.left, And.intro, ClosenessProperty.mk, le_refl, lt_of_le_of_lt, ENNReal, Metric.infEDist, Compl.compl, HMul.hMul, OfNat.ofNat, HPow.hPow, defaultD, Metric.infEDist_anti, Eq.mpr, id, ClosenessProperty.I3_subset, ClosenessProperty.I3_infdist_lt and 4 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
def const_K line 905 source
standard axioms: propext what this means
Statement uses: Nat
Proof uses: HPow.hPow, OfNat.ofNat, HAdd.hAdd, HMul.hMul
9 instances, coercions and auxiliary constants left out.
lemma K_pos line 912 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, Real, OfNat.ofNat, const_K
Proof uses: Eq.mpr, HPow.hPow, HAdd.hAdd, HMul.hMul, id, Eq, congrArg, const_K.eq_1, of_eq_true, Eq.trans, True, Nat.cast_pow
41 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def C4_1_7 TODO: fix overlapping instance warning; this will also fix the linter line 918 source
Source comment
TODO: fix overlapping instance warning; this will also fix the linter

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, NNReal
Proof uses: As, defaultA, HPow.hPow, OfNat.ofNat
14 instances, coercions and auxiliary constants left out.
```
def C4_1_7 [ProofData a q K σ₁ σ₂ F G] : ℝ≥0 := As (defaultA a) (2 ^ 4)
…
```
Mentions: ProofData, K, As, defaultA
lemma C4_1_7_eq line 921 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Eq, NNReal, C4_1_7, HPow.hPow, OfNat.ofNat, HMul.hMul
Proof uses: id, Eq.mpr, Nat.ceil, Real.logb, congrArg, Eq.symm, Real.rpow_natCast, Real.logb_rpow, lt_of_not_ge, LE.le, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance and 61 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma volume_tile_le_volume_ball line 927 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Yk, ENNReal, MeasureTheory.Measure, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, I3, HMul.hMul, C4_1_7, Metric.ball and 5 more
Proof uses: Trans.trans, MeasureTheory.measure_mono, Eq.mpr, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne', Mathlib.Tactic.Ring.Common.mul_congr, NNRat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo and 74 more
140 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma le_s line 939 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, HSub.hSub, const_K, Set.Ioc, Membership.mem
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat, Eq.mp, HAdd.hAdd, HMul.hMul, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 47 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma small_boundary' line 942 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, HSub.hSub, const_K, Yk, ENNReal, tsum, MeasureTheory.Measure, NNReal, defaultA, MeasureTheory.MeasureSpace.volume, Set.iUnion and 6 more
Proof uses: C4_1_7, Countable, Set.Countable.to_subtype, Yk_countable, Trans.trans, Set.Ioc, Membership.mem, le_s, Metric.ball, HPow.hPow, defaultD, Eq, Finset.sum, Finset.univ, Set.ofPred, Eq.mpr, HSMul.hSMul, Finset.card, id, congrArg and 225 more
298 instances, coercions and auxiliary constants left out.

Tactic trace: 193 steps
Open to load the checked before-and-after goal states.
lemma small_boundary line 1148 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, HSub.hSub, const_K, Yk, ENNReal, tsum, finsum, ClosenessProperty, MeasureTheory.Measure, NNReal, defaultA and 6 more
Proof uses: Trans.trans, Eq, Set.iUnion, rfl, AddCommMonoid, TopologicalSpace, Eq.rec, SummationFilter, Eq.refl, funext, Eq.mpr, ite, Classical.propDecidable, id, congrArg, finsum_eq_if, EmptyCollection.emptyCollection, Set.iUnion_eq_if, dite, of_eq_true and 10 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma le_s_1' line 1162 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, HSub.hSub, HMul.hMul, HAdd.hAdd, OfNat.ofNat, const_K
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.Common.neg_add, Mathlib.Meta.NormNum.IsInt.to_raw_eq and 43 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma le_s_2' line 1166 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, HSub.hSub, HMul.hMul, HAdd.hAdd, OfNat.ofNat, const_K
Proof uses: LE.le.trans, Eq.mp, congrArg, Eq.trans, congrFun', Nat.cast_add, Nat.cast_one, right_distrib, Eq.mpr, id, Eq, one_mul, sub_add_add_cancel, mul_nonneg, Nat.cast_nonneg'
73 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma boundary_sum_eq line 1171 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Yk, Eq, ENNReal, tsum, finsum, ClosenessProperty, MeasureTheory.Measure, NNReal, defaultA, MeasureTheory.MeasureSpace.volume and 3 more
Proof uses: Countable, Set.Countable.to_subtype, Yk_countable, Eq.mpr, id, congrArg, MeasureTheory.measure_iUnion, Ne, Function.onFun, Disjoint, Eq.trans, implies_congr, Eq.refl, Inter.inter, EmptyCollection.emptyCollection, propext, Set.disjoint_iff, Membership.mem, I3_prop_1, MeasurableSet.iUnion and 22 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma smaller_boundary line 1187 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, HSub.hSub, HMul.hMul, const_K, Yk, ENNReal, tsum, finsum, ClosenessProperty, MeasureTheory.Measure, NNReal and 7 more
Proof uses: Nat.recAux, Eq.mpr, Set.iUnion, id, Eq, congrArg, boundary_sum_eq, congr, funext, Set.iUnion_congr_Prop, Iff.of_eq, Eq.refl, Eq.trans, congrFun', pow_zero, one_mul, MeasureTheory.measure_mono, forall_congr, ClosenessProperty.I3_subset, HAdd.hAdd and 132 more
199 instances, coercions and auxiliary constants left out.

Tactic trace: 83 steps
Open to load the checked before-and-after goal states.
def const_n TODO: linter false positive line 1291 source
Source comment
TODO: linter false positive

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Membership.mem, Set, Set.Ioo, OfNat.ofNat
Proof uses: Nat.floor, HDiv.hDiv, Neg.neg, Real.logb, defaultD, const_K
24 instances, coercions and auxiliary constants left out.
```
def const_n {t : ℝ} (_ht : t ∈ Ioo 0 1) : ℕ := ⌊-Real.logb D t / K'⌋₊
…
```
Mentions: K'
theorem prefloor_nonneg line 1296 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Membership.mem, Set.Ioo, OfNat.ofNat, LE.le, HDiv.hDiv, Neg.neg, Real.logb, defaultD, const_K
Proof uses: div_nonneg, Eq.mpr, id, Eq, congrArg, propext, Real.logb_nonpos_iff, one_lt_realD, And.left, LT.lt, LT.lt.le, And.right, K_pos
53 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma const_n_prop_1 line 1304 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Membership.mem, Set.Ioo, OfNat.ofNat, LE.le, HPow.hPow, defaultD, HMul.hMul, const_n, const_K, Inv.inv
Proof uses: Eq.mpr, Real.logb, id, Eq, congrArg, Eq.symm, Real.rpow_logb, realD_pos, Ne.symm, LT.lt.ne, one_lt_realD, Iff.mpr, LT.lt, inv_pos, And.left, Eq.mp, And, Real.rpow_natCast, propext, Real.rpow_le_rpow_left_iff and 11 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma const_n_prop_2 line 1313 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Membership.mem, Set.Ioo, OfNat.ofNat, LE.le, HMul.hMul, HPow.hPow, defaultD, HSub.hSub, const_n, const_K
Proof uses: MulPosReflectLE, inferInstance, Eq.mpr, HAdd.hAdd, Neg.neg, id, Eq, congrArg, sub_eq_neg_add, zpow_add₀, Ne.symm, LT.lt.ne, realD_pos, propext, mul_le_mul_iff_left₀, LT.lt, zpow_pos, Inv.inv, zpow_neg, le_inv_comm₀ and 2 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma const_n_is_max line 1321 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Membership.mem, Set.Ioo, OfNat.ofNat, LE.le, HPow.hPow, defaultD, HMul.hMul, const_K, Inv.inv, const_n
Proof uses: Eq.mpr, Real.logb, id, Eq, congrArg, Eq.symm, Real.rpow_logb, realD_pos, Ne.symm, LT.lt.ne, one_lt_realD, Iff.mpr, LT.lt, inv_pos, And.left, Eq.mp, And, Real.rpow_natCast, propext, Real.rpow_le_rpow_left_iff and 12 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma const_n_prop_3 line 1330 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Membership.mem, Set.Ioo, OfNat.ofNat, LE.le, Inv.inv, HMul.hMul, HPow.hPow, defaultD, const_K, const_n
Proof uses: id, Eq.mpr, Nat.floor, HDiv.hDiv, Neg.neg, Real.logb, Eq, congrArg, mul_inv, Eq.symm, div_eq_mul_inv, propext, div_le_iff₀, LT.lt, realD_pos, pow_pos, HAdd.hAdd, pow_add, one_mul, right_distrib and 17 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma const_n_nonneg line 1343 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Membership.mem, Set.Ioo, OfNat.ofNat, LE.le, const_n
Proof uses: const_n_is_max, Eq.mpr, HPow.hPow, defaultD, HMul.hMul, const_K, Inv.inv, id, Eq, congrFun', congrArg, Eq.trans, MulZeroClass.zero_mul, pow_zero, Iff.mpr, And, LT.lt, one_le_inv_iff₀, And.intro, And.left and 2 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma kappa_le_log2D_inv_mul_K_inv line 1349 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, defaultκ, Inv.inv, HMul.hMul, Real.logb, OfNat.ofNat, defaultD, const_K
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 119 more
181 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
lemma boundary_measure line 1384 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Yk, NNReal, Membership.mem, Set.Ioo, OfNat.ofNat, HPow.hPow, defaultD, HMul.hMul, ENNReal, MeasureTheory.Measure and 8 more
Proof uses: HSub.hSub, const_n, const_K, LE.le.trans, const_n_prop_2, Eq.mp, congrArg, propext, Real.rpow_le_rpow_left_iff, one_lt_realD, congr, Eq.mpr, id, Eq, Eq.trans, HAdd.hAdd, mul_nonneg, Nat.cast_nonneg', Trans.trans, Inv.inv and 157 more
289 instances, coercions and auxiliary constants left out.

Tactic trace: 119 steps
Open to load the checked before-and-after goal states.
lemma boundary_measure' line 1510 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, LE.le, Neg.neg, defaultS, Yk, NNReal, Membership.mem, Set.Ioo, OfNat.ofNat, HPow.hPow, defaultD, HMul.hMul, MeasureTheory.Measure.real, defaultA and 8 more
Proof uses: id, Trans.trans, Eq, ENNReal.toReal, MeasureTheory.Measure, rfl, Eq.mpr, congrArg, Eq.symm, ENNReal.toReal_mul, propext, ENNReal.toReal_le_toReal, ne_of_lt, Top.top, LE.le.trans_lt, MeasureTheory.OuterMeasure.measureOf, MeasureTheory.Measure.toOuterMeasure, Inter.inter, WithBot.LE, OrderDual and 27 more
133 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
structure 𝓓 line 1537 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def max_𝓓 line 1545 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, 𝓓
Proof uses: 𝓓.mk, defaultS, Subtype.mk, Membership.mem, Yk, cancelPt, defaultA, o_mem_Yk_S, I3
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def 𝓓.coe line 1552 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, 𝓓
Proof uses: I3, 𝓓.k, 𝓓.hk, 𝓓.y
def forget_map line 1555 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, 𝓓, Sigma, Set.Icc, Neg.neg, defaultS, Yk, Membership.mem
Proof uses: Sigma.mk, Subtype.mk, 𝓓.k, 𝓓.y
25 instances, coercions and auxiliary constants left out.
lemma forget_map_inj line 1558 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Function.Injective, 𝓓, Sigma, Set.Icc, Neg.neg, defaultS, Yk, Membership.mem, forget_map
Proof uses: Eq, Iff.mpr, And, 𝓓.k, HEq, 𝓓.y, 𝓓.ext_iff, Eq.mp, Sigma.mk, Subtype.mk, Eq.trans, congrFun', congrArg, Subtype.mk.injEq
26 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma 𝓓_finite line 1565 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, Finite, 𝓓
Proof uses: Set.Icc, Neg.neg, defaultS, Yk, Membership.mem, Set.Finite.to_subtype, Yk_finite, And.left, LE.le, Subtype.property, Finite.of_injective, Sigma, forget_map, forget_map_inj
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def grid_existence Proof that there exists a grid structure line 1575 source
Source documentation
Proof that there exists a grid structure.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt
Proof uses: GridStructure.mk, 𝓓, Fintype.ofFinite, 𝓓_finite, 𝓓.coe, 𝓓.k, Membership.mem, Yk, 𝓓.y, max_𝓓
33 instances, coercions and auxiliary constants left out.

Tactic trace: 71 steps
Open to load the checked before-and-after goal states.
```
def grid_existence : GridStructure X D κ S o where
…
```
Mentions: GridStructure
def C𝓩 The constant appearing in 4.2.2 (3 / 10) line 1660 source
Source documentation
The constant appearing in 4.2.2 (3 / 10).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HDiv.hDiv, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
@[simp] def C𝓩 : ℝ := 3 / 10
…
```
def 𝓩_cands line 1666 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Finset, FunctionDistances.Θ
Proof uses: Finset.filter, Set.PairwiseDisjoint, WithFunctionDistance, c, HDiv.hDiv, HPow.hPow, s, OfNat.ofNat, Metric.ball, C𝓩, Classical.propDecidable, Finset.powerset, MeasureTheory.SimpleFunc.range, ProofData.Q
53 instances, coercions and auxiliary constants left out.
lemma exists_𝓩_max_card line 1670 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Exists, Finset, FunctionDistances.Θ, And, Membership.mem and 3 more
Proof uses: Finset.exists_max_image, Exists.intro, EmptyCollection.emptyCollection, of_eq_true, Finset.filter, Set.PairwiseDisjoint, WithFunctionDistance, c, HPow.hPow, OfNat.ofNat, HMul.hMul, 𝕔, HDiv.hDiv, s, Metric.ball, Classical.propDecidable, C𝓩, Finset.powerset, MeasureTheory.SimpleFunc.range, ProofData.Q and 7 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def 𝓩 A finset of maximal cardinality satisfying (4.2.1) and (4.2.2) line 1674 source
Source documentation
A finset of maximal cardinality satisfying (4.2.1) and (4.2.2).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Finset, FunctionDistances.Θ
Proof uses: Exists.choose, And, Membership.mem, 𝓩_cands, LE.le, Finset.card, exists_𝓩_max_card
33 instances, coercions and auxiliary constants left out.
```
def 𝓩 : Finset (Θ X) := (exists_𝓩_max_card I).choose
…
```
Mentions: exists_𝓩_max_card
lemma 𝓩_spec line 1678 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, And, LE.le, Finset, FunctionDistances.Θ, 𝓩 and 14 more
Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, propext, and_assoc, Exists.choose, exists_𝓩_max_card, eq_of_heq, HEq, Eq.refl, HEq.refl, Iff, Finset.filter, Classical.propDecidable, Finset.powerset, 𝓩_cands.eq_1, Finset.mem_filter, Finset.mem_powerset and 4 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma 𝓩_subset line 1684 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, LE.le, Finset, FunctionDistances.Θ, 𝓩, MeasureTheory.SimpleFunc.range and 1 more
Proof uses: And.left, And, Set.PairwiseDisjoint, WithFunctionDistance, c, HDiv.hDiv, HPow.hPow, s, OfNat.ofNat, Metric.ball, C𝓩, Membership.mem, 𝓩_cands, Finset.card, 𝓩_spec
65 instances, coercions and auxiliary constants left out.
lemma 𝓩_pairwiseDisjoint line 1685 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Set.PairwiseDisjoint, WithFunctionDistance, c, HDiv.hDiv, HPow.hPow and 7 more
Proof uses: And.left, Membership.mem, 𝓩_cands, LE.le, Finset.card, And.right, MeasureTheory.SimpleFunc.range, ProofData.Q, And, 𝓩_spec
83 instances, coercions and auxiliary constants left out.
lemma 𝓩_max_card line 1686 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Finset, FunctionDistances.Θ, Membership.mem, 𝓩_cands, LE.le and 2 more
Proof uses: And.right, Set.PairwiseDisjoint, WithFunctionDistance, c, HDiv.hDiv, HPow.hPow, s, OfNat.ofNat, Metric.ball, C𝓩, MeasureTheory.SimpleFunc.range, ProofData.Q, And, 𝓩_spec
63 instances, coercions and auxiliary constants left out.
lemma 𝓩_nonempty line 1689 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Finset.Nonempty, FunctionDistances.Θ, 𝓩
Proof uses: Decidable.byContradiction, Not, Finset, Membership.mem, 𝓩_cands, LE.le, Finset.card, 𝓩_max_card, Eq, Singleton.singleton, EmptyCollection.emptyCollection, Iff.mpr, And, Finset.eq_singleton_iff_unique_mem, And.intro, of_eq_true, Finset.filter, Set.PairwiseDisjoint, WithFunctionDistance, c and 32 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
instance (instance at line 1697) line 1697 source
def C4_2_1 7 / 10 line 1700 source
Source documentation
7 / 10

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HDiv.hDiv, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.
```
@[simp] def C4_2_1 : ℝ := 7 / 10 /- 0.6 also works? -/
…
```
lemma frequency_ball_cover Equation (4.2.3), Lemma 4.2.1 line 1704 source
Source documentation
Equation (4.2.3), Lemma 4.2.1

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, LE.le, FunctionDistances.Θ, Finset, MeasureTheory.SimpleFunc.range, ProofData.Q and 11 more
Proof uses: And, Not, Disjoint, C𝓩, Exists, Decidable.byContradiction, Classical.propDecidable, Eq.mp, Eq.trans, binderNameHint, forall_congr, Mathlib.Tactic.Push.not_and_eq, implies_congr, Eq.refl, False.elim, False, Eq, Mathlib.Meta.NormNum.instAtLeastTwo, Bot.bot, congr and 117 more
197 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
```
lemma frequency_ball_cover : (SetLike.coe Q.range) ⊆ ⋃ z ∈ 𝓩 I, ball_{I} z C4_2_1 := by
…
```
Mentions: 𝓩, C4_2_1
def Construction.Ω₁_aux line 1731 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, FunctionDistances.Θ
Proof uses: WellFounded.Nat.fix, InvImage, LT.lt, dite, Nat.card, Subtype, Membership.mem, Finset, 𝓩, SDiff.sdiff, Equiv, Fin, Equiv.symm, Finite.equivFin, Fin.mk, Metric.ball, WithFunctionDistance, c, HDiv.hDiv, HPow.hPow and 8 more
55 instances, coercions and auxiliary constants left out.
lemma Construction.Ω₁_aux_disjoint line 1737 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Ne, Disjoint, FunctionDistances.Θ, Construction.Ω₁_aux
Proof uses: LT.lt, Not, Or, Classical.em, LE.le, Set.iUnion, Set.subset_biUnion_of_mem, Nat.le, Nat.succ, Set.disjoint_of_subset_left, Eq.mpr, dite, Nat.card, Subtype, Membership.mem, Finset, 𝓩, SDiff.sdiff, Equiv, Fin and 26 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Construction.disjoint_ball_Ω₁_aux line 1748 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, FunctionDistances.Θ, Membership.mem, Finset, 𝓩, Ne and 16 more
Proof uses: Eq.mpr, dite, LT.lt, SDiff.sdiff, Equiv.symm, Fin.mk, C4_2_1, Set.iUnion, Singleton.singleton, Not, EmptyCollection.emptyCollection, id, Eq, congrArg, Construction.Ω₁_aux.eq_1, Eq.trans, True, dite_congr, eq_true, Fin.isLt and 20 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
def Construction.Ω₁ line 1756 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, 𝔓, ProofData.Q, FunctionDistances.Θ
Proof uses: Construction.Ω₁_aux, Sigma.fst, Grid, Subtype, Membership.mem, Finset, 𝓩, Nat.card, Equiv, Fin, Finite.equivFin, Sigma.snd
39 instances, coercions and auxiliary constants left out.
lemma Construction.disjoint_frequency_cubes Lemma 4.2.2 line 1759 source
Source documentation
Lemma 4.2.2

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Subtype, FunctionDistances.Θ, Membership.mem, Finset, 𝓩 and 5 more
Proof uses: Mathlib.Tactic.Contrapose.contrapose₂, Disjoint, Construction.Ω₁_aux, Nat.card, Equiv, Fin, Sigma.fst, Finite.equivFin, id, Not, Ne, Construction.Ω₁_aux_disjoint, Mathlib.Tactic.Contrapose.contrapose₄, Eq.mp, congrArg, propext, Equiv.apply_eq_iff_eq, Fin.val_eq_val
50 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma disjoint_frequency_cubes {f g : 𝓩 I} (h : (Ω₁ ⟨I, f⟩ ∩ Ω₁ ⟨I, g⟩).Nonempty) : f = g := by
…
```
Mentions: g, 𝓩, Construction.Ω₁
lemma Construction.ball_subset_Ω₁ Equation (4.2.6), first inclusion line 1768 source
Source documentation
Equation (4.2.6), first inclusion

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, 𝔓, ProofData.Q, LE.le, WithFunctionDistance, 𝔠, HDiv.hDiv and 7 more
Proof uses: Eq.mpr, Construction.Ω₁_aux, Sigma.fst, Grid, Subtype, FunctionDistances.Θ, Membership.mem, Finset, 𝓩, Nat.card, Equiv, Fin, Finite.equivFin, Sigma.snd, id, Eq, congrArg, Construction.Ω₁.eq_1, dite, LT.lt and 66 more
128 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
lemma ball_subset_Ω₁ (p : 𝔓 X) : ball_(p) (𝒬 p) C𝓩 ⊆ Ω₁ p := by
…
```
Mentions: 𝔓, C𝓩, Construction.Ω₁
lemma Construction.Ω₁_subset_ball Equation (4.2.6), second inclusion line 1784 source
Source documentation
Equation (4.2.6), second inclusion

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, 𝔓, ProofData.Q, LE.le, FunctionDistances.Θ, Construction.Ω₁, Metric.ball and 8 more
Proof uses: Eq.mpr, Construction.Ω₁_aux, Sigma.fst, Grid, Subtype, Membership.mem, Finset, 𝓩, Nat.card, Equiv, Fin, Finite.equivFin, Sigma.snd, id, Eq, congrArg, Construction.Ω₁.eq_1, dite, LT.lt, SDiff.sdiff and 26 more
77 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma Ω₁_subset_ball (p : 𝔓 X) : Ω₁ p ⊆ ball_(p) (𝒬 p) C4_2_1 := by
…
```
Mentions: 𝔓, Construction.Ω₁, C4_2_1
lemma Construction.iUnion_ball_subset_iUnion_Ω₁ Equation (4.2.5) line 1795 source
Source documentation
Equation (4.2.5)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, LE.le, WithFunctionDistance, c, HDiv.hDiv, HPow.hPow and 12 more
Proof uses: Eq.mpr, id, Eq, congrArg, propext, Set.iUnion₂_subset_iff, Equiv, Fin, Nat.card, Finite.equivFin, rfl, dite, Exists, And, C𝓩, Classical.propDecidable, Set.subset_iUnion_of_subset, Subtype.mk, subset_rfl, Construction.ball_subset_Ω₁ and 53 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
```
lemma iUnion_ball_subset_iUnion_Ω₁ : ⋃ z ∈ 𝓩 I, ball_{I} z C4_2_1 ⊆ ⋃ f : 𝓩 I, Ω₁ ⟨I, f⟩ := by
…
```
Mentions: 𝓩, C4_2_1, Construction.Ω₁
def Construction.CΩ 1 / 5 line 1820 source
Source documentation
1 / 5

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real
Proof uses: HDiv.hDiv, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
```
@[simp] def CΩ : ℝ := 1 / 5
…
```
def Construction.Ω line 1824 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, 𝔓, ProofData.Q, FunctionDistances.Θ
Proof uses: WellFounded.Nat.fix, Grid.opSize, Sigma.fst, Grid, Subtype, Membership.mem, Finset, 𝓩, InvImage, LT.lt, dite, IsMax, Classical.propDecidable, Construction.Ω₁, Not, Grid.succ, Union.union, Metric.ball, WithFunctionDistance, 𝔠 and 10 more
55 instances, coercions and auxiliary constants left out.
lemma Construction.𝔓_induction line 1830 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, 𝔓, ProofData.Q, IsMax, Grid, Sigma.fst, Subtype and 7 more
Proof uses: WellFounded.Nat.fix, Grid.opSize, InvImage, LT.lt, dite, Classical.propDecidable, Grid.opSize_succ_lt, id
43 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma Construction.Ω_subset_cball line 1840 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, 𝔓, ProofData.Q, LE.le, FunctionDistances.Θ, Construction.Ω, Metric.ball and 7 more
Proof uses: Construction.𝔓_induction, IsMax, Grid, Sigma.fst, Subtype, Membership.mem, Finset, 𝓩, Eq.mpr, dite, Classical.propDecidable, Construction.Ω₁, Not, LT.lt, Grid.opSize, Grid.succ, Union.union, Construction.CΩ, Set.iUnion, Inter.inter and 147 more
246 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
lemma Construction.Ω_disjoint_aux line 1880 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Not, IsMax, Subtype, FunctionDistances.Θ, Membership.mem and 20 more
Proof uses: Set.Nonempty, Function.mt, Eq, Construction.disjoint_frequency_cubes, Mathlib.Tactic.Contrapose.contrapose₂, And, Exists, Eq.mp, congrArg, propext, Set.not_disjoint_iff, Set.mem_iUnion₂, And.intro, C𝓩, Eq.mpr, LT.lt, Dist.dist, id, Metric.mem_ball, dist_comm and 136 more
261 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma Construction.Ω_disjoint line 1916 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, 𝔓, ProofData.Q, Ne, Eq, Grid, 𝓘 and 3 more
Proof uses: id, Sigma.fst, Subtype, Membership.mem, Finset, 𝓩, Sigma.mk, congrArg, Sigma, Grid.induction, IsMax, Eq.mpr, dite, Classical.propDecidable, Construction.Ω₁, Not, LT.lt, Grid.opSize, Grid.succ, Union.union and 76 more
124 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
lemma Construction.Ω_biUnion line 1940 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, LE.le, FunctionDistances.Θ, Finset, MeasureTheory.SimpleFunc.range, ProofData.Q and 7 more
Proof uses: Grid.induction, IsMax, Eq.mpr, Exists, Eq, id, Eq.trans, congrArg, funext, propext, exists_prop_congr, Iff.of_eq, Eq.refl, WithFunctionDistance, c, HDiv.hDiv, HPow.hPow, s, OfNat.ofNat, Subtype and 49 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma Construction.Ω_RFD line 1965 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, 𝔓, ProofData.Q, LE.le, Grid, 𝓘, Or and 3 more
Proof uses: PSigma.mk
47 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
def tile_existence line 2012 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, PseudoMetricSpace, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, TileStructure, ProofData.Q
Proof uses: TileStructure.mk, Construction.Ω, GridStructure.Grid, PreTileStructure.𝔓, Construction.Ω_disjoint, 𝔓, Construction.Ω_RFD, Construction.Ω_subset_cball
26 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.