noncomputable def G12FineGrid.endpoint (ρ : ℝ) (i : ℕ) : ℕ

Rounded geometric endpoints; repeated endpoints are deliberately retained.

Equations

• G12FineGrid.endpoint ρ i = ⌈ρ ^ i⌉₊ - 1

noncomputable def G12FineGrid.cell (ρ : ℝ) (i : ℕ) : Finset ℕ

Equations

• G12FineGrid.cell ρ i = Finset.Ioc (G12FineGrid.endpoint ρ i) (G12FineGrid.endpoint ρ (i + 1))

noncomputable def G12FineGrid.clipped (ρ : ℝ) (L H i : ℕ) : Finset ℕ

Literal clipping, with no positive-width assumption.

Equations

• G12FineGrid.clipped ρ L H i = Finset.Ioc (max L (G12FineGrid.endpoint ρ i)) (min H (G12FineGrid.endpoint ρ (i + 1)))

theorem G12FineGrid.mem_clipped (ρ : ℝ) (L H i n : ℕ) : n ∈ clipped ρ L H i ↔ n ∈ Finset.Ioc L H ∧ n ∈ cell ρ i

theorem G12FineGrid.endpoint_zero (ρ : ℝ) : endpoint ρ 0 = 0

theorem G12FineGrid.endpoint_mono {ρ : ℝ} (hρ : 1 < ρ) : Monotone (endpoint ρ)

theorem G12FineGrid.mem_cell_iff {ρ : ℝ} (hρ : 1 < ρ) {i n : ℕ} (hn : 1 ≤ n) : n ∈ cell ρ i ↔ ρ ^ i ≤ ↑n ∧ ↑n < ρ ^ (i + 1)

theorem G12FineGrid.unique {ρ : ℝ} (hρ : 1 < ρ) {i j n : ℕ} (hi : n ∈ cell ρ i) (hj : n ∈ cell ρ j) : i = j

theorem G12FineGrid.disjoint {ρ : ℝ} (hρ : 1 < ρ) {i j : ℕ} (hij : i ≠ j) : Disjoint (cell ρ i) (cell ρ j)

theorem G12FineGrid.cover_to_endpoint (ρ : ℝ) (K : ℕ) {n : ℕ} (hn : 1 ≤ n) (hN : n ≤ endpoint ρ K) : ∃ i < K, n ∈ cell ρ i

A finite cover works even when several adjacent endpoints coincide.

noncomputable def G12FineGrid.count (ρ : ℝ) (N : ℕ) : ℕ

A concrete logarithmic number of cells, not an existential truncation.

Equations

• G12FineGrid.count ρ N = ⌈Real.log ↑N / Real.log ρ⌉₊ + 1

theorem G12FineGrid.count_covers {ρ : ℝ} (hρ : 1 < ρ) {N : ℕ} (hN : 1 ≤ N) : N ≤ endpoint ρ (count ρ N)

theorem G12FineGrid.cover {ρ : ℝ} (hρ : 1 < ρ) {N n : ℕ} (hn : 1 ≤ n) (hN : n ≤ N) : ∃! i : ℕ, i < count ρ N ∧ n ∈ cell ρ i

theorem G12FineGrid.endpoint_width {ρ : ℝ} (hρ : 1 < ρ) (i : ℕ) : ↑(endpoint ρ (i + 1)) ≤ ρ * (↑(endpoint ρ i) + 1)

theorem G12FineGrid.clipped_width {ρ : ℝ} (hρ : 1 < ρ) (L H i : ℕ) : min ↑H ↑(endpoint ρ (i + 1)) ≤ ρ * (max ↑L ↑(endpoint ρ i) + 1)

theorem G12FineGrid.clipped_dyadic {ρ : ℝ} (hρ : 1 < ρ) (hu : ρ ≤ 3 / 2) (L H i : ℕ) (hlo : 3 ≤ max L (endpoint ρ i)) : min H (endpoint ρ (i + 1)) ≤ 2 * max L (endpoint ρ i)

theorem G12FineGrid.cover_nonempty {ρ : ℝ} (hρ : 1 < ρ) {N n : ℕ} (hn : 1 ≤ n) (hN : n ≤ N) : ∃! i : ℕ, i < count ρ N ∧ n ∈ cell ρ i ∧ (cell ρ i).Nonempty

Occupancy singles out a unique nonempty cell, not merely a chosen index.

theorem G12FineGrid.clipped_disjoint {ρ : ℝ} (hρ : 1 < ρ) (L H : ℕ) {i j : ℕ} (hij : i ≠ j) : Disjoint (clipped ρ L H i) (clipped ρ L H j)

theorem G12FineGrid.clipped_cover {ρ : ℝ} (hρ : 1 < ρ) {L H n : ℕ} (hn : n ∈ Finset.Ioc L H) : ∃! i : ℕ, i < count ρ H ∧ n ∈ clipped ρ L H i

theorem G12FineGrid.clipped_union {ρ : ℝ} (hρ : 1 < ρ) (L H : ℕ) : (Finset.range (count ρ H)).biUnion (clipped ρ L H) = Finset.Ioc L H

Empty and reversed clipping intervals are included in this exact equality.

theorem G12FineGrid.endpoint_dyadic {ρ : ℝ} (hρ : 1 < ρ) (hu : ρ ≤ 3 / 2) (i : ℕ) (hi : 3 ≤ endpoint ρ i) : endpoint ρ (i + 1) ≤ 2 * endpoint ρ i