WeightedReconciliation.lean

1 import KomorebiLSM.Normed
2 import Mathlib.Analysis.InnerProductSpace.Basic
3 import Mathlib.Analysis.SpecialFunctions.Sqrt
4 import Mathlib.Data.Matrix.Basic
5 import Mathlib.Tactic.Ring
6 
7 /-! P21: weighted least squares in a common semantic space, with the actual
8 Frobenius-square specialization for finite real matrices. -/
9 set_option autoImplicit false
10 open scoped BigOperators InnerProductSpace
11 namespace Komorebi.LSM.Reconciliation
12 variable {I : Type*} [Fintype I]
13 
14 noncomputable def weightedMean {E : Type*} [AddCommGroup E] [Module ℝ E]
15     (w : I → ℝ) (x : I → E) : E := ∑ i, w i • x i
16 
17 noncomputable def weightedCost {E : Type*} [NormedAddCommGroup E]
18     (w : I → ℝ) (x : I → E) (z : E) : ℝ := ∑ i, w i*‖z-x i‖^2
19 
20 section Hilbert
21 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
22 
23 theorem weighted_cost_expansion (w : I → ℝ) (x : I → E)
24     (total : ∑ i, w i=1) (z : E) :
25     weightedCost w x z = ‖z‖^2-2*⟪z,weightedMean w x⟫_ℝ+∑ i, w i*‖x i‖^2 := by
26   have hinner : ⟪z,weightedMean w x⟫_ℝ=∑ i, w i*⟪z,x i⟫_ℝ := by
27     simp only [weightedMean, inner_sum, real_inner_smul_right]
28   rw [hinner]
29   calc
30     weightedCost w x z =
31         (∑ i, w i)*‖z‖^2-2*(∑ i, w i*⟪z,x i⟫_ℝ)+∑ i, w i*‖x i‖^2 := by
32       unfold weightedCost
33       rw [Finset.sum_mul, Finset.mul_sum, ← Finset.sum_sub_distrib, ← Finset.sum_add_distrib]
34       apply Finset.sum_congr rfl
35       intro i _
36       rw [norm_sub_sq_real]
37       ring
38     _ = _ := by rw [total, one_mul]
39 
40 theorem weighted_variance_identity (w : I → ℝ) (x : I → E)
41     (total : ∑ i, w i=1) (z : E) :
42     weightedCost w x z = ‖z-weightedMean w x‖^2+weightedCost w x (weightedMean w x) := by
43   rw [weighted_cost_expansion w x total z,
44     weighted_cost_expansion w x total (weightedMean w x), norm_sub_sq_real,
45     real_inner_self_eq_norm_sq]
46   ring
47 
48 theorem weighted_cost_minimum (w : I → ℝ) (x : I → E)
49     (total : ∑ i, w i=1) (z : E) :
50     weightedCost w x (weightedMean w x) ≤ weightedCost w x z := by
51   rw [weighted_variance_identity w x total z]
52   exact le_add_of_nonneg_left (sq_nonneg _)
53 
54 theorem weighted_cost_eq_minimum_iff (w : I → ℝ) (x : I → E)
55     (total : ∑ i, w i=1) (z : E) :
56     weightedCost w x z = weightedCost w x (weightedMean w x) ↔ z=weightedMean w x := by
57   rw [weighted_variance_identity w x total z]
58   constructor
59   · intro h
60     have hn : ‖z-weightedMean w x‖^2=0 := by linarith
61     exact sub_eq_zero.mp (norm_eq_zero.mp (sq_eq_zero_iff.mp hn))
62   · intro h
63     rw [h, sub_self, norm_zero, zero_pow (by decide : (2:ℕ) ≠ 0), zero_add]
64 
65 theorem weighted_unique_minimizer (w : I → ℝ) (x : I → E)
66     (total : ∑ i, w i=1) :
67     ∃! z : E, ∀ y, weightedCost w x z ≤ weightedCost w x y := by
68   refine ⟨weightedMean w x, weighted_cost_minimum w x total, ?_⟩
69   intro z hz
70   apply (weighted_cost_eq_minimum_iff w x total z).mp
71   exact le_antisymm (hz _) (weighted_cost_minimum w x total z)
72 
73 end Hilbert
74 
75 section Normed
76 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
77 
78 theorem weighted_mean_sub (w : I → ℝ) (x : I → E)
79     (total : ∑ i, w i=1) (target : E) :
80     weightedMean w x-target=∑ i, w i • (x i-target) := by
81   simp only [smul_sub, Finset.sum_sub_distrib, ← Finset.sum_smul, total, one_smul, weightedMean]
82 
83 theorem weighted_target_error (w : I → ℝ) (x : I → E)
84     (positive : ∀ i, 0 ≤ w i) (total : ∑ i, w i=1) (target : E) :
85     ‖weightedMean w x-target‖ ≤ ∑ i, w i*‖x i-target‖ := by
86   rw [weighted_mean_sub w x total target]
87   apply (norm_sum_le _ _).trans
88   apply Finset.sum_le_sum
89   intro i _
90   rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (positive i)]
91 
92 end Normed
93 
94 /-- Frobenius square, explicitly distinct from an induced operator norm. -/
95 noncomputable def frobeniusSq {J K : Type*} [Fintype J] [Fintype K]
96     (A : Matrix J K ℝ) : ℝ := ∑ j, ∑ k, (A j k)^2
97 
98 noncomputable def frobeniusNorm {J K : Type*} [Fintype J] [Fintype K]
99     (A : Matrix J K ℝ) : ℝ := Real.sqrt (frobeniusSq A)
100 
101 theorem frobeniusNorm_sq {J K : Type*} [Fintype J] [Fintype K] (A : Matrix J K ℝ) :
102     frobeniusNorm A^2=frobeniusSq A := by
103   apply Real.sq_sqrt
104   exact Finset.sum_nonneg (fun _ _ => Finset.sum_nonneg (fun _ _ => sq_nonneg _))
105 
106 theorem frobeniusSq_nonneg {J K : Type*} [Fintype J] [Fintype K] (A : Matrix J K ℝ) :
107     0 ≤ frobeniusSq A :=
108   Finset.sum_nonneg (fun _ _ => Finset.sum_nonneg (fun _ _ => sq_nonneg _))
109 
110 theorem frobeniusSq_eq_zero_iff {J K : Type*} [Fintype J] [Fintype K] (A : Matrix J K ℝ) :
111     frobeniusSq A=0 ↔ A=0 := by
112   classical
113   constructor
114   · intro h
115     ext j k
116     have hj := (Finset.sum_eq_zero_iff_of_nonneg
117       (fun j _ => Finset.sum_nonneg (fun k _ => sq_nonneg (A j k)))).mp h j (Finset.mem_univ j)
118     have hjk := (Finset.sum_eq_zero_iff_of_nonneg (fun k _ => sq_nonneg (A j k))).mp hj k (Finset.mem_univ k)
119     exact sq_eq_zero_iff.mp hjk
120   · rintro rfl
121     simp [frobeniusSq]
122 
123 noncomputable def frobeniusCost {J K : Type*} [Fintype J] [Fintype K]
124     (w : I → ℝ) (A : I → Matrix J K ℝ) (M : Matrix J K ℝ) : ℝ :=
125   ∑ i, w i*frobeniusSq (M-A i)
126 
127 /-- The general least-squares identity is instantiated at every matrix entry. -/
128 theorem frobenius_variance_identity {J K : Type*} [Fintype J] [Fintype K]
129     (w : I → ℝ) (A : I → Matrix J K ℝ) (total : ∑ i, w i=1) (M : Matrix J K ℝ) :
130     frobeniusCost w A M = frobeniusSq (M-weightedMean w A)+frobeniusCost w A (weightedMean w A) := by
131   have hc : ∀ j k, (∑ i, w i*(M j k-A i j k)^2) =
132       (M j k-weightedMean w A j k)^2+
133       (∑ i, w i*(weightedMean w A j k-A i j k)^2) := by
134     intro j k
135     simpa only [weightedCost, weightedMean, Matrix.sum_apply, Matrix.smul_apply, smul_eq_mul,
136       Real.norm_eq_abs, sq_abs] using
137       weighted_variance_identity w (fun i => A i j k) total (M j k)
138   have swap (f : I → J → K → ℝ) :
139       (∑ i, ∑ j, ∑ k, f i j k) = ∑ j, ∑ k, ∑ i, f i j k := by
140     rw [Finset.sum_comm]
141     apply Finset.sum_congr rfl
142     intro j _
143     rw [Finset.sum_comm]
144   unfold frobeniusCost frobeniusSq
145   simp only [Matrix.sub_apply, Finset.mul_sum]
146   rw [swap (fun i j k => w i*(M j k-A i j k)^2),
147       swap (fun i j k => w i*(weightedMean w A j k-A i j k)^2)]
148   simp_rw [hc, Finset.sum_add_distrib]
149 
150 theorem frobenius_unique_minimizer {J K : Type*} [Fintype J] [Fintype K]
151     (w : I → ℝ) (A : I → Matrix J K ℝ) (total : ∑ i, w i=1) :
152     ∃! M : Matrix J K ℝ, ∀ N, frobeniusCost w A M ≤ frobeniusCost w A N := by
153   have hmin : ∀ N, frobeniusCost w A (weightedMean w A) ≤ frobeniusCost w A N := by
154     intro N
155     rw [frobenius_variance_identity w A total N]
156     exact le_add_of_nonneg_left (frobeniusSq_nonneg _)
157   refine ⟨weightedMean w A,hmin,?_⟩
158   intro M hM
159   have hz : frobeniusSq (M-weightedMean w A)=0 := by
160     have h := hM (weightedMean w A)
161     rw [frobenius_variance_identity w A total M] at h
162     linarith [frobeniusSq_nonneg (M-weightedMean w A)]
163   exact sub_eq_zero.mp ((frobeniusSq_eq_zero_iff _).mp hz)
164 
165 end Komorebi.LSM.Reconciliation

Back to source controls