Fibers: the trace fiber and the energy fiber

This file implements blueprint nodes C01 and C02 of docs/nikodym_construction_lean_blueprint.md.

• C01: Scaffold.exists_trace_fiber: under Scaffold with K₀ > 0, for every real T ≥ 1 there is an integer s and a Finset A ⊆ boxFinset T on which the trace is constantly s, with (T / (n * K₀)) ^ n / ((2 * n + 1) * T) ≤ #A.
• C02: the energy fiber of the digit space. Everything is parametrised by k = h - 1, the number of digits. Scaffold.radix n q k : Fin k → ℕ is the radix vector (Q₁, …, Q_k) of Q01, and Scaffold.D_radix identifies the mixed-radix weights of D01 with the products Dᵢ of Q01: D (radix n q k) i = Params.D n q (i + 1). The digit space is Scaffold.digitSpace S n q k ρ = ∏ i, boxFinset (ρ * Qᵢ₊₁), the prefix sums are Scaffold.prefixSum n q k w i = ∑_{j ≤ i} Dⱼ wⱼ (= yᵢ(w)), the base point is Scaffold.base n q k w = ∑ j, Dⱼ wⱼ (= b(w)), and the color is Scaffold.color σ n q k w i = trace (yᵢ(w) ^ 2) (an integer). The main results are the prefix bound Scaffold.abs_prefixSum_le, the base bounds Scaffold.abs_base_le, Scaffold.abs_base_le_M, the color bound Scaffold.color_mem_colorBox, the pigeonhole theorem Scaffold.exists_energy_fiber producing a color class B ⊆ digitSpace with #digitSpace / (2 ^ k * ∏ i, D_{i+2} ^ 2) ≤ #B, and injectivity of base on the digit space (Scaffold.base_injOn, Scaffold.card_image_base).

Throughout, n denotes Fintype.card ι in Layer S/D statements; in Layer C, n and q are the integer parameters of Q01 and the number of embeddings is written Fintype.card ι.

theorem Nikodym.Scaffold.floor_trace_mem_Icc {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} (h : Scaffold b σ φ K₀ K₁) {T : ℝ} {x : R} (hx : ∀ (i : ι), |(σ i) x| ≤ T) : ⌊trace σ x⌋ ∈ Finset.Icc (-⌊↑(Fintype.card ι) * T⌋) ⌊↑(Fintype.card ι) * T⌋

Blueprint C01: the trace of an element of the box of radius T lies in Finset.Icc (-⌊n * T⌋) ⌊n * T⌋.

theorem Nikodym.Scaffold.exists_trace_fiber {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} (h : Scaffold b σ φ K₀ K₁) (hK₀ : 0 < K₀) {T : ℝ} (hT : 1 ≤ T) : ∃ (s : ℤ), ∃ A ⊆ h.boxFinset T, (∀ a ∈ A, trace σ a = ↑s) ∧ (T / (↑(Fintype.card ι) * K₀)) ^ Fintype.card ι / ((2 * ↑(Fintype.card ι) + 1) * T) ≤ ↑A.card

Blueprint C01: the trace fiber. Under Scaffold with K₀ > 0, for every real T ≥ 1 there is an integer s and a Finset A ⊆ boxFinset T on which the trace is constantly s, with (T / (n * K₀)) ^ n / ((2 * n + 1) * T) ≤ #A.

Blueprint C02: the radix vector and the bridge between the two Ds

noncomputable def Nikodym.Scaffold.radix (n q k : ℕ) : Fin k → ℕ

Blueprint C02: the radix vector (Q₁, …, Q_k) of Q01, as a function on Fin k (here k = h - 1): radix n q k i = Params.Q n q (i + 1).

Equations

• Nikodym.Scaffold.radix n q k i = Nikodym.Params.Q n q (↑i + 1)

@[simp]

theorem Nikodym.Scaffold.radix_apply {n q k : ℕ} (i : Fin k) : radix n q k i = Params.Q n q (↑i + 1)

Blueprint C02: radix n q k i = Params.Q n q (i + 1).

theorem Nikodym.Scaffold.radix_pos {n q k : ℕ} (hq : 1 ≤ q) (i : Fin k) : 1 ≤ radix n q k i

Blueprint C02: all radices are ≥ 1 when q ≥ 1.

theorem Nikodym.Scaffold.D_radix {n q k : ℕ} (i : Fin k) : D (radix n q k) i = Params.D n q (↑i + 1)

Blueprint C02: the bridge between the mixed-radix weights of D01 and the products of Q01: D (radix n q k) i = Params.D n q (i + 1) (both are ∏_{j=1}^{i} Q_j).

