Block8ApproximationExamples.lean

1 import KomorebiLSM.Block8Examples
2 import KomorebiLSM.ReconciliationHilbert
3 import Mathlib.Analysis.SpecificLimits.Basic
4 import Mathlib.Analysis.SpecificLimits.Normed
5 
6 /-! Concrete nonlinear, chart and horizon examples. All equalities are exact;
7 no sampled trajectories establish the general limits or bounds. -/
8 set_option autoImplicit false
9 open scoped BigOperators Topology
10 open Filter
11 namespace Komorebi.LSM.Block8ApproximationExamples
12 open Komorebi.LSM.Stability Komorebi.LSM.PacketApproximation
13 open Komorebi.LSM.Reconciliation Komorebi.LSM.Block8Examples
14 
15 noncomputable def rate (n : ℕ) : ℝ := (n:ℝ)/((n:ℝ)+1)
16 
17 theorem rate_bounds (n : ℕ) : 0 ≤ rate n ∧ rate n < 1 := by
18   have hn : (0:ℝ) ≤ n := Nat.cast_nonneg n
19   constructor
20   · exact div_nonneg hn (by linarith)
21   · apply (div_lt_one (by positivity : (0:ℝ) < n+1)).mpr
22     linarith
23 
24 theorem rate_tendsto : Tendsto rate atTop (𝓝 1) := tendsto_natCast_div_add_atTop 1
25 
26 theorem scale_power_apply (r x : ℝ) (k : ℕ) : ((scale r)^k) x=r^k*x := by
27   induction k with
28   | zero => simp
29   | succ k ih => rw [pow_succ',mul_apply_eq_comp,ih,scale_apply,pow_succ']; ring
30 
31 /-- The general fixed-power theorem applies even though uniform-in-time error
32 will fail below. These are approximating operators, not projection maps. -/
33 theorem scalar_fixed_horizon_convergence (x : ℝ) (k : ℕ) :
34     Tendsto (fun n => ((scale (rate n))^k) x) atTop (𝓝 x) := by
35   have h := strong_fixed_powers (fun n => scale (rate n)) (ContinuousLinearMap.id ℝ ℝ)
36     (C:=1) (fun n => by rw [scale_norm,abs_of_nonneg (rate_bounds n).1]; exact (rate_bounds n).2.le)
37     (fun y => by simpa only [scale_apply,one_mul,ContinuousLinearMap.id_apply] using rate_tendsto.mul_const y) x k
38   simpa using h
39 
40 theorem each_resolution_has_large_late_error (n : ℕ) :
41     Tendsto (fun k : ℕ => ‖((scale (rate n))^k) (1:ℝ)-1‖) atTop (𝓝 1) := by
42   have h := (tendsto_pow_atTop_nhds_zero_of_lt_one (rate_bounds n).1 (rate_bounds n).2).sub_const 1
43   have hn := h.norm
44   simpa only [scale_power_apply,mul_one,zero_sub,norm_neg,norm_one] using hn
45 
46 theorem refinement_horizon_cannot_be_exchanged :
47     ‖((scale (rate 1))^1) (1:ℝ)-1‖=1/2 ∧
48     ‖((scale (rate 1))^2) (1:ℝ)-1‖=3/4 := by
49   norm_num [scale_power_apply,rate]
50 
51 noncomputable def packet (i : Bool) : (ℝ×ℝ) →L[ℝ] (ℝ×ℝ) :=
52   if i then (0 : (ℝ×ℝ) →L[ℝ] ℝ).prod (ContinuousLinearMap.snd ℝ ℝ ℝ)
53   else (ContinuousLinearMap.fst ℝ ℝ ℝ).prod 0
54 
55 noncomputable def sumCoordinate : (ℝ×ℝ) →L[ℝ] ℝ :=
56   ContinuousLinearMap.fst ℝ ℝ ℝ+ContinuousLinearMap.snd ℝ ℝ ℝ
57 
58 noncomputable def powerTerm (m : ℕ) :
59     ContinuousMultilinearMap ℝ (fun _ : Fin (m+1) => ℝ×ℝ) ℝ :=
60   (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin (m+1)) ℝ).compContinuousLinearMap
61     (fun _ => sumCoordinate)
62 
63 theorem packet_complete (x : ℝ×ℝ) : ∑ i : Bool, packet i x=x := by
64   ext <;> simp [packet]
65 
66 theorem packet_contractive (i : Bool) : ‖packet i‖ ≤ 1 := by
67   apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one
68   intro x
69   cases i <;> simp [packet,Prod.norm_def]
70 
71 theorem packet_range_coordinate_norm (i : Bool) (v : ℝ×ℝ)
72     (hv : v ∈ LinearMap.range (packet i).toLinearMap) : |v.1+v.2|=‖v‖ := by
73   obtain ⟨w,hw⟩ := hv
74   rw [← hw]
75   cases i <;> simp [packet,Prod.norm_def,Real.norm_eq_abs]
76 
77 theorem powerTerm_apply (m : ℕ) (v : Fin (m+1) → ℝ×ℝ) :
78     powerTerm m v=∏ k, ((v k).1+(v k).2) := by
79   simp [powerTerm,sumCoordinate]
80 
81 theorem powerTerm_packet_bound (m : ℕ) (f : Fin (m+1) → Bool) :
82     HasPacketBound packet (powerTerm m) f 1 := by
83   intro v hv
84   rw [powerTerm_apply,one_mul,Real.norm_eq_abs,Finset.abs_prod]
85   apply le_of_eq
86   exact Finset.prod_congr rfl (fun k _ => packet_range_coordinate_norm (f k) (v k) (hv k))
87 
88 noncomputable def diagonalTuples (m : ℕ) : Finset (Fin (m+1) → Bool) :=
89   {fun _ => false,fun _ => true}
90 
91 noncomputable def fullQuadratic : (ℝ×ℝ) → ℝ :=
92   fullPolynomial 2 (fun m => powerTerm m.val) 0
93 
94 noncomputable def diagonalQuadratic : (ℝ×ℝ) → ℝ :=
95   retainedPolynomial 2 packet (fun m => powerTerm m.val) (fun m => diagonalTuples m.val) 0
96 
97 theorem fullQuadratic_formula (x : ℝ×ℝ) :
98     fullQuadratic x=x.1+x.2+(x.1+x.2)^2 := by
99   simp [fullQuadratic,fullPolynomial,Fin.sum_univ_succ,powerTerm_apply]
100 
101 theorem diagonalQuadratic_formula (x : ℝ×ℝ) :
102     diagonalQuadratic x=x.1+x.2+x.1^2+x.2^2 := by
103   simp [diagonalQuadratic,retainedPolynomial,Fin.sum_univ_succ,diagonalTuples,
104     powerTerm_apply,Fin.prod_univ_succ,packet,funext_iff]
105   ring
106 
107 theorem quadratic_omitted_interaction (x : ℝ×ℝ) :
108     fullQuadratic x-diagonalQuadratic x=2*x.1*x.2 := by
109   rw [fullQuadratic_formula,diagonalQuadratic_formula]
110   ring
111 
112 theorem quadratic_sharp_error (x : ℝ×ℝ) :
113     ‖fullQuadratic x-diagonalQuadratic x‖=2 * |x.1| * |x.2| := by
114   rw [quadratic_omitted_interaction,Real.norm_eq_abs,abs_mul,abs_mul]
115   norm_num
116 
117 /-- The true block bounds above instantiate the general ordered-tuple theorem. -/
118 theorem quadratic_general_truncation_bound (x : ℝ×ℝ) :
119     ‖fullQuadratic x-diagonalQuadratic x‖ ≤
120       ∑ m : Fin 2, ∑ f ∈ Finset.univ \ diagonalTuples m.val,
121         (1:ℝ)*∏ k, ‖packet (f k) x‖ := by
122   exact packet_interaction_truncation_bound 2 packet packet_complete
123     (fun m => powerTerm m.val) (fun m => diagonalTuples m.val) (fun _ _ => 1)
124     (fun m f => powerTerm_packet_bound m.val f) 0 x
125 
126 theorem quadratic_general_lipschitz (x y : ℝ×ℝ) {R : ℝ} (hR : 0 ≤ R)
127     (hx : ‖x‖ ≤ R) (hy : ‖y‖ ≤ R) :
128     ‖diagonalQuadratic x-diagonalQuadratic y‖ ≤
129       (∑ m : Fin 2, ∑ _f ∈ diagonalTuples m.val, (m.val+1:ℕ)*(1:ℝ)*R^m.val)*‖x-y‖ := by
130   exact retained_polynomial_lipschitz_bound 2 packet packet_contractive
131     (fun m => powerTerm m.val) (fun m => diagonalTuples m.val) (fun _ _ => 1)
132     (fun _ _ => zero_le_one) (fun m f => powerTerm_packet_bound m.val f) 0 hR x y hx hy
133 
134 theorem nonlinear_cross_term_numeric : fullQuadratic (2,3)-diagonalQuadratic (2,3)=12 := by
135   rw [quadratic_omitted_interaction]
136   norm_num
137 
138 noncomputable def chartWeights : Fin 2 → ℝ := ![1/4,3/4]
139 noncomputable def chartFits : Fin 2 → ℝ := ![2,4]
140 
141 theorem chartWeights_total : ∑ i, chartWeights i=1 := by norm_num [chartWeights,Fin.sum_univ_succ]
142 
143 theorem chart_mean : weightedMean chartWeights chartFits=7/2 := by
144   norm_num [weightedMean,chartWeights,chartFits,Fin.sum_univ_succ]
145 
146 theorem chart_minimum_cost : weightedCost chartWeights chartFits (7/2)=3/4 := by
147   norm_num [weightedCost,chartWeights,chartFits,Fin.sum_univ_succ]
148 
149 theorem chart_unique_minimum : ∀ x : ℝ,
150     weightedCost chartWeights chartFits x=3/4 ↔ x=7/2 := by
151   intro x
152   have h := weighted_cost_eq_minimum_iff chartWeights chartFits chartWeights_total x
153   simpa only [chart_mean,chart_minimum_cost] using h
154 
155 theorem unanimous_wrong_fit : weightedMean chartWeights (fun _ => (4:ℝ))=4 := by
156   norm_num [weightedMean,chartWeights,Fin.sum_univ_succ]
157 
158 noncomputable def redundantAtlas : LinearAtlas ℝ (ℝ×ℝ) where
159   analysis := (LinearMap.id).prod ((2:ℝ) • LinearMap.id)
160   synthesis := LinearMap.fst ℝ ℝ ℝ
161   reconstruct := fun _ => rfl
162 
163 noncomputable def scaledAtlas : LinearAtlas ℝ ℝ where
164   analysis := (3:ℝ) • LinearMap.id
165   synthesis := (1/3:ℝ) • LinearMap.id
166   reconstruct := by intro x; change (1/3:ℝ)*(3*x)=x; ring
167 
168 theorem chart_transport_exact :
169     redundantAtlas.transport scaledAtlas (redundantAtlas.encode 2)=scaledAtlas.encode 2 := by
170   simp [LinearAtlas.transport]
171 
172 theorem chart_transport_pullback_distance (c d : redundantAtlas.Coeff) :
173     dist (scaledAtlas.decode (redundantAtlas.transport scaledAtlas c))
174       (scaledAtlas.decode (redundantAtlas.transport scaledAtlas d)) =
175       dist (redundantAtlas.decode c) (redundantAtlas.decode d) := by
176   rw [LinearAtlas.decode_transport,LinearAtlas.decode_transport]
177 
178 theorem invalid_redundant_coefficient : (1,0) ∉ redundantAtlas.analysis.range := by
179   rintro ⟨x,h⟩
180   have h1 := congrArg Prod.fst h
181   have h2 := congrArg Prod.snd h
182   change x=1 at h1
183   change (2:ℝ)*x=0 at h2
184   linarith
185 
186 theorem repaired_ambient_output_is_realizable (L : ℝ →ₗ[ℝ] ℝ) :
187     redundantAtlas.repaired L (1,0) ∈ redundantAtlas.analysis.range :=
188   redundantAtlas.repaired_consistent L (1,0)
189 
190 end Komorebi.LSM.Block8ApproximationExamples

Back to source controls