ReleaseCoordinatesConsumers.lean

1 import KomorebiVerification.PaperII.ReleaseCoordinatesAlgebra
2 import KomorebiVerification.PaperII.ReleaseCoordinatesHilbert
3 import KomorebiVerification.PaperII.ReleaseCoordinatesFourier
4 
5 /-! Exact formal-series endpoints used by the chapter's selector and CRT statements. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace Komorebi.Residue
9 universe u
10 variable {R : Type u}
11 
12 /-- The printed residue family satisfies the manuscript's nonzero packet convention. -/
13 theorem manuscript_series_residue_packet [CommRing R] [Nontrivial R]
14     (N : Nat) (hN : 0 < N) :
15     Komorebi.PaperII.CommonRefinement.Nonzero (seriesResidueFamily (R := R) N hN) :=
16   seriesResidueProj_nonzero N hN
17 
18 /-- Coefficient selectors commute even without coprimality of their moduli. -/
19 theorem seriesResidueProj_commute [Semiring R]
20     (m n : Nat) (hm : 0 < m) (hn : 0 < n) (j : Fin m) (k : Fin n) :
21     (seriesResidueProj (R := R) m hm j).comp (seriesResidueProj n hn k) =
22       (seriesResidueProj n hn k).comp (seriesResidueProj m hm j) := by
23   ext f a
24   simp only [LinearMap.comp_apply, seriesResidueProj_coeff]
25   by_cases hj : residueAddress m hm a = j <;>
26     by_cases hk : residueAddress n hn a = k <;> simp [hj, hk]
27 
28 /-- Dyadic-odd factorization on actual formal series, including dyadic exponent zero. -/
29 theorem manuscript_series_dyadic_odd [CommRing R]
30     (a M : Nat) (hM : 0 < M) (hodd : Odd M) (s : Fin (2 ^ a * M)) :
31     let h2 : 0 < 2 ^ a := pow_pos (by decide) a
32     let c := crtComponents (2 ^ a) M h2 hM s
33     seriesResidueProj (R := R) (2 ^ a * M) (Nat.mul_pos h2 hM) s =
34         (seriesResidueProj (2 ^ a) h2 c.1).comp (seriesResidueProj M hM c.2) ∧
35       seriesResidueProj (R := R) (2 ^ a * M) (Nat.mul_pos h2 hM) s =
36         (seriesResidueProj M hM c.2).comp (seriesResidueProj (2 ^ a) h2 c.1) := by
37   dsimp only
38   have h := (seriesResidueProj_crt (R := R) (2 ^ a) M (pow_pos (by decide) a) hM
39     (twoPow_coprime_of_odd a M hodd) s).symm
40   exact ⟨h, h.trans (seriesResidueProj_commute _ _ _ _ _ _)⟩
41 
42 end Komorebi.Residue
43 
44 namespace Komorebi.PaperII.HilbertCoordinates
45 open Komorebi.Foundation
46 universe u v w x y
47 variable {𝕜 : Type u} [RCLike 𝕜]
48 variable {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
49 variable {ι : Type w} {κ : Type x} {τ : Type y}
50 variable [Fintype ι] [Fintype κ] [Fintype τ]
51 
52 theorem hilbertCoordinateChange_self (P : LinearProjectorFamily 𝕜 E ι)
53     (hP : ∀ i, (P.proj i).IsSymmetric) :
54     hilbertCoordinateChange P P hP hP = LinearIsometryEquiv.refl 𝕜 (HilbertPacketSpace P) := by
55   apply LinearIsometryEquiv.ext
56   intro x
57   exact (hilbertPacketUnitary P hP).apply_symm_apply x
58 
59 theorem hilbertCoordinateChange_symm (P : LinearProjectorFamily 𝕜 E ι)
60     (Q : LinearProjectorFamily 𝕜 E κ)
61     (hP : ∀ i, (P.proj i).IsSymmetric) (hQ : ∀ j, (Q.proj j).IsSymmetric) :
62     (hilbertCoordinateChange P Q hP hQ).symm = hilbertCoordinateChange Q P hQ hP := by
63   apply LinearIsometryEquiv.ext
64   intro x
65   rfl
66 
67 theorem hilbertCoordinateChange_trans (P : LinearProjectorFamily 𝕜 E ι)
68     (Q : LinearProjectorFamily 𝕜 E κ) (S : LinearProjectorFamily 𝕜 E τ)
69     (hP : ∀ i, (P.proj i).IsSymmetric) (hQ : ∀ j, (Q.proj j).IsSymmetric)
70     (hS : ∀ k, (S.proj k).IsSymmetric) :
71     (hilbertCoordinateChange P Q hP hQ).trans (hilbertCoordinateChange Q S hQ hS) =
72       hilbertCoordinateChange P S hP hS := by
73   apply LinearIsometryEquiv.ext
74   intro x
75   simp only [hilbertCoordinateChange, LinearIsometryEquiv.trans_apply,
76     LinearIsometryEquiv.symm_apply_apply]
77 
78 end Komorebi.PaperII.HilbertCoordinates
79 #print axioms Komorebi.Residue.manuscript_series_residue_packet
80 #print axioms Komorebi.Residue.manuscript_series_dyadic_odd
81 #print axioms Komorebi.PaperII.HilbertCoordinates.hilbertCoordinateChange_trans

Back to source controls