DyadicSupport.lean

1 import KomorebiSpace.DyadicInfiniteReconstruction
2 import Mathlib.NumberTheory.Padics.PadicVal.Basic
3 
4 set_option autoImplicit false
5 
6 /-!
7 # KS55: congruence support of the actual dyadic residual remainder
8 
9 These statements use the original varying operator fibers, coarseners, target
10 sections and residual remainder. No fixed scalar replacement is introduced.
11 -/
12 universe u v
13 noncomputable section
14 namespace KomorebiSpace.DyadicResidual.System
15 open BanachTower
16 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
17 variable (T : System.{u,v} 𝕜)
18 
19 theorem finite_details_zero_coordinate_of_not_dvd (r : Residuals T.source T.target)
20     (N j k : ℕ)
21     (hd : ∀ i < N, T.cascade.detail r (j+i) = 0)
22     (hk : ¬ 2^N ∣ k+1) : T.residualLevel r j k = 0 := by
23   induction N generalizing j k with
24   | zero => exact (hk (by simp)).elim
25   | succ N ih =>
26     let U := T.stage j
27     have hh : hidden U.source U.target U.source_contractive U.target_contractive
28         U.target_splitting (T.residualLevel r j) = 0 := by
29       have h := hd 0 (Nat.zero_lt_succ N)
30       rw [Nat.add_zero] at h
31       exact h
32     have hpar : k = 2*(k/2) ∨ k = 2*(k/2)+1 := by omega
33     rcases hpar with he | ho
34     · have hv := congrArg (fun f : Residuals U.source U.target => f (2*(k/2))) hh
35       rw [hidden_even] at hv
36       rw [he]
37       exact hv
38     · have hv := congrArg (fun f : Residuals U.source U.target => f (2*(k/2)+1)) hh
39       rw [hidden_odd] at hv
40       have hk' : ¬ 2^N ∣ k/2+1 := by
41         rintro ⟨t, ht⟩
42         apply hk
43         refine ⟨t, ?_⟩
44         calc
45           k+1 = 2*(k/2+1) := by omega
46           _ = 2*(2^N*t) := by rw [ht]
47           _ = 2^(N+1)*t := by rw [pow_succ]; ring
48       have hd' : ∀ i < N, T.cascade.detail r ((j+1)+i) = 0 := by
49         intro i hi
50         rw [show j+1+i = j+(i+1) by omega]
51         exact hd (i+1) (by omega)
52       have hc : coarsen U.source U.target U.source_contractive U.target_contractive
53           (T.residualLevel r j) (k/2) = 0 := ih (j+1) (k/2) hd' hk'
54       change T.residualLevel r j (2*(k/2)+1) -
55         (U.target_splitting.up (2*(k/2))).comp
56           (coarsen U.source U.target U.source_contractive U.target_contractive
57             (T.residualLevel r j) (k/2)) = 0 at hv
58       rw [hc, ContinuousLinearMap.comp_zero, sub_zero] at hv
59       rw [ho]
60       exact hv
61 
62 theorem remainder_coordinate_zero_of_not_dvd
63     (r : Residuals T.source T.target) (N k : ℕ) (hk : ¬ 2^N ∣ k+1) :
64     T.residualRemainder N r k = 0 := by
65   have hd : ∀ i < N, T.cascade.detail (T.residualRemainder N r) (0+i) = 0 := by
66     intro i hi
67     rw [Nat.zero_add]
68     exact T.cascade.remainder_details_below r N i hi
69   exact T.finite_details_zero_coordinate_of_not_dvd (T.residualRemainder N r) N 0 k hd hk
70 
71 theorem reconstruction_coordinate_of_not_dvd
72     (r : Residuals T.source T.target) (N k : ℕ) (hk : ¬ 2^N ∣ k+1) :
73     T.reconstructedResidual N r k = r k := by
74   change r k - T.residualRemainder N r k = r k
75   rw [T.remainder_coordinate_zero_of_not_dvd r N k hk, sub_zero]
76 
77 /-- Nonzero remainder coordinates must belong to the indicated congruence class. -/
78 theorem nonzero_remainder_requires_divisibility
79     (r : Residuals T.source T.target) (N k : ℕ)
80     (hk : T.residualRemainder N r k ≠ 0) : 2^N ∣ k+1 := by
81   by_contra h
82   exact hk (T.remainder_coordinate_zero_of_not_dvd r N k h)
83 
84 /-- The precise sufficient coordinate threshold is the dyadic valuation, not the index. -/
85 theorem reconstruction_after_valuation
86     (r : Residuals T.source T.target) (N k : ℕ)
87     (hk : padicValNat 2 (k+1) < N) : T.reconstructedResidual N r k = r k := by
88   apply T.reconstruction_coordinate_of_not_dvd r N k
89   rw [padicValNat_dvd_iff_le_of_ne_one (by decide : (2:ℕ) ≠ 1) (by omega : k+1 ≠ 0)]
90   exact Nat.not_le_of_lt hk
91 
92 end KomorebiSpace.DyadicResidual.System
93 end

Back to source controls