`Carleson/GridStructure.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

67 declarations, 0 contain sorry, 0 declared as axioms

Maximal elements of finsets of dyadic cubes

Imports (1)

Carleson.ProofData

Imported by 2 files

class GridStructure A grid structure on X line 20 source
Source documentation
A grid structure on X. We prefer coeGrid : Grid → Set X over Grid : Set (Set X) Note: the s in this paper is -s of Christ's paper.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: outParam, NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real
```
class GridStructure {A : outParam ℝ≥0} [PseudoMetricSpace X] [DoublingMeasure X A]
    (D : outParam ℕ) (κ : outParam ℝ) (S : outParam ℕ) (o : outParam X) where
…
```
Mentions: A
abbrev Grid The indexing type of the grid structure line 58 source
Source documentation
The indexing type of the grid structure. Elements are called (dyadic) cubes. Note that this type has instances for both ≤ and ⊆, but they do not coincide.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure
Proof uses: GridStructure.Grid
```
abbrev Grid : Type u := GridStructure.Grid X
```
def s line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, Int
Proof uses: GridStructure.s
def c line 61 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid
Proof uses: GridStructure.c
instance (instance at line 65) line 65 source
instance (instance at line 66) line 66 source
instance (instance at line 67) line 67 source
instance (instance at line 68) line 68 source
instance (instance at line 69) line 69 source
lemma Grid.mem_def not sure whether these should be simp lemmas, but that might be required if we want to conveniently rewrite/simp with Set-lemmas line 73 source
Source comment
not sure whether these should be simp lemmas, but that might be required if we want to conveniently rewrite/simp with Set-lemmas

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, Iff, Membership.mem, Set
Proof uses: Iff.rfl
4 instances, coercions and auxiliary constants left out.
```
@[simp] lemma Grid.mem_def {x : X} : x ∈ i ↔ x ∈ (i : Set X) := .rfl
```
lemma Grid.le_def not sure whether these should be simp lemmas, but that might be required if we want to conveniently rewrite/simp with Set-lemmas line 74 source
Source comment
not sure whether these should be simp lemmas, but that might be required if we want to conveniently rewrite/simp with Set-lemmas

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, Iff, LE.le, And, Set, Int, s
Proof uses: Iff.rfl
9 instances, coercions and auxiliary constants left out.
```
@[simp] lemma Grid.le_def : i ≤ j ↔ (i : Set X) ⊆ (j : Set X) ∧ s i ≤ s j := .rfl
```
Mentions: s
lemma Grid.eq_iff line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, Iff, Eq, And, Set, Int, s
Proof uses: Iff.intro, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', eq_self, and_self, le_antisymm, LE.le
20 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Grid.mem_mono line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Monotone, Grid, Membership.mem
Proof uses: LE.le, Eq.mpr, Set, id, Eq, congrArg, propext, Grid.mem_def, And.left, Int, s, Eq.mp, And, Grid.le_def
12 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma fundamental_dyadic line 85 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, LE.le, Int, s, Or, Set, Disjoint
Proof uses: GridStructure.fundamental_dyadic'
12 instances, coercions and auxiliary constants left out.
lemma le_or_disjoint line 89 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, LE.le, Int, s, Or, Disjoint, Set
Proof uses: Or.imp, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, And.intro, Prod.snd, id, fundamental_dyadic
33 instances, coercions and auxiliary constants left out.
lemma le_or_ge_or_disjoint line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, Or, LE.le, Disjoint, Set
Proof uses: Int, s, LT.lt, le_or_gt, le_or_disjoint, Iff.mpr, Not, Classical.or_iff_not_imp_left, False.elim, LT.lt.le, Bot.bot, Membership.mem
37 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma le_or_ge_of_mem_of_mem line 97 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, Membership.mem, Or, LE.le
Proof uses: Or.resolve_right, Disjoint, Set, Iff.mpr, or_assoc, le_or_ge_or_disjoint, Not, Exists, And, Set.not_disjoint_iff, Exists.intro, And.intro
25 instances, coercions and auxiliary constants left out.
lemma le_of_mem_of_mem line 100 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, LE.le, Int, s, Membership.mem
Proof uses: And.intro, Set, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, Prod.snd, Or.resolve_right, Disjoint, fundamental_dyadic, Iff.mpr, Not, Exists, And, Set.not_disjoint_iff, Exists.intro
32 instances, coercions and auxiliary constants left out.
lemma eq_or_disjoint line 103 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, Eq, Int, s, Or, Disjoint, Set
Proof uses: Or.elim, LE.le, le_or_disjoint, Eq.le, Eq.ge, Or.inl, le_antisymm, Or.inr, Disjoint.symm
28 instances, coercions and auxiliary constants left out.
lemma disjoint_of_not_le_not_le line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, Not, LE.le, Disjoint, Set
Proof uses: Int, s, Or, le_total, Classical.byContradiction, Or.resolve_right, le_or_disjoint, Disjoint.symm
29 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma subset_of_notMem_Iic_of_not_disjoint line 117 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, Not, Membership.mem, Set, Set.Iic, Disjoint, LE.le
Proof uses: Classical.byContradiction, Eq.mpr, And, Int, s, id, Eq, congrArg, propext, Grid.le_def, Iff.mpr, not_and, disjoint_of_not_le_not_le
30 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma scale_mem_Icc line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, Membership.mem, Int, Set, Set.Icc, Neg.neg, s
Proof uses: Iff.mp, And, LE.le, Set.mem_Icc, GridStructure.range_s_subset, Exists.intro, GridStructure.Grid, Eq, GridStructure.s, rfl
21 instances, coercions and auxiliary constants left out.
lemma volume_coeGrid_pos line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, LT.lt, OfNat.ofNat, ENNReal, MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume
Proof uses: HDiv.hDiv, HPow.hPow, Int, GridStructure.s, Eq.mpr, id, Eq, of_eq_true, zpow_pos, Iff.mpr, Nat.cast_pos', MeasureTheory.measure_pos_of_superset, Metric.ball, GridStructure.c, GridStructure.ball_subset_Grid, ne_of_gt, Metric.measure_ball_pos
79 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma volume_coeGrid_lt_top line 136 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, LT.lt, ENNReal, MeasureTheory.Measure, Set, MeasureTheory.MeasureSpace.volume, Top.top
Proof uses: MeasureTheory.measure_lt_top_of_subset, Metric.ball, GridStructure.c, HMul.hMul, OfNat.ofNat, HPow.hPow, Int, GridStructure.s, GridStructure.Grid_subset_ball, MeasureTheory.measure_ball_ne_top
36 instances, coercions and auxiliary constants left out.
lemma Grid.inj line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Function.Injective, Grid, Prod, Set, Int, Prod.mk, s
Proof uses: GridStructure.inj
1 instances, coercions and auxiliary constants left out.
lemma Grid.le_topCube line 143 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, LE.le, GridStructure.topCube
Proof uses: And.intro, Set, Prod.fst, Int, GridStructure.Grid, Prod.mk, GridStructure.s, Prod.snd, GridStructure.subset_topCube, LE.le.trans_eq, s, And.right, Neg.neg, scale_mem_Icc, Eq.symm, GridStructure.s_topCube
19 instances, coercions and auxiliary constants left out.
lemma Grid.isTop_topCube line 146 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, IsTop, GridStructure.Grid, GridStructure.topCube
Proof uses: Grid.le_topCube
3 instances, coercions and auxiliary constants left out.
lemma Grid.isMax_iff line 148 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, Iff, IsMax, Eq, GridStructure.topCube
Proof uses: IsTop.isMax_iff, GridStructure.Grid, Grid.isTop_topCube
4 instances, coercions and auxiliary constants left out.
def Grid.int The set I ↦ Iᵒ in the blueprint line 151 source
Source documentation
The set I ↦ Iᵒ in the blueprint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, Set
Proof uses: Metric.ball, c, HDiv.hDiv, HPow.hPow, Int, s, OfNat.ofNat
10 instances, coercions and auxiliary constants left out.
```
def int (i : Grid X) : Set X := ball (c i) (D ^ s i / 4)
…
```
Mentions: Grid, c, s
def Grid.opSize An auxiliary measure used in the well-foundedness of Ω in Lemma tile_structure line 156 source
Source documentation
An auxiliary measure used in the well-foundedness of Ω in Lemma tile_structure.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid
Proof uses: Int.toNat, HSub.hSub, Int, s
4 instances, coercions and auxiliary constants left out.
```
def opSize (i : Grid X) : ℕ := (S - s i).toNat
```
Mentions: Grid, s
lemma Grid.int_subset line 158 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: NNReal, PseudoMetricSpace, MeasureTheory.DoublingMeasure, Nat, Real, GridStructure, Grid, LE.le, Set, Grid.int
Proof uses: GridStructure.ball_subset_Grid
2 instances, coercions and auxiliary constants left out.
lemma Grid.c_mem_Grid line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Membership.mem, c
Proof uses: NeZero, NeZero.of_pos, LT.lt.trans_le, OfNat.ofNat, zero_lt_one, one_le_realD, Ne, Set.mem_of_mem_of_subset, Metric.ball, HDiv.hDiv, HPow.hPow, GridStructure.s, Metric.mem_ball_self, div_pos, zpow_pos, lt_of_le_of_ne', Nat.cast_nonneg', Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 4 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Grid.nonempty line 182 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Set.Nonempty
Proof uses: Exists.intro, Membership.mem, c, Grid.c_mem_Grid
23 instances, coercions and auxiliary constants left out.
lemma Grid.scale_eq_scale_topCube_iff line 184 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Iff, Eq, s, GridStructure.topCube
Proof uses: Iff.intro, Or.resolve_right, Disjoint, eq_or_disjoint, Iff.mpr, Not, Exists, And, Membership.mem, Set.not_disjoint_iff, Exists.intro, c, And.intro, Grid.c_mem_Grid, GridStructure.subset_topCube, Eq.rec, rfl
39 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Grid.scale_lt_scale_topCube line 188 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Ne, GridStructure.topCube, LT.lt, s
Proof uses: LE.le, Eq.mpr, GridStructure.s, id, Eq, congrArg, s.eq_1, GridStructure.s_topCube, And.right, Neg.neg, scale_mem_Icc, LE.le.lt_of_ne, Not, ne_eq, propext, Grid.scale_eq_scale_topCube_iff
31 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Grid.eq_topCube_of_S_eq_zero line 193 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Eq, OfNat.ofNat, GridStructure.topCube
Proof uses: s, id, Eq.mp, Membership.mem, Set.Icc, Neg.neg, HPow.hPow, HMul.hMul, 𝕔, Eq.trans, Singleton.singleton, congrFun', congrArg, congr, CharP.cast_eq_zero, neg_zero, Set.Icc_self, scale_mem_Icc, Eq.mpr, Eq.symm and 3 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Grid.le_dyadic line 198 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, LE.le, s
Proof uses: Membership.mem, Set.Nonempty, Grid.nonempty, le_of_mem_of_mem, Set.mem_of_mem_of_subset, And.left, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, Prod.snd
41 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Grid.lt_def line 202 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Iff, LT.lt, And, LE.le, s
Proof uses: Iff.intro, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, Prod.snd, LT.lt.le, And.intro, lt_of_le_of_ne, id, Ne, Eq, LT.lt.trans_le, Grid.le_dyadic, Eq.ge, le_rfl, Eq.mp, False, congrArg, propext and 5 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma Grid.isMin_iff line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Iff, IsMin, Eq, s, Neg.neg
Proof uses: Iff.intro, le_antisymm, Mathlib.Tactic.Contrapose.contrapose₁, LE.le, Eq.mpr, Not, LT.lt, id, implies_congr, Eq.refl, Membership.mem, Set.Ico, of_eq_true, HPow.hPow, OfNat.ofNat, HMul.hMul, 𝕔, Eq.trans, And, True and 33 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
lemma Grid.exists_unique_succ There exists a unique successor of each non-maximal cube line 235 source
Source documentation
There exists a unique successor of each non-maximal cube.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Not, IsMax, ExistsUnique, And, Membership.mem and 4 more
Proof uses: Eq.mpr, True, id, Eq, congrArg, funext, congrFun', true_and, Finset.filter, Classical.propDecidable, Finset.Nonempty, Exists.intro, GridStructure.topCube, lt_of_le_of_ne, Grid.le_topCube, Iff.mp, Iff.not, Grid.isMax_iff, Minimal, Exists and 17 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma exists_unique_succ (i : Grid X) (h : ¬IsMax i) :
    ∃! j ∈ Finset.univ, i < j ∧ ∀ j', i < j' → j ≤ j' := by
…
```
Mentions: Grid
def Grid.succ If i is not a maximal element, this is the (unique) minimal element greater than i line 254 source
Source documentation
If i is not a maximal element, this is the (unique) minimal element greater than i. This is not a SuccOrder since an element can be the successor of multiple other elements.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid
Proof uses: dite, IsMax, Classical.propDecidable, Not, Finset.choose, And, LT.lt, LE.le, Finset.univ, Grid.exists_unique_succ
28 instances, coercions and auxiliary constants left out.
```
def succ (i : Grid X) : Grid X := if h : IsMax i then i else Finset.choose (hp := exists_unique_succ i h)
…
```
Mentions: Grid, Grid.exists_unique_succ
lemma Grid.succ_spec line 258 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Not, IsMax, And, LT.lt, Grid.succ and 1 more
Proof uses: Eq.mpr, Finset.choose, Classical.propDecidable, Finset.univ, Grid.exists_unique_succ, Eq.mpr_not, False, eq_false, not_false, id, Eq, congr, congrArg, Eq.trans, dite, dite_congr, Eq.refl, dite_false, forall_congr, implies_congr and 5 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Grid.succ_unique line 263 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Not, IsMax, LT.lt, LE.le, Eq and 1 more
Proof uses: Eq.symm, ExistsUnique.unique, And, Membership.mem, Finset, Finset.univ, Grid.exists_unique_succ, And.intro, of_eq_true, HPow.hPow, OfNat.ofNat, HMul.hMul, 𝕔, Grid.succ_spec
39 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Grid.le_succ line 267 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, LE.le, Grid.succ
Proof uses: dite, IsMax, Classical.propDecidable, of_eq_true, HPow.hPow, OfNat.ofNat, HMul.hMul, 𝕔, Eq.trans, True, congrArg, dite_eq_left_of_eq_true, Not, Finset.choose, And, LT.lt, Finset.univ, Grid.exists_unique_succ, eq_true, LT.lt.le and 2 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Grid.max_of_le_succ line 272 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, LE.le, Grid.succ, IsMax
Proof uses: Mathlib.Tactic.Contrapose.contrapose₁, Not, id, LT.lt, LT.lt.trans_le, And.left, Grid.succ_spec, Eq.mp, False, congrArg, propext, lt_self_iff_false
27 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Grid.not_isMax_of_scale_lt line 276 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, LT.lt, s, Not, IsMax
Proof uses: Eq.mpr, Eq, GridStructure.topCube, id, congrArg, propext, Grid.isMax_iff, False.elim, False, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat, Eq.mp, HAdd.hAdd, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast and 41 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Grid.succ_le_of_lt line 282 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, LT.lt, LE.le, Grid.succ
Proof uses: dite, IsMax, Classical.propDecidable, Eq.mpr, id, Eq, congrFun', congrArg, Eq.trans, Not, Finset.choose, And, Finset.univ, Grid.exists_unique_succ, True, Eq.mpr_not, eq_true, dite_congr, Eq.refl, dite_true and 3 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Grid.exists_containing_subcube line 287 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Membership.mem, Set.Icc, Neg.neg, s, Exists and 2 more
Proof uses: LE.le, LT.lt, Or, LE.le.eq_or_lt, Exists.intro, And.intro, Eq.symm, id, Eq.mp, Set.iUnion, GridStructure.Grid, Set.preimage, GridStructure.s, Singleton.singleton, HPow.hPow, OfNat.ofNat, HMul.hMul, 𝕔, Eq.trans, congrArg and 2 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Grid.exists_supercube line 295 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Membership.mem, Set.Icc, s, Exists, And and 2 more
Proof uses: LT.lt, Or, LE.le.eq_or_lt, Exists.intro, GridStructure.topCube, And.intro, Eq.mpr, HPow.hPow, OfNat.ofNat, HMul.hMul, 𝕔, id, congrArg, GridStructure.s_topCube, Grid.le_topCube, Set.Nonempty, Grid.nonempty, Neg.neg, scale_mem_Icc, Set.iUnion and 23 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Grid.exists_sandwiched line 307 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, LE.le, Membership.mem, Set.Icc, s, Exists and 2 more
Proof uses: Neg.neg, scale_mem_Icc, Grid.exists_supercube, id, Eq.mp, congrArg, propext, Set.mem_Icc, Exists.intro, And.intro, Grid.le_dyadic
45 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma Grid.scale_succ line 315 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Not, IsMax, Eq, s, Grid.succ and 2 more
Proof uses: LT.lt, LE.le, And, Grid.succ_spec, le_antisymm, Decidable.byContradiction, Exists, False, Grid.exists_sandwiched, Grid.le_succ, Eq.mpr, Membership.mem, Set.Icc, id, congrArg, propext, Set.mem_Icc, Eq.mp, LT.lt.trans_le, Iff.mpr and 11 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Grid.exists_scale_succ line 324 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, LT.lt, s, Exists, And, LE.le and 3 more
Proof uses: Exists.intro, Grid.succ, And.intro, Grid.le_succ, Grid.scale_succ, Grid.not_isMax_of_scale_lt
34 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Grid.opSize_succ_lt line 330 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Not, IsMax, LT.lt, Grid.opSize, Grid.succ
Proof uses: Eq.mpr, Int.toNat, HSub.hSub, s, id, Eq, LE.le, And.right, Neg.neg, Iff.mp, Membership.mem, Set.Icc, And, Set.mem_Icc, scale_mem_Icc, OfNat.ofNat, congrArg, Int.toNat_of_nonneg, HAdd.hAdd, Grid.scale_succ
46 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Grid.induction line 338 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, IsMax, Not, Grid.succ
Proof uses: WellFounded.Nat.fix, Grid.opSize, InvImage, LT.lt, dite, Classical.propDecidable, Grid.opSize_succ_lt, id
27 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Grid.succ_def line 346 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Not, IsMax, Iff, Eq, Grid.succ and 5 more
Proof uses: Iff.intro, And.intro, Grid.le_succ, Grid.scale_succ, LT.lt, Iff.mpr, Grid.lt_def, And.left, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, Prod.snd, Grid.succ_unique, And.right, Iff.mp, Grid.le_dyadic, LT.lt.le
50 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
def Grid.maxCubes line 356 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Finset, Grid
Proof uses: Finset.filter, Membership.mem, LE.le, Eq, Classical.propDecidable
29 instances, coercions and auxiliary constants left out.
lemma Grid.exists_maximal_supercube line 358 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, Finset, Membership.mem, Exists, And, Grid.maxCubes and 1 more
Proof uses: Maximal, Finset.exists_le_maximal, id, Eq.mpr, Finset.filter, Eq, Classical.propDecidable, congrArg, funext, congrFun', Exists.intro, And.intro, Eq.mp, propext, maximal_iff
37 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Grid.maxCubes_pairwiseDisjoint line 362 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Finset, Grid, Set.PairwiseDisjoint, Grid.maxCubes
Proof uses: Membership.mem, Ne, Or.resolve_left, LE.le, Disjoint, Or, le_or_ge_or_disjoint, Function.mt, Eq, And.right, Eq.mp, And, congrFun', Set.ofPred, congrArg, Finset.coe_filter, Classical.propDecidable, And.left, Ne.symm
53 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def Grid._root_.C2_1_2 The constant appearing in Lemma 2.1.2, 2 ^ {-95a} line 371 source
Source documentation
The constant appearing in Lemma 2.1.2, 2 ^ {-95a}.
```
def _root_.C2_1_2 (a : ℕ) : ℝ := 2 ^ ((-𝕔 + 5) * a : ℝ)
…
```
lemma Grid._root_.C2_1_2_le_inv_256 line 375 source
lemma Grid._root_.C2_1_2_le_one line 386 source
lemma Grid._root_.C2_1_2_lt_one line 391 source
lemma Grid.dist_strictMono Stronger version of Lemma 2.1.2 line 397 source
Source documentation
Stronger version of Lemma 2.1.2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, LT.lt, FunctionDistances.Θ, LE.le, Dist.dist, WithFunctionDistance and 7 more
Proof uses: Trans.trans, Eq, HAdd.hAdd, Neg.neg, 𝕔, CompatibleFunctions.cdist_mono, Metric.ball_subset_ball, Eq.mpr, Inv.inv, id, congrFun', congrArg, div_eq_inv_mul, mul_le_mul_of_nonneg_right, Mathlib.Meta.NormNum.isRat_le_true, Int.ofNat, Mathlib.Meta.NormNum.IsNNRat.to_isRat, Mathlib.Meta.NormNum.isNNRat_inv_pos, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat and 143 more
208 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
lemma dist_strictMono {I J : Grid X} (hpq : I < J) {f g : Θ X} :
    dist_{I} f g ≤ C2_1_2 a * dist_{J} f g := by
