AntichainTileCount.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

69 declarations, 0 contain sorry, 0 declared as axioms

6.3. Proof of the Antichain Tile Count Lemma

This file contains the proofs of lemmas 6.3.1, 6.3.2, 6.3.3, 6.3.4 and 6.1.6 from the blueprint.

Main results

Antichain.tile_reach: Lemma 6.3.1.
Antichain.stack_density: Lemma 6.3.2.
Antichain.local_antichain_density : Lemma 6.3.3.
Antichain.global_antichain_density : Lemma 6.3.4.
Antichain.tile_count: Lemma 6.1.6.

Imports (1)

Carleson.Antichain.Basic

Imported by 2 files

lemma Antichain.tile_reach Lemma 6.3.1 line 36 source
Source documentation
Lemma 6.3.1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, FunctionDistances.Θ, 𝔓, LE.le, Dist.dist, WithFunctionDistance and 12 more
Proof uses: Eq.mpr, id, Eq, congrArg, dist_comm, le_trans, c, s, Grid.dist_mono, Trans.trans, rfl, dist_triangle, add_le_add, Mathlib.Tactic.Ring.of_eq, HMul.hMul, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 191 more
287 instances, coercions and auxiliary constants left out.

Tactic trace: 84 steps
Open to load the checked before-and-after goal states.
```
lemma tile_reach {ϑ : Θ X} {N : ℕ} {p p' : 𝔓 X} (hp : dist_(p) (𝒬 p) ϑ ≤ 2 ^ N)
    (hp' : dist_(p') (𝒬 p') ϑ ≤ 2 ^ N) (hI : 𝓘 p ≤ 𝓘 p') (hs : 𝔰 p < 𝔰 p') :
    smul (2^(N + 2)) p ≤ smul (2^(N + 2)) p' := by
…
```
Mentions: Antichain.p', 𝔓, 𝓘, 𝔰, smul
def Antichain.𝔄_aux Def 6.3.15 line 133 source
Source documentation
Def 6.3.15.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ
Proof uses: Set.ofPred, And, Membership.mem, Set.Ico, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Dist.dist, WithFunctionDistance, 𝔠, HDiv.hDiv, 𝔰, PreTileStructure.𝒬
57 instances, coercions and auxiliary constants left out.
```
def 𝔄_aux (𝔄 : Set (𝔓 X)) (ϑ : Θ X) (N : ℕ) : Set (𝔓 X) :=
…
```
Mentions: 𝔓
lemma Antichain.pairwiseDisjoint_𝔄_aux line 138 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.PairwiseDisjoint, Finset, Set.univ and 4 more
Proof uses: Ne, id, Function.onFun, Disjoint, LT.lt, Not, Or, Classical.em, Eq.mpr, Eq, Set.ofPred, And, Set.Ico, HPow.hPow, OfNat.ofNat, HAdd.hAdd, Dist.dist, WithFunctionDistance, 𝔠, HDiv.hDiv and 18 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma Antichain.biUnion_𝔄_aux line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Exists, Eq, Finset and 6 more
Proof uses: EmptyCollection.emptyCollection, Set.Nonempty, Or, Set.eq_empty_or_nonempty, Exists.intro, OfNat.ofNat, of_eq_true, Eq.trans, True, congrArg, Set.toFinset_empty, eq_self, Eq.symm, Nat.floor, Real.logb, HAdd.hAdd, Dist.dist, WithFunctionDistance, 𝔠, HDiv.hDiv and 55 more
125 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
lemma Antichain.stack_density Lemma 6.3.2 line 175 source
Source documentation
Lemma 6.3.2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Grid, LE.le, ENNReal and 17 more
Proof uses: Set.ofPred, And, rfl, Eq.mpr, id, congrArg, And.right, Set.Ico, Dist.dist, WithFunctionDistance, 𝔠, HDiv.hDiv, 𝔰, PreTileStructure.𝒬, Eq.mp, congrFun', Eq.refl, AddCommMonoid, Finset, Eq.rec and 176 more
297 instances, coercions and auxiliary constants left out.

