FiniteGram.lean

1 import Mathlib.Algebra.BigOperators.Ring.Finset
2 import Mathlib.Basic.Real.Basic
3 import Mathlib.Algebra.BigOperators.Group.Finset.Sigma
4 import Mathlib.Algebra.Order.BigOperators.Group.Finset
5 import Mathlib.Tactic.Ring
6 
7 /-!
8 # Finite exact algebra for the Quadratic-Form Engine
9 
10 These definitions use exact real arithmetic. They model a factor A with sample
11 coordinates i and variant coordinates k. No floating-point implementation or
12 probability-distribution theorem is asserted by this module.
13 -/
14 
15 namespace KomorebiQCOS
16 
17 open scoped BigOperators
18 
19 variable {Row Variant : Type*} [Fintype Row] [DecidableEq Variant]
20 
21 /- An entry of the sample Gram matrix A_s A_sᵀ. -/
22 def gramEntry (s : Finset Variant) (A : Row → Variant → ℝ) (i j : Row) : ℝ :=
23   ∑ k ∈ s, A i k * A j k
24 
25 /- Exact action of a finite sample-coordinate matrix on a vector. -/
26 def matrixAction (K : Row → Row → ℝ) (v : Row → ℝ) (i : Row) : ℝ :=
27   ∑ j, K i j * v j
28 
29 /- Factor action evaluated one variant coordinate at a time. -/
30 def streamedAction (s : Finset Variant) (A : Row → Variant → ℝ)
31     (v : Row → ℝ) (i : Row) : ℝ :=
32   ∑ k ∈ s, A i k * (∑ j, A j k * v j)
33 
34 /- Exact real quadratic form vᵀKv. -/
35 def quadraticForm (K : Row → Row → ℝ) (v : Row → ℝ) : ℝ :=
36   ∑ i, v i * matrixAction K v i
37 
38 /- Sum of squares of factor-coordinate projections. -/
39 def factorEnergy (s : Finset Variant) (A : Row → Variant → ℝ)
40     (v : Row → ℝ) : ℝ :=
41   ∑ k ∈ s, (∑ i, A i k * v i) ^ 2
42 
43 omit [Fintype Row] [DecidableEq Variant] in
44 @[simp] theorem gramEntry_empty (A : Row → Variant → ℝ) (i j : Row) :
45     gramEntry ∅ A i j = 0 := by
46   simp [gramEntry]
47 
48 omit [Fintype Row] [DecidableEq Variant] in
49 @[simp] theorem gramEntry_singleton (k : Variant) (A : Row → Variant → ℝ)
50     (i j : Row) : gramEntry {k} A i j = A i k * A j k := by
51   simp [gramEntry]
52 
53 omit [Fintype Row] [DecidableEq Variant] in
54 theorem gramEntry_symm (s : Finset Variant) (A : Row → Variant → ℝ)
55     (i j : Row) : gramEntry s A i j = gramEntry s A j i := by
56   simp [gramEntry, mul_comm]
57 
58 /- Splitting a variant block into disjoint children preserves each Gram entry. -/
59 omit [Fintype Row] in
60 theorem gramEntry_union (s t : Finset Variant) (h : Disjoint s t)
61     (A : Row → Variant → ℝ) (i j : Row) :
62     gramEntry (s ∪ t) A i j = gramEntry s A i j + gramEntry t A i j := by
63   simp only [gramEntry, Finset.sum_union h]
64 
65 /- A bijection of variant coordinates, with factor columns moved along it,
66 preserves the exact sample Gram entry. -/
67 omit [Fintype Row] [DecidableEq Variant] in
68 theorem gramEntry_reindex (s : Finset Variant) (e : Variant ≃ Variant)
69     (A : Row → Variant → ℝ) (i j : Row) :
70     gramEntry (s.map e.toEmbedding) (fun i k => A i (e.symm k)) i j =
71       gramEntry s A i j := by
72   simp [gramEntry, Finset.sum_map]
73 
74 /- Streamed factor multiplication agrees with multiplication by A_s A_sᵀ. -/
75 omit [DecidableEq Variant] in
76 theorem matrixAction_gram_eq_streamed (s : Finset Variant)
77     (A : Row → Variant → ℝ) (v : Row → ℝ) (i : Row) :
78     matrixAction (gramEntry s A) v i = streamedAction s A v i := by
79   simp only [matrixAction, gramEntry, streamedAction,
80     Finset.sum_mul, Finset.mul_sum, mul_assoc]
81   rw [Finset.sum_comm]
82 
83 theorem matrixAction_add (K L : Row → Row → ℝ) (v : Row → ℝ) (i : Row) :
84     matrixAction (fun i j => K i j + L i j) v i =
85       matrixAction K v i + matrixAction L v i := by
86   simp [matrixAction, add_mul, Finset.sum_add_distrib]
87 
88 /- Refinement also preserves every streamed sample-coordinate action. -/
89 theorem matrixAction_gram_union (s t : Finset Variant) (h : Disjoint s t)
90     (A : Row → Variant → ℝ) (v : Row → ℝ) (i : Row) :
91     matrixAction (gramEntry (s ∪ t) A) v i =
92       matrixAction (gramEntry s A) v i + matrixAction (gramEntry t A) v i := by
93   simp only [matrixAction, gramEntry_union s t h, add_mul,
94     Finset.sum_add_distrib]
95 
96 theorem streamedAction_union (s t : Finset Variant) (h : Disjoint s t)
97     (A : Row → Variant → ℝ) (v : Row → ℝ) (i : Row) :
98     streamedAction (s ∪ t) A v i =
99       streamedAction s A v i + streamedAction t A v i := by
100   simp only [streamedAction, Finset.sum_union h]
101 
102 theorem quadraticForm_add (K L : Row → Row → ℝ) (v : Row → ℝ) :
103     quadraticForm (fun i j => K i j + L i j) v =
104       quadraticForm K v + quadraticForm L v := by
105   simp [quadraticForm, matrixAction_add, mul_add, Finset.sum_add_distrib]
106 
107 /- The quadratic form of a Gram matrix equals a sum of squares. -/
108 omit [DecidableEq Variant] in
109 theorem quadraticForm_gram_eq_energy (s : Finset Variant)
110     (A : Row → Variant → ℝ) (v : Row → ℝ) :
111     quadraticForm (gramEntry s A) v = factorEnergy s A v := by
112   simp only [quadraticForm, matrixAction_gram_eq_streamed,
113     streamedAction, factorEnergy, pow_two, Finset.mul_sum, Finset.sum_mul]
114   rw [Finset.sum_comm]
115   apply Finset.sum_congr rfl
116   intro k hk
117   apply Finset.sum_congr rfl
118   intro i hi
119   apply Finset.sum_congr rfl
120   intro j hj
121   ring
122 
123 /- Positive semidefiniteness of the exact Gram form. -/
124 omit [DecidableEq Variant] in
125 theorem quadraticForm_gram_nonneg (s : Finset Variant)
126     (A : Row → Variant → ℝ) (v : Row → ℝ) :
127     0 ≤ quadraticForm (gramEntry s A) v := by
128   rw [quadraticForm_gram_eq_energy]
129   exact Finset.sum_nonneg (fun k hk => sq_nonneg (∑ i, A i k * v i))
130 
131 /- Splitting a block preserves the exact quadratic statistic as well. -/
132 theorem quadraticForm_gram_union (s t : Finset Variant) (h : Disjoint s t)
133     (A : Row → Variant → ℝ) (v : Row → ℝ) :
134     quadraticForm (gramEntry (s ∪ t) A) v =
135       quadraticForm (gramEntry s A) v + quadraticForm (gramEntry t A) v := by
136   simp only [quadraticForm, matrixAction_gram_union s t h, mul_add,
137     Finset.sum_add_distrib]
138 
139 /- A supplied diagonal spectral form. No diagonalization theorem is assumed. -/
140 def weightedSquares (s : Finset Variant) (coeff z : Variant → ℝ) : ℝ :=
141   ∑ k ∈ s, coeff k * z k ^ 2
142 
143 /- Coefficient intervals give pointwise order for supplied diagonal forms.
144 This statement even permits signed coefficients; the squared coordinates are
145 nonnegative. -/
146 omit [Fintype Row] [DecidableEq Variant] in
147 theorem weightedSquares_mono (s : Finset Variant)
148     (lower upper z : Variant → ℝ) (h : ∀ k ∈ s, lower k ≤ upper k) :
149     weightedSquares s lower z ≤ weightedSquares s upper z := by
150   apply Finset.sum_le_sum
151   intro k hk
152   exact mul_le_mul_of_nonneg_right (h k hk) (sq_nonneg (z k))
153 
154 omit [Fintype Row] [DecidableEq Variant] in
155 theorem weightedSquares_nonneg (s : Finset Variant)
156     (coeff z : Variant → ℝ) (h : ∀ k ∈ s, 0 ≤ coeff k) :
157     0 ≤ weightedSquares s coeff z := by
158   exact Finset.sum_nonneg (fun k hk => mul_nonneg (h k hk) (sq_nonneg (z k)))
159 
160 /- A pointwise tail-event implication. Passing to probabilities requires a
161 separate measure-theoretic monotonicity argument. -/
162 omit [Fintype Row] [DecidableEq Variant] in
163 theorem weightedSquares_tail_imp (s : Finset Variant)
164     (lower upper z : Variant → ℝ) (q : ℝ)
165     (h : ∀ k ∈ s, lower k ≤ upper k)
166     (htail : q ≤ weightedSquares s lower z) :
167     q ≤ weightedSquares s upper z := by
168   exact htail.trans (weightedSquares_mono s lower upper z h)
169 
170 end KomorebiQCOS

Back to source controls