Add new theorems and proofs

MathTest.lean

@@ -1 +1,2 @@
 import MathTest.Basic
+import MathTest.Sequences.exists_sequence_with_affine_hits

MathTest/Sequences/Definitions.lean

@@ -0,0 +1,12 @@
+import Mathlib
+
+noncomputable section
+
+/-- Decode a pair of rationals from its natural number code, defaulting to `(0, 0)` if decoding fails. -/
+def qpair_of_code (n : ℕ) : ℚ × ℚ :=
+  (Encodable.decode (α := ℚ × ℚ) n).getD (0, 0)
+
+/-- The sequence obtained by evaluating the decoded affine function corresponding to the first coordinate of `Nat.unpair t` at `t`. -/
+def s_seq (t : ℕ) : ℚ :=
+  ((Encodable.decode (α := ℚ × ℚ) (Nat.unpair t).1).getD (0, 0)).1
+    + ((Encodable.decode (α := ℚ × ℚ) (Nat.unpair t).1).getD (0, 0)).2 * (t : ℚ)

MathTest/Sequences/exists_sequence_with_affine_hits.lean

@@ -0,0 +1,14 @@
+import Mathlib
+import MathTest.Sequences.Definitions
+import MathTest.Sequences.infinite_hits_for_code
+
+noncomputable section
+
+theorem exists_sequence_with_affine_hits :
+    ∃ s : ℕ → ℚ, ∀ a d : ℚ, Set.Infinite { t : ℕ | s t = a + d * (t : ℚ) } := by
+  classical
+  refine ⟨s_seq, ?_⟩
+  intro a d
+  have h := infinite_hits_for_code (Encodable.encode (a, d))
+  -- simplify the decoded pair to (a, d)
+  simpa [Encodable.encodek] using h

MathTest/Sequences/infinite_fst_unpair_preimage.lean

@@ -0,0 +1,23 @@
+import Mathlib
+
+open Set
+
+theorem infinite_fst_unpair_preimage (m : ℕ) :
+    Set.Infinite {t : ℕ | (Nat.unpair t).1 = m} := by
+  classical
+  -- Consider the map g k := Nat.pair m k
+  let g : ℕ → ℕ := fun k => Nat.pair m k
+  have hginj : Function.Injective g := by
+    intro k₁ k₂ h
+    have h' : Nat.unpair (g k₁) = Nat.unpair (g k₂) := congrArg Nat.unpair h
+    -- Compare second coordinates
+    have : Prod.snd (Nat.unpair (g k₁)) = Prod.snd (Nat.unpair (g k₂)) := congrArg Prod.snd h'
+    simpa [g, Nat.unpair_pair] using this
+  -- The image of g lies in the target set
+  have himage : ∀ k, g k ∈ {t : ℕ | (Nat.unpair t).1 = m} := by
+    intro k
+    -- By unpair_pair, the first coordinate of unpair (pair m k) is m
+    simpa [g, Set.mem_setOf_eq, Nat.unpair_pair] using
+      congrArg Prod.fst (Nat.unpair_pair m k)
+  -- An injective map from an infinite type into a set yields an infinite set
+  exact Set.infinite_of_injective_forall_mem hginj himage

MathTest/Sequences/infinite_hits_for_code.lean

@@ -0,0 +1,23 @@
+import Mathlib
+import MathTest.Sequences.Definitions
+import MathTest.Sequences.infinite_fst_unpair_preimage
+import MathTest.Sequences.s_seq_eq_on_fiber
+
+noncomputable section
+
+theorem infinite_hits_for_code (n : ℕ) : Set.Infinite { t : ℕ |
+  s_seq t = ((Encodable.decode (α := ℚ × ℚ) n).getD (0, 0)).1
+           + ((Encodable.decode (α := ℚ × ℚ) n).getD (0, 0)).2 * (t : ℚ) } := by
+  classical
+  -- Let T := {t | (Nat.unpair t).1 = n}. T is infinite
+  have hTinf : Set.Infinite {t : ℕ | (Nat.unpair t).1 = n} :=
+    infinite_fst_unpair_preimage n
+  -- Show T ⊆ target set using s_seq_eq_on_fiber
+  have hsubset : {t : ℕ | (Nat.unpair t).1 = n} ⊆
+      {t : ℕ |
+        s_seq t = ((Encodable.decode (α := ℚ × ℚ) n).getD (0, 0)).1
+          + ((Encodable.decode (α := ℚ × ℚ) n).getD (0, 0)).2 * (t : ℚ)} := by
+    intro t ht
+    exact s_seq_eq_on_fiber n t ht
+  -- Conclude by monotonicity of infinitude under supersets
+  exact hTinf.mono hsubset

MathTest/Sequences/qpair_of_code_encode.lean

@@ -0,0 +1,8 @@
+import Mathlib
+import MathTest.Sequences.Definitions
+
+noncomputable section
+
+theorem qpair_of_code_encode (p : ℚ × ℚ) : qpair_of_code (Encodable.encode p) = p := by
+  classical
+  simpa [qpair_of_code, Encodable.encodek]

MathTest/Sequences/s_seq_eq_on_fiber.lean

@@ -0,0 +1,9 @@
+import Mathlib
+import MathTest.Sequences.Definitions
+
+noncomputable section
+
+theorem s_seq_eq_on_fiber (n t : ℕ) (h : (Nat.unpair t).1 = n) :
+    s_seq t = ((Encodable.decode (α := ℚ × ℚ) n).getD (0, 0)).1
+              + ((Encodable.decode (α := ℚ × ℚ) n).getD (0, 0)).2 * (t : ℚ) := by
+  simp [s_seq, h]