Tactic trace: 112 steps
Open to load the checked before-and-after goal states.
```
lemma stack_density (𝔄 : Set (𝔓 X)) (ϑ : Θ X) (N : ℕ) (L : Grid X) :
    ∑ p ∈ 𝔄_aux 𝔄 ϑ N with 𝓘 p = L, volume (E p ∩ G) ≤
      2^(a * (N + 5)) * dens₁ (𝔄 : Set (𝔓 X)) * volume (L : Set X) := by
…
```
Mentions: 𝔓, Grid, Antichain.𝔄_aux, 𝓘, E, dens₁
lemma Antichain.Ep_inter_G_inter_Ip'_subset_E2 We prove inclusion 6.3.24 for every p ∈ (𝔄_aux 𝔄 ϑ N) with 𝔰 p' < 𝔰 p such that (𝓘 p : Set X) ∩ (𝓘 p') ≠ ∅ line 301 source
Source documentation
We prove inclusion 6.3.24 for every p ∈ (𝔄_aux 𝔄 ϑ N) with 𝔰 p' < 𝔰 p such that (𝓘 p : Set X) ∩ (𝓘 p') ≠ ∅. The variable p' corresponds to 𝔭_ϑ in the blueprint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Membership.mem, Finset, Set.toFinset and 18 more
Proof uses: Grid, And.intro, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, Prod.snd, Or.resolve_right, Disjoint, fundamental_dyadic, le_of_lt, s, Iff.mpr, Not, Set.not_disjoint_iff_nonempty_inter, Dist.dist, LT.lt.trans, lt_one_add, And.right, And and 43 more
176 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma Ep_inter_G_inter_Ip'_subset_E2 {𝔄 : Set (𝔓 X)} (ϑ : Θ X) (N : ℕ) {p p' : 𝔓 X}
    (hpin : p ∈ (𝔄_aux 𝔄 ϑ N).toFinset) (hp' : ϑ ∈ ball_(p') (𝒬 p') (2 ^ (N + 1)))
    (hs : 𝔰 p' < 𝔰 p) (h𝓘 : ((𝓘 p' : Set X) ∩ (𝓘 p)).Nonempty) :
    E p ∩ G ∩ ↑(𝓘 p') ⊆ E₂ (2^(N + 3)) p' := by
…
```
Mentions: 𝔓, Antichain.p', Antichain.𝔄_aux, 𝔰, 𝓘, E, E₂
lemma Antichain.local_antichain_density Lemma 6.3.3 line 329 source
Source documentation
Lemma 6.3.3.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, IsAntichain, LE.le, FunctionDistances.Θ, Membership.mem and 22 more
Proof uses: Eq.mpr, Set.iUnion, Finset, id, Eq, congrArg, Eq.symm, MeasureTheory.measure_biUnion_finset, Set.PairwiseDisjoint, Set.ofPred, And, congrFun', Finset.coe_filter, Ne, Disjoint, Eq.mp, Not, Function.mt, tile_disjointness, And.left and 39 more
139 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma local_antichain_density {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ ·) 𝔄) (ϑ : Θ X) (N : ℕ)
    {p' : 𝔓 X} (hp' : ϑ ∈ ball_(p') (𝒬 p') (2 ^ (N + 1))) :
    ∑ p ∈ 𝔄_aux 𝔄 ϑ N with 𝔰 p' < 𝔰 p, volume (E p ∩ G ∩ 𝓘 p') ≤
      volume (E₂ (2 ^ (N + 3)) p') := by
…
```
Mentions: 𝔓, Antichain.p', Antichain.𝔄_aux, 𝔰, E, 𝓘, E₂
def Antichain.C6_3_4 The constant appearing in Lemma 6.3.4 line 354 source
Source documentation
The constant appearing in Lemma 6.3.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal
Proof uses: HPow.hPow, OfNat.ofNat, HAdd.hAdd, HMul.hMul, 𝕔
17 instances, coercions and auxiliary constants left out.
```
def C6_3_4 (a N : ℕ) : ℝ≥0 := 2 ^ ((𝕔 + 1) * a ^ 3 + N * a)
```
def Antichain.C6_3_4' Auxiliary constant for Lemma 6.3.4 line 357 source
Source documentation
Auxiliary constant for Lemma 6.3.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal
Proof uses: HMul.hMul, HAdd.hAdd, HPow.hPow, OfNat.ofNat, 𝕔
20 instances, coercions and auxiliary constants left out.
```
def C6_3_4' (a N : ℕ) : ℝ≥0 := ((2 ^ (a * (N + 5)) + 2 ^ (a * N + a * 3)) * 2 ^ (𝕔 * a^3 + 5 * a))
…
```
def Antichain.𝔄' The set 𝔄' defined in Lemma 6.3.4 line 362 source
Source documentation
The set 𝔄' defined in Lemma 6.3.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc
Proof uses: Set.ofPred, And, Membership.mem, Antichain.𝔄_aux, Ne, Inter.inter, 𝓘, EmptyCollection.emptyCollection, GT.gt, 𝔰, Neg.neg
53 instances, coercions and auxiliary constants left out.
```
def 𝔄' : Set (𝔓 X) := {p ∈ 𝔄_aux 𝔄 ϑ N | ((𝓘 p : Set X) ∩ G) ≠ ∅ ∧ 𝔰 p > -S}
```
Mentions: 𝔓, Antichain.𝔄_aux, 𝓘, 𝔰
def Antichain.𝔄_min The set 𝔄_-S defined in Lemma 6.3.4 line 365 source
Source documentation
The set 𝔄_-S defined in Lemma 6.3.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc
Proof uses: Set.ofPred, And, Membership.mem, Antichain.𝔄_aux, Ne, Inter.inter, 𝓘, EmptyCollection.emptyCollection, Eq, 𝔰, Neg.neg
52 instances, coercions and auxiliary constants left out.
```
def 𝔄_min : Set (𝔓 X) := {p ∈ 𝔄_aux 𝔄 ϑ N | ((𝓘 p : Set X) ∩ G) ≠ ∅ ∧ 𝔰 p = -S}
…
```
Mentions: 𝔓, Antichain.𝔄_aux, 𝓘, 𝔰
lemma Antichain.𝔄_aux_sum_splits line 369 source
def Antichain.𝓛_min The set 𝓛_{-S} defined in Lemma 6.3.4 line 393 source
Source documentation
The set 𝓛_{-S} defined in Lemma 6.3.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid
Proof uses: Set.ofPred, Exists, Antichain.𝔄_min, Eq, 𝓘, Membership.mem
48 instances, coercions and auxiliary constants left out.
```
def 𝓛_min : Set (Grid X) := {I : Grid X | ∃ (p : 𝔄_min 𝔄 ϑ N), I = 𝓘 (p : 𝔓 X)}
…
```
Mentions: Grid, Antichain.𝔄_min, 𝓘, 𝔓
lemma Antichain.𝔄_min_sum_le line 398 source
def Antichain.𝓛 The set 𝓛 defined in Lemma 6.3.4 line 449 source
Source documentation
The set 𝓛 defined in Lemma 6.3.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid
Proof uses: Set.ofPred, And, Exists, Antichain.𝔄', LE.le, 𝓘, Membership.mem, Eq, 𝔰, Neg.neg
53 instances, coercions and auxiliary constants left out.
```
def 𝓛 : Set (Grid X) := {I : Grid X | (∃ (p : 𝔄' 𝔄 ϑ N), I ≤ 𝓘 (p : 𝔓 X)) ∧
…
```
Mentions: Grid, Antichain.𝔄', 𝓘, 𝔓
lemma Antichain.I_p_subset_union_L Ineq line 454 source
Source comment
Ineq. 6.3.27

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Antichain.𝔄' and 6 more
Proof uses: Trans.trans, Set.ofPred, And, Eq, s, Neg.neg, rfl, Exists, Grid.exists_containing_subcube, of_eq_true, Set.Icc, HPow.hPow, OfNat.ofNat, HMul.hMul, 𝕔, Eq.trans, True, congr, congrArg, PseudoMetricSpace and 37 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma I_p_subset_union_L (p : 𝔄' 𝔄 ϑ N) : (𝓘 (p : 𝔓 X) : Set X) ⊆ ⋃ (L ∈ 𝓛 𝔄 ϑ N), L := by
…
```
Mentions: Antichain.𝔄', 𝓘, 𝔓, Antichain.𝓛
lemma Antichain.union_L_eq_union_I_p Ineq line 473 source
Source comment
Ineq. 6.3.28

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Eq and 6 more
Proof uses: le_antisymm, Eq.mpr, Exists, id, Eq.trans, congrArg, funext, Eq.mp, LE.le, And.left, 𝔰, Neg.neg, Exists.intro, Subtype.property, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, Prod.snd, And and 2 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma union_L_eq_union_I_p : ⋃ (L ∈ 𝓛 𝔄 ϑ N), L = ⋃ (p ∈ 𝔄' 𝔄 ϑ N), (𝓘 (p : 𝔓 X) : Set X) := by
…
```
Mentions: Antichain.𝓛, Antichain.𝔄', 𝓘, 𝔓
def Antichain.𝓛' The set 𝓛* defined in Lemma 6.3.4 line 486 source
Source documentation
The set 𝓛* defined in Lemma 6.3.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid
Proof uses: Set.ofPred, Maximal, Membership.mem, Antichain.𝓛
50 instances, coercions and auxiliary constants left out.
```
def 𝓛' : Set (Grid X) := {I : Grid X | Maximal (· ∈ 𝓛 𝔄 ϑ N) I}
…
```
Mentions: Grid, Antichain.𝓛
lemma Antichain.pairwiseDisjoint_𝓛' line 489 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Set.PairwiseDisjoint and 6 more
Proof uses: Ne, IsAntichain, LE.le, setOfPred_maximal_antichain, Antichain.𝓛, Or.resolve_left, Disjoint, Or, le_or_ge_or_disjoint, Iff.mp, Set.mem_toFinset, Ne.symm
80 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Antichain.union_L'_eq_union_I_p Eq. 6.3.29 line 498 source
Source comment
Eq. 6.3.29

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Eq and 6 more
Proof uses: Eq.mpr, Antichain.𝓛, id, congrArg, Eq.symm, Antichain.union_L_eq_union_I_p, le_antisymm, LE.le, HPow.hPow, OfNat.ofNat, HMul.hMul, 𝕔, Eq.trans, forall_congr, Set.subset_biUnion_of_mem, And.left, Exists, And, funext, Eq.mp and 16 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma union_L'_eq_union_I_p : ⋃ (L ∈ 𝓛' 𝔄 ϑ N), L = ⋃ (p ∈ 𝔄' 𝔄 ϑ N), (𝓘 (p : 𝔓 X) : Set X) := by
…
```
Mentions: Antichain.𝓛', Antichain.𝔄', 𝓘, 𝔓
lemma Antichain.exists_p'_ge_L line 524 source
lemma Antichain.SL_nonempty line 528 source
def Antichain.p' p' in the blueprint line 535 source
Source documentation
p' in the blueprint.
```
private def p' : 𝔓 X :=(Finset.exists_minimalFor 𝔰 (SL 𝔄 ϑ N L).toFinset (SL_nonempty hL)).choose
…
```
Mentions: 𝔓, 𝔰, Antichain.SL_nonempty
lemma Antichain.p'_mem line 538 source
lemma Antichain.L_le_I_p' line 542 source
lemma Antichain.not_I_p'_le_L line 548 source
lemma Antichain.s_L_le_s_p' line 563 source
lemma Antichain.exists_larger_grid line 573 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid and 9 more
Proof uses: Antichain.𝔄', 𝓘, Finset, Set.toFinset, Classical.propDecidable, rfl, Finset.Nonempty, And.left, Exists.choose, MinimalFor, 𝔰, Finset.exists_minimalFor, Exists.choose_spec, Not, LT.lt, GridStructure.topCube, Eq.mpr, id, Eq.rec, Eq.refl and 8 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
def Antichain.L' The L' introduced in the proof of Lemma 6.3.4 line 590 source
Source documentation
The L' introduced in the proof of Lemma 6.3.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid and 2 more
Proof uses: Exists.choose, And, LE.le, Eq, s, HAdd.hAdd, OfNat.ofNat, Antichain.exists_larger_grid
54 instances, coercions and auxiliary constants left out.
```
def L' : Grid X := (exists_larger_grid hL).choose
```
Mentions: Grid, Antichain.exists_larger_grid
lemma Antichain.L_le_L' line 592 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid and 4 more
Proof uses: And.left, Exists.choose, And, Eq, s, HAdd.hAdd, OfNat.ofNat, Antichain.exists_larger_grid, Exists.choose_spec
57 instances, coercions and auxiliary constants left out.
lemma Antichain.s_L'_eq line 594 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid and 7 more
Proof uses: And.right, LE.le, Exists.choose, And, Antichain.exists_larger_grid, Exists.choose_spec
57 instances, coercions and auxiliary constants left out.
lemma Antichain.c_L_mem line 596 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid and 4 more
Proof uses: And.left, LE.le, Prod.fst, GridStructure.Grid, Prod.mk, GridStructure.s, Prod.snd, Antichain.L_le_L', Grid.c_mem_Grid
62 instances, coercions and auxiliary constants left out.
lemma Antichain.L'_not_mem line 598 source
lemma Antichain.L'_le_I_p' line 605 source
lemma Antichain.exists_p''_le_L' line 618 source
def Antichain.p'' p'' in the blueprint line 631 source
Source documentation
p'' in the blueprint

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid and 2 more
Proof uses: Exists.choose, And, Antichain.𝔄', LE.le, 𝓘, Antichain.L'
52 instances, coercions and auxiliary constants left out.
```
@[no_expose] def p'' : 𝔓 X := (exists_p''_le_L' hL).choose
```
Mentions: 𝔓, Antichain.exists_p''_le_L'
lemma Antichain.p''_mem p'' in the blueprint line 633 source
Source documentation
p'' in the blueprint

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid and 4 more
Proof uses: And.left, Exists.choose, And, LE.le, 𝓘, Antichain.L', Exists.choose_spec
52 instances, coercions and auxiliary constants left out.
```
lemma p''_mem : p'' hL ∈ 𝔄' 𝔄 ϑ N := (exists_p''_le_L' hL).choose_spec.1
```
Mentions: Antichain.p'', Antichain.𝔄', Antichain.exists_p''_le_L'
lemma Antichain.I_p''_le_L' line 635 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid and 6 more
Proof uses: And.right, Antichain.𝔄', Exists.choose, And, Exists.choose_spec
55 instances, coercions and auxiliary constants left out.
lemma Antichain.exists_pΘ_eq_L' line 637 source
def Antichain.pΘ p_Θ in the blueprint line 650 source
Source documentation
p_Θ in the blueprint

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid and 2 more
Proof uses: ite, Eq, 𝓘, Antichain.p'', Antichain.L', Classical.propDecidable, Exists.choose, And, TileStructure.Ω
51 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
@[no_expose] def pΘ : 𝔓 X := by
…
```
Mentions: 𝔓
lemma Antichain.I_pΘ_eq_L' line 653 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid and 6 more
Proof uses: id, dite, ite, Antichain.p'', Classical.propDecidable, Exists.choose, And, TileStructure.Ω, Eq.mpr, congrFun', congrArg, ite_eq_left, Not, ite_eq_right, And.left, Exists.choose_spec
51 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma Antichain.theta_mem_Omega_pΘ line 659 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid and 9 more
Proof uses: Eq.mpr, Exists.choose, And, id, congrFun', congrArg, Decidable, ite_eq_right, Classical.propDecidable, And.right, And.left, Exists.choose_spec
53 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Antichain.pΘ_unique line 663 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid and 10 more
Proof uses: Eq.mpr, Exists.choose, id, forall_congr, implies_congr, Eq.refl, congrArg, Decidable, ite_eq_right, Classical.propDecidable, And.right, Exists.choose_spec
53 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Antichain.eq_6_3_35 Eq. 6.3.35 line 670 source
Source comment
Eq. 6.3.35
```
private lemma eq_6_3_35 : ϑ.val ∈ ball_(p'' hL) (𝒬 (p'' hL)) (2 ^ (N + 1)) := by
…
```
Mentions: Antichain.p''
lemma Antichain.eq_6_3_37 Eq. 6.3.37 line 678 source
Source comment
Eq. 6.3.37
```
private lemma eq_6_3_37 : ϑ.val ∈ ball_(pΘ hL) (𝒬 (pΘ hL)) (2 ^ (N + 1)) := by
…
```
Mentions: Antichain.pΘ
lemma Antichain.ineq_6_3_36 Ineq line 688 source
Source comment
Ineq. 6.3.36
```
private lemma ineq_6_3_36 : smul (2^(N + 3)) (p'' hL) ≤ smul (2^(N + 3)) (pΘ hL) := by
…
```
Mentions: smul, Antichain.p'', Antichain.pΘ

lemma Antichain.ineq_6_3_38 Ineq line 703 source

Source comment

Ineq. 6.3.38

private lemma ineq_6_3_38 : volume (E₂ (2 ^ (N + 3)) (pΘ hL)) ≤
      2 ^ (a * N + a * 3) * (dens₁ (𝔄 : Set (𝔓 X)) * volume (L' hL : Set X)) := by
…

Mentions: E₂, Antichain.pΘ, dens₁, 𝔓, Antichain.L'

lemma Antichain.ineq_6_3_39 line 719 source

lemma Antichain.volume_L'_le Ineq line 784 source

Source comment

Ineq. 6.3.41

private lemma volume_L'_le :
    volume (L' hL : Set X) ≤ 2 ^ (𝕔 * a^3 + 5*a) * volume (L : Set X) := by
…

Mentions: Antichain.L'

lemma Antichain.global_antichain_density_aux line 812 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, FunctionDistances.Θ, Set.range, MeasureTheory.SimpleFunc, Grid and 16 more
Proof uses: Trans.trans, Eq, HAdd.hAdd, HPow.hPow, OfNat.ofNat, 𝕔, Antichain.L', E₂, Antichain.pΘ, Finset.filter, Not, 𝓘, rfl, Eq.mpr, id, congrArg, Eq.symm, Finset.sum_filter_add_sum_filter_not, Eq.refl, add_le_add and 55 more
140 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Antichain.volume_union_I_p_eq_sum line 857 source
lemma Antichain.lhs' line 866 source
lemma Antichain.lhs line 896 source
lemma Antichain.le_C6_3_4 line 905 source
lemma Antichain.global_antichain_density Lemma 6.3.4 line 915 source
Source documentation
Lemma 6.3.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, IsAntichain, LE.le, FunctionDistances.Θ, Set.range and 16 more
Proof uses: Eq.mpr, HAdd.hAdd, Grid, Antichain.𝓛', Antichain.𝔄', Antichain.𝔄_min, id, Eq, congrArg, Trans.trans, Antichain.C6_3_4', HPow.hPow, OfNat.ofNat, rfl, add_le_add, Finset.sum_le_sum, Finset, Antichain.global_antichain_density_aux, Iff.mp, Set.mem_toFinset and 25 more
145 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma global_antichain_density {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ ·) 𝔄) (ϑ : range Q) (N : ℕ) :
    ∑ p ∈ (𝔄_aux 𝔄 ϑ.val N).toFinset, volume (E p ∩ G) ≤
      C6_3_4 a N * dens₁ (𝔄 : Set (𝔓 X)) * volume (⋃ p ∈ 𝔄, (𝓘 p : Set X)) := by
…
```
Mentions: 𝔓, Antichain.𝔄_aux, E, Antichain.C6_3_4, dens₁, 𝓘
def Antichain.p₆ p in Lemma 6.1.6 line 941 source
Source documentation
p in Lemma 6.1.6. We append a subscript ₆ to keep p available for tiles.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: HMul.hMul, OfNat.ofNat, HPow.hPow
11 instances, coercions and auxiliary constants left out.
```
def p₆ (a : ℕ) : ℝ := 4 * a ^ 4
```
def Antichain.q₆ p' in the proof of Lemma 6.1.4, the Hölder conjugate exponent of p₆ line 944 source
Source documentation
p' in the proof of Lemma 6.1.4, the Hölder conjugate exponent of p₆.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real
Proof uses: Inv.inv, HSub.hSub, OfNat.ofNat, Antichain.p₆
5 instances, coercions and auxiliary constants left out.
```
def q₆ (a : ℕ) : ℝ := (1 - (p₆ a)⁻¹)⁻¹
```
Mentions: Antichain.p₆
lemma Antichain.p₆_ge_1024 line 946 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Real, Antichain.p₆
Proof uses: id, Eq.mpr, HMul.hMul, HPow.hPow, Eq, Eq.trans, congrArg, Trans.trans, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.isNat_mul, Mathlib.Meta.NormNum.isNat_pow, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.trans, Nat.pow, Mathlib.Meta.NormNum.IsNatPowT.bit0, mul_le_mul', le_refl, pow_le_pow_left'
56 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma Antichain.one_lt_p₆ line 952 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Real, Antichain.p₆
Proof uses: lt_of_lt_of_le, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false, Antichain.p₆_ge_1024
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Antichain.p₆_pos line 954 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Real, Antichain.p₆
Proof uses: lt_of_lt_of_le, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.false, Antichain.p₆_ge_1024
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Antichain.holderConjugate_p₆ line 956 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Real.HolderConjugate, Antichain.p₆, Antichain.q₆
Proof uses: Eq.mpr, Eq, Real, HDiv.hDiv, HSub.hSub, id, congrArg, propext, Real.holderConjugate_iff_eq_conjExponent, Antichain.one_lt_p₆, Inv.inv, Antichain.q₆.eq_1, inv_eq_iff_eq_inv, inv_div, sub_div, one_div, div_self, LT.lt.ne', LT.lt.trans, zero_lt_one and 1 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Antichain.q₆_le_superparticular line 960 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Real, Antichain.q₆, HDiv.hDiv
Proof uses: LT.lt, Inv.inv, Antichain.p₆, Eq.mpr, Or, id, Eq, congrArg, propext, inv_lt_one_iff₀, Or.inr, Antichain.one_lt_p₆, HSub.hSub, Antichain.q₆.eq_1, Mathlib.Meta.NormNum.isNNRat_eq_true, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, HMul.hMul, Eq.refl, Mathlib.Meta.NormNum.IsNat.to_isNNRat and 77 more
113 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Antichain.one_lt_q₆ line 967 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Real, Antichain.q₆
Proof uses: Real.HolderConjugate, Antichain.p₆, Real.HolderConjugate.symm, Antichain.holderConjugate_p₆, And.left, Eq, HAdd.hAdd, Inv.inv, Eq.mp, And, congrArg, propext, Real.holderConjugate_iff
13 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Antichain.q₆_pos line 971 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, Real, Antichain.q₆
Proof uses: LT.lt.trans, zero_lt_one, Antichain.one_lt_q₆
23 instances, coercions and auxiliary constants left out.
lemma Antichain.C2_0_6_q₆_le A very involved bound needed for Lemma 6.1.4 line 974 source
Source documentation
A very involved bound needed for Lemma 6.1.4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, NNReal, C2_0_6, defaultA, Real.toNNReal, Antichain.q₆, HPow.hPow, HAdd.hAdd
Proof uses: Eq.mpr, Real, CMB, HDiv.hDiv, Inv.inv, id, Eq, congrArg, C2_0_6.eq_1, Real.coe_toNNReal, LT.lt.le, Antichain.q₆_pos, of_eq_true, Eq.trans, True, Real.toNNReal_ofNat, eq_self, Eq.symm, Real.toNNReal_div, zero_le_two and 127 more
204 instances, coercions and auxiliary constants left out.

Tactic trace: 62 steps
Open to load the checked before-and-after goal states.
```
lemma C2_0_6_q₆_le (a4 : 4 ≤ a) : C2_0_6 (defaultA a) (q₆ a).toNNReal 2 ≤ 2 ^ (a + 2) := by
…
```
Mentions: defaultA, Antichain.q₆
lemma Antichain.tile_count_aux line 1021 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, IsAntichain, LE.le, FunctionDistances.Θ, Set.range and 25 more
Proof uses: KernelProofData.four_le_a, LT.lt, Antichain.p₆_pos, Eq, Real.toNNReal, Eq.refl, Eq.mpr, id, congrArg, Eq.symm, propext, ENNReal.rpow_le_rpow_iff, Eq.trans, Max.max, Or, False, or_false, MeasureTheory.lintegral, ENorm.enorm, MeasureTheory.eLpNorm_nnreal_pow_eq_lintegral and 205 more
372 instances, coercions and auxiliary constants left out.

Tactic trace: 90 steps
Open to load the checked before-and-after goal states.
def Antichain.C6_1_6 The constant appearing in Lemma 6.1.6 line 1093 source
Source documentation
The constant appearing in Lemma 6.1.6.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, NNReal
Proof uses: HPow.hPow, OfNat.ofNat, HMul.hMul
14 instances, coercions and auxiliary constants left out.
```
def C6_1_6 (a : ℕ) : ℝ≥0 := 2 ^ (5 * a)
```
lemma Antichain.le_C6_1_6 line 1095 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, ENNReal, HMul.hMul, HPow.hPow, Real, HDiv.hDiv, HAdd.hAdd, 𝕔, Antichain.p₆, Finset.sum, Finset.range, Neg.neg, Inv.inv, Antichain.C6_1_6
Proof uses: LT.lt, Antichain.p₆_pos, Trans.trans, mul_le_mul', le_refl, Eq, ENNReal.ofReal, HSub.hSub, tsum, SummationFilter.unconditional, ENNReal.sum_le_tsum, ENNReal.tsum_geometric, near_1_geometric_bound, And.intro, Eq.mpr, congrArg, propext, inv_nonneg, le_imp_le_of_le_of_le, LT.lt.le and 95 more
213 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma Antichain.tile_count Lemma 6.1.6 line 1124 source
Source documentation
Lemma 6.1.6.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Complex, Int, Set, MetricSpace, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, IsAntichain, LE.le, FunctionDistances.Θ, Set.range and 30 more
Proof uses: Eq, Finset, Finset.biUnion, Finset.range, Set.toFinset, Antichain.𝔄_aux, Exists, Antichain.biUnion_𝔄_aux, Trans.trans, 𝕔, HSub.hSub, eq_of_heq, ENorm, MeasurableSpace, autoParam, HEq, Eq.refl, HEq.refl, Eq.symm, funext and 109 more
305 instances, coercions and auxiliary constants left out.

Tactic trace: 39 steps
Open to load the checked before-and-after goal states.
```
lemma tile_count {𝔄 : Set (𝔓 X)} (h𝔄 : IsAntichain (· ≤ ·) 𝔄) (ϑ : range (Q (X := X))) :
…
```
Mentions: 𝔓