…
```
Mentions: Grid, g
lemma Grid.dist_mono Weaker version of Lemma 2.1.2 line 434 source
Source documentation
Weaker version of Lemma 2.1.2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, LE.le, FunctionDistances.Θ, Dist.dist, WithFunctionDistance, c and 4 more
Proof uses: Eq, LT.lt, Or, LE.le.eq_or_lt, le_refl, LE.le.trans, HMul.hMul, C2_1_2, Grid.dist_strictMono, mul_le_of_le_one_left, dist_nonneg, C2_1_2_le_one
77 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma dist_mono {I J : Grid X} (hpq : I ≤ J) {f g : Θ X} : dist_{I} f g ≤ dist_{J} f g := by
…
```
Mentions: Grid, g
lemma Grid.dist_strictMono_iterate line 439 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, LE.le, Eq, HAdd.hAdd, s, FunctionDistances.Θ and 8 more
Proof uses: Nat.recAux, Eq.mpr, 𝕔, id, congrArg, Eq.trans, congrFun', pow_zero, one_mul, Grid.dist_mono, And, Exists, Grid.exists_sandwiched, Membership.mem, Set.Icc, propext, Set.mem_Icc, LT.lt, Grid.lt_def, And.intro and 49 more
140 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma Grid.dist_strictMono_iterate' Version of dist_strictMono_iterate with d in ℤ line 455 source
Source comment
Version of `dist_strictMono_iterate` with `d` in `ℤ`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, GE.ge, OfNat.ofNat, LE.le, Eq, HAdd.hAdd and 9 more
Proof uses: Eq.mpr, Int.toNat, id, congrArg, Eq.symm, Int.toNat_of_nonneg, Grid.dist_strictMono_iterate, Eq.mp
77 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma dist_strictMono_iterate' {I J : Grid X} {d : ℤ} (hd : d ≥ 0) (hij : I ≤ J)
    (hs : s I + d = s J) {f g : Θ X} : dist_{I} f g ≤ C2_1_2 a ^ d * dist_{J} f g := by
…
```
Mentions: Grid, d, s, g
lemma Grid.dist_c_le_of_subset line 460 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, GridStructure, NNReal, defaultA, defaultD, defaultκ, defaultS, cancelPt, Grid, LE.le, LT.lt, Dist.dist, c, HMul.hMul and 3 more
Proof uses: GridStructure.Grid_subset_ball, Grid.c_mem_Grid
37 instances, coercions and auxiliary constants left out.