Tangent lines on the product set #
This file implements blueprint node T01 of docs/nikodym_construction_lean_blueprint.md.
Everything is parametrised by k = h - 1 (the number of digits), as in Fibers.lean: digit
vectors are Fin k → R, points of F ^ h are Fin (k + 1) → F built with Fin.snoc.
- Definitions: the point
Scaffold.pt φ n q k a w = (φ (a i))_i ++ φ (base w), the directionScaffold.dir φ w = (φ (w i))_i ++ 1, the product familyScaffold.ptFamily φ n q k A B = (A.image φ, …, A.image φ, B.image (φ ∘ base))and the product setScaffold.ptSet φ n q k A B = Fintype.piFinset (ptFamily …), so thatptSet = φ(A)^k × φ(b(B)). - T01a:
Scaffold.eq_zero_of_map_eq_zero_of_lt_M(small kernel on boxes of radius< M),Scaffold.eq_of_map_eq_of_box,Scaffold.injOn_of_box,Scaffold.injOn_A,Scaffold.eq_of_map_base_eq,Scaffold.injOn_base_B,Scaffold.pt_injOn. - T01b:
Scaffold.eq_zero_of_map_eq_zero_of_small. - T01c:
Scaffold.prefixSumBelow(y_{i-1}),Scaffold.abs_prefixSumBelow_le,Scaffold.base_sub_base_eq,Scaffold.abs_mul_sub_prefixSum_le,Scaffold.digit_eq_of_trace_eq_zero(the D02 step) andScaffold.no_collision. - Main statements:
Scaffold.tangent_hypothesis(the hypothesis of P01 forptSet),Scaffold.card_ptSet(#ptSet = #A ^ k * #B) andScaffold.isNikodym_univ_sdiff_ptSet(univ \ ptSetis a Nikodym set).
Throughout, n and q are the integer parameters of Q01, related to the types by
Fintype.card ι = n and Fintype.card F = q; the constants are given as hypotheses
ρ = 1 / (100 (k + 1) √n) and γ = 1 / 10. Only 1 ≤ n and 1 ≤ q are needed here (the
Q02 threshold 2 ^ (n 2 ^ k) ≤ q implies 1 ≤ q). Declarations involving Finset.image
carry a [DecidableEq F] assumption (consumers may use classical).
Blueprint T01: points, directions and the product set #
noncomputable def
Nikodym.Scaffold.pt
{R : Type u_1}
{F : Type u_2}
[CommRing R]
[Field F]
(φ : R →+* F)
(n q k : ℕ)
(a w : Fin k → R)
:
Blueprint T01: the point p(a, w) = (φ (a 0), …, φ (a (k-1)), φ (b(w))) ∈ F ^ (k + 1).
Equations
- Nikodym.Scaffold.pt φ n q k a w = Fin.snoc (fun (i : Fin k) => φ (a i)) (φ (Nikodym.Scaffold.base n q k w))
Instances For
noncomputable def
Nikodym.Scaffold.ptFamily
{R : Type u_1}
{F : Type u_2}
[CommRing R]
[Field F]
(φ : R →+* F)
[DecidableEq F]
(n q k : ℕ)
(A : Finset R)
(B : Finset (Fin k → R))
:
Blueprint T01: the family of factors (φ(A), …, φ(A), φ(b(B))) of the product set.
Equations
- Nikodym.Scaffold.ptFamily φ n q k A B = Fin.snoc (fun (x : Fin k) => Finset.image (⇑φ) A) (Finset.image (⇑φ ∘ Nikodym.Scaffold.base n q k) B)
Instances For
noncomputable def
Nikodym.Scaffold.ptSet
{R : Type u_1}
{F : Type u_2}
[CommRing R]
[Field F]
(φ : R →+* F)
[DecidableEq F]
(n q k : ℕ)
(A : Finset R)
(B : Finset (Fin k → R))
:
Blueprint T01: the product set P = φ(A) ^ k × φ(b(B)) ⊆ F ^ (k + 1).
Equations
- Nikodym.Scaffold.ptSet φ n q k A B = Fintype.piFinset (Nikodym.Scaffold.ptFamily φ n q k A B)
Instances For
theorem
Nikodym.Scaffold.pt_mem_ptSet
{R : Type u_1}
{F : Type u_2}
[CommRing R]
[Field F]
(φ : R →+* F)
{n q k : ℕ}
[DecidableEq F]
{A : Finset R}
{B : Finset (Fin k → R)}
{a w : Fin k → R}
(ha : a ∈ Fintype.piFinset fun (x : Fin k) => A)
(hw : w ∈ B)
:
Blueprint T01: p(a, w) ∈ P for a ∈ A ^ k and w ∈ B.
theorem
Nikodym.Scaffold.exists_pt_eq
{R : Type u_1}
{F : Type u_2}
[CommRing R]
[Field F]
(φ : R →+* F)
{n q k : ℕ}
[DecidableEq F]
{A : Finset R}
{B : Finset (Fin k → R)}
{u : Fin (k + 1) → F}
(hu : u ∈ ptSet φ n q k A B)
:
Blueprint T01: every point of P is of the form p(a, w) with a ∈ A ^ k and w ∈ B.
Blueprint T01a: the small-kernel property on boxes of radius < M #
theorem
Nikodym.Scaffold.eq_zero_of_map_eq_zero_of_lt_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 : ℕ}
(S : Scaffold b σ φ K₀ K₁)
(hn : Fintype.card ι = n)
(hn1 : 1 ≤ n)
(hqF : Fintype.card F = q)
{T : ℝ}
(hT : T < ↑(Params.M n q))
{x : R}
(hx : ∀ (i : ι), |(σ i) x| ≤ T)
(h0 : φ x = 0)
:
Blueprint T01a: if x ∈ box T with T < M and φ x = 0 then x = 0, since
∏ i, |σ i x| ≤ T ^ n < M ^ n ≤ q.
theorem
Nikodym.Scaffold.eq_of_map_eq_of_box
{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 : ℕ}
(S : Scaffold b σ φ K₀ K₁)
(hn : Fintype.card ι = n)
(hn1 : 1 ≤ n)
(hqF : Fintype.card F = q)
{T : ℝ}
(hT : 2 * T < ↑(Params.M n q))
{x y : R}
(hx : ∀ (i : ι), |(σ i) x| ≤ T)
(hy : ∀ (i : ι), |(σ i) y| ≤ T)
(hxy : φ x = φ y)
:
Blueprint T01a: φ is injective on any box of radius T with 2 T < M.
theorem
Nikodym.Scaffold.injOn_of_box
{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 : ℕ}
(S : Scaffold b σ φ K₀ K₁)
(hn : Fintype.card ι = n)
(hn1 : 1 ≤ n)
(hqF : Fintype.card F = q)
{T : ℝ}
(hT : 2 * T < ↑(Params.M n q))
{A : Finset R}
(hA : A ⊆ S.boxFinset T)
:
Set.InjOn ⇑φ ↑A
Blueprint T01a: φ is injective on any Finset contained in a box of radius T with
2 T < M.
Blueprint T01: the constants ρ = 1 / (100 (k + 1) √n) and γ = 1 / 10 #
theorem
Nikodym.Scaffold.injOn_A
{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 : ℕ}
{γ : ℝ}
(S : Scaffold b σ φ K₀ K₁)
(hn : Fintype.card ι = n)
(hn1 : 1 ≤ n)
(hqF : Fintype.card F = q)
(hq1 : 1 ≤ q)
(hγ : γ = 1 / 10)
{A : Finset R}
(hA : A ⊆ S.boxFinset (γ * ↑(Params.M n q)))
:
Set.InjOn ⇑φ ↑A
Blueprint T01a: φ is injective on the trace fiber A ⊆ box (γ M) (γ = 1/10).
theorem
Nikodym.Scaffold.eq_of_map_base_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₁)
(hn : Fintype.card ι = n)
(hn1 : 1 ≤ n)
(hqF : Fintype.card F = q)
(hq1 : 1 ≤ q)
(hρ : ρ = 1 / (100 * (↑k + 1) * √↑n))
{w w' : Fin k → R}
(hw : w ∈ S.digitSpace n q k ρ)
(hw' : w' ∈ S.digitSpace n q k ρ)
(h : φ (base n q k w) = φ (base n q k w'))
:
Blueprint T01a: φ is injective on the base points b(w), w ∈ B ⊆ digitSpace.
theorem
Nikodym.Scaffold.injOn_base_B
{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 : Fintype.card ι = n)
(hn1 : 1 ≤ n)
(hqF : Fintype.card F = q)
(hq1 : 1 ≤ q)
(hρ : ρ = 1 / (100 * (↑k + 1) * √↑n))
{B : Finset (Fin k → R)}
(hB : B ⊆ S.digitSpace n q k ρ)
:
theorem
Nikodym.Scaffold.pt_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₁)
(hn : Fintype.card ι = n)
(hn1 : 1 ≤ n)
(hqF : Fintype.card F = q)
(hq1 : 1 ≤ q)
(hρ : ρ = 1 / (100 * (↑k + 1) * √↑n))
(hγ : γ = 1 / 10)
{A : Finset R}
(hA : A ⊆ S.boxFinset (γ * ↑(Params.M n q)))
{B : Finset (Fin k → R)}
(hB : B ⊆ S.digitSpace n q k ρ)
:
Blueprint T01a: the point map (a, w) ↦ p(a, w) is injective on A ^ k × B.
Blueprint T01b: lifting #
theorem
Nikodym.Scaffold.eq_zero_of_map_eq_zero_of_small
{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 : Fintype.card ι = n)
(hn1 : 1 ≤ n)
(hqF : Fintype.card F = q)
(hq1 : 1 ≤ q)
(hρ : ρ = 1 / (100 * (↑k + 1) * √↑n))
(hγ : γ = 1 / 10)
{δ : R}
(hδ : ∀ (i : ι), |(σ i) δ| ≤ 2 * γ * ↑(Params.M n q) + 2 * ρ ^ 2 * (↑k + 1) * ↑(Params.M n q))
(h0 : φ δ = 0)
:
Blueprint T01b: if φ δ = 0 and δ ∈ box (2 γ M + 2 ρ² (k + 1) M) then δ = 0, because
2 γ + 2 ρ² (k + 1) < 1.
Blueprint T01c: prefix sums below an index #
noncomputable def
Nikodym.Scaffold.prefixSumBelow
{R : Type u_1}
[CommRing R]
(n q k : ℕ)
(w : Fin k → R)
(i : Fin k)
:
R
Blueprint T01c: the prefix sum strictly below i, y_{i-1}(w) = ∑_{j < i} Dⱼ wⱼ
(0 for i = 0).
Equations
- Nikodym.Scaffold.prefixSumBelow n q k w i = ∑ j < i, ↑(Nikodym.Scaffold.D (Nikodym.Scaffold.radix n q k) j) * w j
Instances For
theorem
Nikodym.Scaffold.abs_prefixSumBelow_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)
(ε : ι)
:
Blueprint T01c: the prefix sum below i is bounded by ρ i D_{i+1} on the digit space.
Blueprint T01c: the collision argument #
theorem
Nikodym.Scaffold.abs_sub_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 w' : Fin k → R}
(hw : w ∈ S.digitSpace n q k ρ)
(hw' : w' ∈ S.digitSpace n q k ρ)
(i : Fin k)
(ε : ι)
:
Blueprint T01c: t = yᵢ(w') - yᵢ(w) lies in box (2 ρ (i + 1) D_{i+2}).
theorem
Nikodym.Scaffold.abs_mul_sub_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₁)
(hn1 : 1 ≤ n)
(hq1 : 1 ≤ q)
(hρ : ρ = 1 / (100 * (↑k + 1) * √↑n))
{w w' : Fin k → R}
(hw : w ∈ S.digitSpace n q k ρ)
(hw' : w' ∈ S.digitSpace n q k ρ)
(i : Fin k)
(ε : ι)
:
Blueprint T01c: wᵢ t lies in box (2 ρ² (k + 1) M), using D_{i+1} Q_{i+1} ^ 2 ≤ M.
theorem
Nikodym.Scaffold.digit_eq_of_trace_eq_zero
{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 : Fintype.card ι = n)
(hn1 : 1 ≤ n)
(hq1 : 1 ≤ q)
(hρ : ρ = 1 / (100 * (↑k + 1) * √↑n))
{w w' : Fin k → R}
(hw : w ∈ S.digitSpace n q k ρ)
(hw' : w' ∈ S.digitSpace n q k ρ)
(hc : color σ n q k w = color σ n q k w')
(i : Fin k)
(ht : trace σ (w i * (prefixSum n q k w' i - prefixSum n q k w i)) = 0)
:
Blueprint T01c (decoding step): if w, w' ∈ digitSpace have the same color and
trace (wᵢ (yᵢ(w') - yᵢ(w))) = 0, then wᵢ = w'ᵢ. This is D02 with Q = Dᵢ, u = y_{i-1}(w),
u' = y_{i-1}(w').
theorem
Nikodym.Scaffold.no_collision
{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 : Fintype.card ι = n)
(hn1 : 1 ≤ n)
(hqF : Fintype.card F = q)
(hq1 : 1 ≤ q)
(hρ : ρ = 1 / (100 * (↑k + 1) * √↑n))
(hγ : γ = 1 / 10)
{s : ℤ}
{A : Finset R}
(hA : A ⊆ S.boxFinset (γ * ↑(Params.M n q)))
(hAs : ∀ a ∈ A, trace σ a = ↑s)
{B : Finset (Fin k → R)}
(hB : B ⊆ S.digitSpace n q k ρ)
(hBc : ∀ w ∈ B, ∀ w' ∈ B, color σ n q k w = color σ n q k w')
{a a' w w' : Fin k → R}
(ha : a ∈ Fintype.piFinset fun (x : Fin k) => A)
(hw : w ∈ B)
(ha' : a' ∈ Fintype.piFinset fun (x : Fin k) => A)
(hw' : w' ∈ B)
(μ : F)
(hcol : pt φ n q k a' w' = pt φ n q k a w + μ • dir φ w)
:
Blueprint T01c (collision): if p(a', w') = p(a, w) + μ v(w) with a, a' ∈ A ^ k and
w, w' ∈ B, then (a', w') = (a, w).
Blueprint T01: main statements #
theorem
Nikodym.Scaffold.tangent_hypothesis
{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 F]
(S : Scaffold b σ φ K₀ K₁)
(hn : Fintype.card ι = n)
(hn1 : 1 ≤ n)
(hqF : Fintype.card F = q)
(hq1 : 1 ≤ q)
(hρ : ρ = 1 / (100 * (↑k + 1) * √↑n))
(hγ : γ = 1 / 10)
{s : ℤ}
{A : Finset R}
(hA : A ⊆ S.boxFinset (γ * ↑(Params.M n q)))
(hAs : ∀ a ∈ A, trace σ a = ↑s)
{B : Finset (Fin k → R)}
(hB : B ⊆ S.digitSpace n q k ρ)
(hBc : ∀ w ∈ B, ∀ w' ∈ B, color σ n q k w = color σ n q k w')
(u : Fin (k + 1) → F)
:
Blueprint T01 (main statement): the product set P = ptSet φ n q k A B satisfies the
hypothesis of P01: through every u ∈ P there is a direction v ≠ 0 whose punctured line
u + t v (t ≠ 0) misses P. Here A ⊆ box (γ M) is a trace fiber and B ⊆ digitSpace is a
color class, with ρ = 1 / (100 (k + 1) √n) and γ = 1 / 10.
theorem
Nikodym.Scaffold.card_ptSet
{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 F]
(S : Scaffold b σ φ K₀ K₁)
(hn : Fintype.card ι = n)
(hn1 : 1 ≤ n)
(hqF : Fintype.card F = q)
(hq1 : 1 ≤ q)
(hρ : ρ = 1 / (100 * (↑k + 1) * √↑n))
(hγ : γ = 1 / 10)
{A : Finset R}
(hA : A ⊆ S.boxFinset (γ * ↑(Params.M n q)))
{B : Finset (Fin k → R)}
(hB : B ⊆ S.digitSpace n q k ρ)
:
Blueprint T01: #P = #A ^ k * #B.
theorem
Nikodym.Scaffold.isNikodym_univ_sdiff_ptSet
{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 F]
(S : Scaffold b σ φ K₀ K₁)
(hk : 1 ≤ k)
(hn : Fintype.card ι = n)
(hn1 : 1 ≤ n)
(hqF : Fintype.card F = q)
(hq1 : 1 ≤ q)
(hρ : ρ = 1 / (100 * (↑k + 1) * √↑n))
(hγ : γ = 1 / 10)
{s : ℤ}
{A : Finset R}
(hA : A ⊆ S.boxFinset (γ * ↑(Params.M n q)))
(hAs : ∀ a ∈ A, trace σ a = ↑s)
{B : Finset (Fin k → R)}
(hB : B ⊆ S.digitSpace n q k ρ)
(hBc : ∀ w ∈ B, ∀ w' ∈ B, color σ n q k w = color σ n q k w')
:
IsNikodym (Finset.univ \ ptSet φ n q k A B)
Blueprint T01 + P01: the complement univ \ P of the product set is a Nikodym set in
F ^ (k + 1) (for k ≥ 1, i.e. h = k + 1 ≥ 2).