theorem Nikodym.Scaffold.D_radix_mul_radix {n q k : ℕ} (i : Fin k) : D (radix n q k) i * radix n q k i = Params.D n q (↑i + 2)

Blueprint C02: D (radix n q k) j * Q_{j+1} = Params.D n q (j + 2).

Blueprint C02: the digit space, prefix sums, base point and colors

noncomputable def Nikodym.Scaffold.digitSpace {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} (S : Scaffold b σ φ K₀ K₁) (n q k : ℕ) (ρ : ℝ) : Finset (Fin k → R)

Blueprint C02: the digit space W = ∏ i, boxFinset (ρ * Q_{i+1}) as a Finset of digit vectors Fin k → R.

Equations

• S.digitSpace n q k ρ = Fintype.piFinset fun (i : Fin k) => S.boxFinset (ρ * ↑(Nikodym.Scaffold.radix n q k i))

noncomputable def Nikodym.Scaffold.prefixSum {R : Type u_1} [CommRing R] (n q k : ℕ) (w : Fin k → R) (i : Fin k) : R

Blueprint C02: the prefix sum yᵢ(w) = ∑_{j ≤ i} Dⱼ wⱼ.

Equations

• Nikodym.Scaffold.prefixSum n q k w i = ∑ j ≤ i, ↑(Nikodym.Scaffold.D (Nikodym.Scaffold.radix n q k) j) * w j

noncomputable def Nikodym.Scaffold.base {R : Type u_1} [CommRing R] (n q k : ℕ) (w : Fin k → R) : R

Blueprint C02: the base point b(w) = ∑ j, Dⱼ wⱼ.

Equations

• Nikodym.Scaffold.base n q k w = ∑ j : Fin k, ↑(Nikodym.Scaffold.D (Nikodym.Scaffold.radix n q k) j) * w j

noncomputable def Nikodym.Scaffold.color {R : Type u_1} {ι : Type u_2} [CommRing R] [Fintype ι] (σ : ι → R →+* ℝ) (n q k : ℕ) (w : Fin k → R) : Fin k → ℤ

Blueprint C02: the energy color c(w)ᵢ = trace (yᵢ(w) ^ 2), landed in ℤ via the floor (see Scaffold.color_eq: the trace is an integer).

Equations

• Nikodym.Scaffold.color σ n q k w i = ⌊Nikodym.Scaffold.trace σ (Nikodym.Scaffold.prefixSum n q k w i ^ 2)⌋

noncomputable def Nikodym.Scaffold.colorBox (n q k : ℕ) : Finset (Fin k → ℤ)

Blueprint C02: the finite set of admissible colors ∏ i, Icc 0 (D_{i+2} ^ 2).

Equations

• Nikodym.Scaffold.colorBox n q k = Fintype.piFinset fun (i : Fin k) => Finset.Icc 0 (↑(Nikodym.Params.D n q (↑i + 2)) ^ 2)

theorem Nikodym.Scaffold.mem_digitSpace {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} {n q k : ℕ} {ρ : ℝ} (S : Scaffold b σ φ K₀ K₁) {w : Fin k → R} : w ∈ S.digitSpace n q k ρ ↔ ∀ (i : Fin k) (ε : ι), |(σ ε) (w i)| ≤ ρ * ↑(radix n q k i)

Blueprint C02: membership in the digit space.

theorem Nikodym.Scaffold.card_digitSpace {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} {n q k : ℕ} {ρ : ℝ} (S : Scaffold b σ φ K₀ K₁) : (S.digitSpace n q k ρ).card = ∏ i : Fin k, (S.boxFinset (ρ * ↑(radix n q k i))).card

Blueprint C02: |W| = ∏ i, |boxFinset (ρ * Q_{i+1})|.

theorem Nikodym.Scaffold.prefixSum_eq_sum_filter {R : Type u_1} [CommRing R] {n q k : ℕ} (w : Fin k → R) (i : Fin k) : prefixSum n q k w i = ∑ j : Fin k with j ≤ i, ↑(D (radix n q k) j) * w j

Blueprint C02: the prefix sum as a sum over the filter {j | j ≤ i}.

theorem Nikodym.Scaffold.base_eq_prefixSum_last {R : Type u_1} [CommRing R] {n q k : ℕ} (hk : 0 < k) (w : Fin k → R) : base n q k w = prefixSum n q k w ⟨k - 1, ⋯⟩

Blueprint C02: b(w) = y_{k-1}(w) for k ≥ 1.

theorem Nikodym.Scaffold.abs_term_le {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} {n q k : ℕ} {ρ : ℝ} (S : Scaffold b σ φ K₀ K₁) {w : Fin k → R} (hw : w ∈ S.digitSpace n q k ρ) (j : Fin k) (ε : ι) : |(σ ε) (↑(D (radix n q k) j) * w j)| ≤ ρ * ↑(Params.D n q (↑j + 2))

