DyadicFourIsometry.lean

1 module
2 public import DensePadicIsometry
3 public import RationalPadicEmbedding
4 public import DyadicPacketRational
5 
6 /-!
7 # Isometric bijections from the four actual dyadic Euler packets
8 
9 Author: Komorebi P.
10 The normalized maps are isometries of the dyadic integers. The original
11 coefficients instead fill their exact factorial-centered affine images.
12 -/
13 
14 @[expose] public section
15 noncomputable section
16 set_option autoImplicit false
17 
18 namespace KomorebiPaperIX.DyadicFourIsometry
19 
20 open Congruential DyadicFourLeastPeriods
21 
22 def samples (j : ℕ) (hj : j < 4) : ℕ → ℤ_[2] :=
23   RationalPadicEmbedding.samples 2 (DyadicPacketRational.packet j)
24     (DyadicPacketRational.packet_zero j) (fun m n => DyadicPacketRational.norm_sub j m n hj)
25 
26 @[simp]
27 theorem samples_coe (j : ℕ) (hj : j < 4) (n : ℕ) :
28     (samples j hj n : ℚ_[2]) = (DyadicPacketRational.packet j n : ℚ_[2]) := rfl
29 
30 theorem samples_dist (j : ℕ) (hj : j < 4) (m n : ℕ) :
31     dist (samples j hj m) (samples j hj n) = dist (m : ℤ_[2]) (n : ℤ_[2]) :=
32   RationalPadicEmbedding.samples_dist 2 (DyadicPacketRational.packet j)
33     (DyadicPacketRational.packet_zero j) (fun a b => DyadicPacketRational.norm_sub j a b hj) m n
34 
35 /-- The uniquely determined isometric bijection arising from the actual packet. -/
36 def isometry (j : ℕ) (hj : j < 4) : ℤ_[2] ≃ᵢ ℤ_[2] :=
37   DensePadicIsometry.extensionEquiv 2 (samples j hj) (samples_dist j hj)
38 
39 @[simp]
40 theorem isometry_nat (j : ℕ) (hj : j < 4) (n : ℕ) :
41     (isometry j hj (n : ℤ_[2]) : ℚ_[2]) = (DyadicPacketRational.packet j n : ℚ_[2]) := by
42   change (DensePadicIsometry.extensionEquiv 2 (samples j hj) (samples_dist j hj) n : ℚ_[2]) = _
43   rw [DensePadicIsometry.extensionEquiv_nat, samples_coe]
44 
45 @[simp]
46 theorem isometry_zero (j : ℕ) (hj : j < 4) : isometry j hj 0 = 0 := by
47   apply PadicInt.ext
48   simpa using isometry_nat j hj 0
49 
50 theorem isometry_dist (j : ℕ) (hj : j < 4) (x y : ℤ_[2]) :
51     dist (isometry j hj x) (isometry j hj y) = dist x y :=
52   (isometry j hj).dist_eq x y
53 
54 theorem isometry_surjective (j : ℕ) (hj : j < 4) :
55     Function.Surjective (isometry j hj) := (isometry j hj).surjective
56 
57 theorem isometry_continuous (j : ℕ) (hj : j < 4) :
58     Continuous (isometry j hj) := (isometry j hj).continuous
59 
60 /-- Uniqueness is among all continuous maps with the prescribed rational values. -/
61 theorem unique_continuous (j : ℕ) (hj : j < 4) (g : ℤ_[2] → ℤ_[2])
62     (hg : Continuous g)
63     (hgnat : ∀ n : ℕ, (g (n : ℤ_[2]) : ℚ_[2]) = (DyadicPacketRational.packet j n : ℚ_[2])) :
64     g = isometry j hj := by
65   apply DensePadicIsometry.extensionEquiv_unique_continuous 2 (samples j hj) (samples_dist j hj) g hg
66   intro n
67   exact PadicInt.ext (hgnat n)
68 
69 /-- Every dyadic target has exactly one input under the normalized map. -/
70 theorem unique_preimage (j : ℕ) (hj : j < 4) (z : ℤ_[2]) :
71     ∃! x : ℤ_[2], isometry j hj x = z := by
72   refine ⟨(isometry j hj).symm z, (isometry j hj).apply_symm_apply z, ?_⟩
73   intro x hx
74   exact (isometry j hj).injective (hx.trans ((isometry j hj).apply_symm_apply z).symm)
75 
76 /-- A literal existence-and-uniqueness theorem for an isometric bijection
77 interpolating the normalized actual rational coefficients. -/
78 theorem existsUnique_isometry (j : ℕ) (hj : j < 4) :
79     ∃! e : ℤ_[2] ≃ᵢ ℤ_[2], ∀ n : ℕ,
80       (e (n : ℤ_[2]) : ℚ_[2]) = (DyadicPacketRational.packet j n : ℚ_[2]) := by
81   refine ⟨isometry j hj, isometry_nat j hj, ?_⟩
82   intro e he
83   apply IsometryEquiv.ext
84   exact congrFun (unique_continuous j hj e e.continuous he)
85 
86 /-- Undo the normalization to extend the original coefficients themselves. -/
87 def originalExtension (j : ℕ) (hj : j < 4) (x : ℤ_[2]) : ℤ_[2] :=
88   (j.factorial : ℤ_[2]) + (2 : ℤ_[2]) ^ originalBonus j * isometry j hj x
89 
90 theorem originalExtension_nat (j : ℕ) (hj : j < 4) (n : ℕ) :
91     (originalExtension j hj (n : ℤ_[2]) : ℚ_[2]) = (unnormalized 4 j n : ℚ_[2]) := by
92   simp only [originalExtension, PadicInt.coe_add, PadicInt.coe_mul, PadicInt.coe_pow,
93     PadicInt.coe_natCast, isometry_nat]
94   have htwo : ((2 : ℤ_[2]) : ℚ_[2]) = (2 : ℚ_[2]) := rfl
95   rw [htwo]
96   have he : (j.factorial : ℚ) + (2 : ℚ) ^ originalBonus j * DyadicPacketRational.packet j n =
97       unnormalized 4 j n := by
98     rw [DyadicPacketRational.packet]
99     have hd : (2 : ℚ) ^ originalBonus j ≠ 0 := pow_ne_zero _ (by norm_num)
100     field_simp
101     ring
102   simpa using congrArg (fun q : ℚ => (q : ℚ_[2])) he
103 
104 theorem originalExtension_continuous (j : ℕ) (hj : j < 4) :
105     Continuous (originalExtension j hj) :=
106   continuous_const.add (continuous_const.mul (isometry_continuous j hj))
107 
108 /-- The original continuous coefficients retain their exact displacement scale. -/
109 theorem originalExtension_dist (j : ℕ) (hj : j < 4) (x y : ℤ_[2]) :
110     dist (originalExtension j hj x) (originalExtension j hj y) =
111       (2 : ℝ) ^ (-(originalBonus j : ℤ)) * dist x y := by
112   have hsub : originalExtension j hj x - originalExtension j hj y =
113       (2 : ℤ_[2]) ^ originalBonus j * (isometry j hj x - isometry j hj y) := by
114     unfold originalExtension
115     ring
116   have hn : ‖(2 : ℤ_[2]) ^ originalBonus j‖ = (2 : ℝ) ^ (-(originalBonus j : ℤ)) := by
117     simpa using PadicInt.norm_p_pow (p := 2) (originalBonus j)
118   rw [dist_eq_norm, hsub, norm_mul, hn, ← dist_eq_norm, isometry_dist]
119 
120 theorem originalExtension_injective (j : ℕ) (hj : j < 4) :
121     Function.Injective (originalExtension j hj) := by
122   intro x y h
123   have hd : (2 : ℤ_[2]) ^ originalBonus j ≠ 0 := pow_ne_zero _ (by norm_num)
124   apply (isometry j hj).injective
125   exact (mul_left_cancel₀ hd) (add_left_cancel h)
126 
127 /-- Every point of the exact affine image has one original-packet preimage. -/
128 theorem unique_original_preimage (j : ℕ) (hj : j < 4) (z : ℤ_[2]) :
129     ∃! x : ℤ_[2], originalExtension j hj x =
130       (j.factorial : ℤ_[2]) + (2 : ℤ_[2]) ^ originalBonus j * z := by
131   refine ⟨(isometry j hj).symm z, ?_, ?_⟩
132   · simp only [originalExtension, (isometry j hj).apply_symm_apply]
133   · intro x hx
134     apply originalExtension_injective j hj
135     simpa only [originalExtension, (isometry j hj).apply_symm_apply] using hx
136 
137 theorem originalExtension_range (j : ℕ) (hj : j < 4) :
138     Set.range (originalExtension j hj) =
139       Set.range (fun z : ℤ_[2] => (j.factorial : ℤ_[2]) + (2 : ℤ_[2]) ^ originalBonus j * z) := by
140   ext y
141   constructor
142   · rintro ⟨x, rfl⟩
143     exact ⟨isometry j hj x, rfl⟩
144   · rintro ⟨z, rfl⟩
145     obtain ⟨x, hx, _⟩ := unique_original_preimage j hj z
146     exact ⟨x, hx⟩
147 
148 end KomorebiPaperIX.DyadicFourIsometry

Back to source controls