DyadicIsometryContract.lean

1 module
2 public import DyadicFourIsometry
3 
4 @[expose] public section
5 set_option autoImplicit false
6 
7 open KomorebiPaperIX
8 
9 /-- Actual coefficient normalization is written out rather than supplied as
10 an assumed isometry hypothesis. The result is a bijective isometry. -/
11 example (j : ℕ) (hj : j < 4) :
12     ∃! e : ℤ_[2] ≃ᵢ ℤ_[2], ∀ n : ℕ,
13       (e (n : ℤ_[2]) : ℚ_[2]) =
14         (((Congruential.unnormalized 4 j n - (j.factorial : ℚ)) /
15           (2 : ℚ) ^ DyadicFourLeastPeriods.originalBonus j : ℚ) : ℚ_[2]) :=
16   DyadicFourIsometry.existsUnique_isometry j hj
17 
18 /-- Uniqueness includes continuous functions that are not assumed isometries. -/
19 example (j : ℕ) (hj : j < 4) (g : ℤ_[2] → ℤ_[2]) (hg : Continuous g)
20     (hn : ∀ n : ℕ, (g (n : ℤ_[2]) : ℚ_[2]) =
21       (((Congruential.unnormalized 4 j n - (j.factorial : ℚ)) /
22         (2 : ℚ) ^ DyadicFourLeastPeriods.originalBonus j : ℚ) : ℚ_[2])) :
23     g = DyadicFourIsometry.isometry j hj :=
24   DyadicFourIsometry.unique_continuous j hj g hg hn
25 
26 /-- Original coefficients interpolate on the packet index, not the degree index. -/
27 example (j : ℕ) (hj : j < 4) (n : ℕ) :
28     (DyadicFourIsometry.originalExtension j hj (n : ℤ_[2]) : ℚ_[2]) =
29       (NishibuchiCompletion.generalizedEuler 4 (by decide) j (4 * n) : ℚ_[2]) := by
30   rw [NishibuchiCompletion.generalizedEuler_at_packet]
31   exact DyadicFourIsometry.originalExtension_nat j hj n
32 
33 example (j : ℕ) (hj : j < 4) (z : ℤ_[2]) :
34     ∃! x : ℤ_[2], DyadicFourIsometry.originalExtension j hj x =
35       (j.factorial : ℤ_[2]) + (2 : ℤ_[2]) ^ DyadicFourLeastPeriods.originalBonus j * z :=
36   DyadicFourIsometry.unique_original_preimage j hj z
37 
38 /-- The generic extension theorem uses the p-adic distance on embedded naturals. -/
39 example (p : ℕ) [Fact p.Prime] (f : ℕ → ℤ_[p])
40     (h : ∀ m n : ℕ, dist (f m) (f n) = dist (m : ℤ_[p]) (n : ℤ_[p])) :
41     ∃! e : ℤ_[p] ≃ᵢ ℤ_[p], ∀ n : ℕ, e (n : ℤ_[p]) = f n :=
42   DensePadicIsometry.existsUnique_extensionEquiv p f h

Back to source controls