Blueprint C02: the digit term Dⱼ wⱼ of a digit vector satisfies |σ (Dⱼ wⱼ)| ≤ ρ * Dⱼ Q_{j+1} = ρ * Params.D n q (j + 2).

theorem Nikodym.Scaffold.abs_prefixSum_le {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} {n q k : ℕ} {ρ : ℝ} (S : Scaffold b σ φ K₀ K₁) (hq : 1 ≤ q) (hρ : 0 ≤ ρ) {w : Fin k → R} (hw : w ∈ S.digitSpace n q k ρ) (i : Fin k) (ε : ι) : |(σ ε) (prefixSum n q k w i)| ≤ ρ * (↑↑i + 1) * ↑(Params.D n q (↑i + 2))

Blueprint C02 (prefix bound): for w ∈ W, yᵢ(w) ∈ box (ρ (i+1) D_{i+2}).

theorem Nikodym.Scaffold.abs_base_le {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} {n q k : ℕ} {ρ : ℝ} (S : Scaffold b σ φ K₀ K₁) (hq : 1 ≤ q) (hρ : 0 ≤ ρ) {w : Fin k → R} (hw : w ∈ S.digitSpace n q k ρ) (ε : ι) : |(σ ε) (base n q k w)| ≤ ρ * ↑k * ↑(Params.D n q (k + 1))

Blueprint C02 (prefix bound for the base point): for w ∈ W, b(w) ∈ box (ρ k D_{k+1}).

theorem Nikodym.Scaffold.abs_base_le_M {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} {n q k : ℕ} {ρ : ℝ} (S : Scaffold b σ φ K₀ K₁) (hn : 1 ≤ n) (hq : 1 ≤ q) (hρ : 0 ≤ ρ) {w : Fin k → R} (hw : w ∈ S.digitSpace n q k ρ) (ε : ι) : |(σ ε) (base n q k w)| ≤ ρ * ↑k * ↑(Params.M n q)

Blueprint C02: for w ∈ W, b(w) ∈ box (ρ k M) (using D_{k+1} ≤ M from Q01).

theorem Nikodym.Scaffold.abs_base_le_M' {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} {n q k : ℕ} {ρ : ℝ} (S : Scaffold b σ φ K₀ K₁) (hn : 1 ≤ n) (hq : 1 ≤ q) (hρ : 0 ≤ ρ) {w : Fin k → R} (hw : w ∈ S.digitSpace n q k ρ) (ε : ι) : |(σ ε) (base n q k w)| ≤ ρ * (↑k + 1) * ↑(Params.M n q)

Blueprint C02: for w ∈ W, b(w) ∈ box (ρ h M) with h = k + 1.

theorem Nikodym.Scaffold.trace_sq_le {R : Type u_1} {ι : Type u_2} [CommRing R] [Fintype ι] {σ : ι → R →+* ℝ} {x : R} {T : ℝ} (hx : ∀ (i : ι), |(σ i) x| ≤ T) : trace σ (x ^ 2) ≤ ↑(Fintype.card ι) * T ^ 2

Blueprint C02: on the box of radius T, trace (x ^ 2) ≤ n * T ^ 2.

theorem Nikodym.Scaffold.color_eq {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} (n q k : ℕ) (S : Scaffold b σ φ K₀ K₁) (w : Fin k → R) (i : Fin k) : ↑(color σ n q k w i) = trace σ (prefixSum n q k w i ^ 2)

Blueprint C02: the color is the trace of the squared prefix sum (an integer).

theorem Nikodym.Scaffold.trace_prefixSum_eq_of_color_eq {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} (n q k : ℕ) (S : Scaffold b σ φ K₀ K₁) {w w' : Fin k → R} (h : color σ n q k w = color σ n q k w') (i : Fin k) : trace σ (prefixSum n q k w i ^ 2) = trace σ (prefixSum n q k w' i ^ 2)

Blueprint C02: equal colors give equal energies trace (yᵢ(w) ^ 2) = trace (yᵢ(w') ^ 2).

theorem Nikodym.Scaffold.color_mem_Icc {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} {n q k : ℕ} {ρ : ℝ} (S : Scaffold b σ φ K₀ K₁) (hq : 1 ≤ q) (hρ : 0 ≤ ρ) (hρ2 : ↑(Fintype.card ι) * ρ ^ 2 * (↑k + 1) ^ 2 ≤ 1) {w : Fin k → R} (hw : w ∈ S.digitSpace n q k ρ) (i : Fin k) : color σ n q k w i ∈ Finset.Icc 0 (↑(Params.D n q (↑i + 2)) ^ 2)

Blueprint C02 (colors): under n ρ² (k+1)² ≤ 1, for w ∈ W the color satisfies 0 ≤ c(w)ᵢ ≤ D_{i+2} ^ 2.

theorem Nikodym.Scaffold.color_mem_colorBox {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} {n q k : ℕ} {ρ : ℝ} (S : Scaffold b σ φ K₀ K₁) (hq : 1 ≤ q) (hρ : 0 ≤ ρ) (hρ2 : ↑(Fintype.card ι) * ρ ^ 2 * (↑k + 1) ^ 2 ≤ 1) {w : Fin k → R} (hw : w ∈ S.digitSpace n q k ρ) : color σ n q k w ∈ colorBox n q k

Blueprint C02 (colors): the color of a digit vector lies in colorBox.

theorem Nikodym.Scaffold.zero_mem_colorBox {n q k : ℕ} : 0 ∈ colorBox n q k

Blueprint C02: 0 ∈ colorBox.

theorem Nikodym.Scaffold.card_colorBox {n q k : ℕ} : (colorBox n q k).card = ∏ i : Fin k, (Params.D n q (↑i + 2) ^ 2 + 1)

Blueprint C02: |colorBox| = ∏ i, (D_{i+2} ^ 2 + 1).

theorem Nikodym.Scaffold.card_colorBox_le {n q k : ℕ} (hq : 1 ≤ q) : (colorBox n q k).card ≤ 2 ^ k * ∏ i : Fin k, Params.D n q (↑i + 2) ^ 2

Blueprint C02: |colorBox| ≤ 2 ^ k * ∏ i, D_{i+2} ^ 2 (as D ≥ 1).

theorem Nikodym.Scaffold.exists_energy_fiber {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} {n q k : ℕ} {ρ : ℝ} (S : Scaffold b σ φ K₀ K₁) (hq : 1 ≤ q) (hρ : 0 ≤ ρ) (hρ2 : ↑(Fintype.card ι) * ρ ^ 2 * (↑k + 1) ^ 2 ≤ 1) : ∃ B ⊆ S.digitSpace n q k ρ, (∀ w ∈ B, ∀ w' ∈ B, color σ n q k w = color σ n q k w') ∧ ↑(S.digitSpace n q k ρ).card / (2 ^ k * ∏ i : Fin k, ↑(Params.D n q (↑i + 2)) ^ 2) ≤ ↑B.card

Blueprint C02 (main statement): the energy fiber. Under Scaffold, q ≥ 1, ρ ≥ 0 and n ρ² (k+1)² ≤ 1 (with n = Fintype.card ι the number of embeddings and k = h - 1), there is a color class B ⊆ digitSpace on which color is constant, with #digitSpace / (2 ^ k * ∏ i, D_{i+2} ^ 2) ≤ #B.

theorem Nikodym.Scaffold.base_injOn {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} {n q k : ℕ} {ρ : ℝ} (S : Scaffold b σ φ K₀ K₁) (hρ' : 2 * ρ * √↑(Fintype.card ι) < 1) (hq : 1 ≤ q) : Set.InjOn (base n q k) ↑(S.digitSpace n q k ρ)

Blueprint C02: the base map b(w) = ∑ j, Dⱼ wⱼ is injective on the digit space whenever 2 ρ √n < 1 (D01 with θ = 2ρ).

theorem Nikodym.Scaffold.card_image_base_of_subset {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} {n q k : ℕ} {ρ : ℝ} [DecidableEq R] (S : Scaffold b σ φ K₀ K₁) (hρ' : 2 * ρ * √↑(Fintype.card ι) < 1) (hq : 1 ≤ q) {B : Finset (Fin k → R)} (hB : B ⊆ S.digitSpace n q k ρ) : (Finset.image (base n q k) B).card = B.card

Blueprint C02: |b(B)| = |B| for every B ⊆ digitSpace when 2 ρ √n < 1.

theorem Nikodym.Scaffold.card_image_base {R : Type u_1} {ι : Type u_2} {κ : Type u_3} {F : Type u_4} [CommRing R] [Fintype ι] [Fintype κ] [Field F] [Fintype F] {b : Module.Basis κ ℤ R} {σ : ι → R →+* ℝ} {φ : R →+* F} {K₀ K₁ : ℝ} {n q k : ℕ} {ρ : ℝ} [DecidableEq R] (S : Scaffold b σ φ K₀ K₁) (hρ' : 2 * ρ * √↑(Fintype.card ι) < 1) (hq : 1 ≤ q) : (Finset.image (base n q k) (S.digitSpace n q k ρ)).card = (S.digitSpace n q k ρ).card

Blueprint C02: |b(W)| = |W| when 2 ρ √n < 1.