PositivePackets.lean

1 import Mathlib.Geometry.Convex.Cone.Basic
2 import Mathlib.Basic.Real.Basic
3 import Mathlib.LinearAlgebra.Pi
4 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
5 
6 /-!
7 # Positive packet mixtures
8 
9 Core 2.5, general cone sector. Probability meaning belongs to a declared convex
10 cone and a strictly positive linear mass, not to the visible signs of coordinates.
11 Only positive-mass packets are normalized. Idempotence is not needed here.
12 -/
13 namespace Komorebi.MachineTheory.PositivePackets
14 
15 noncomputable section
16 
17 open scoped BigOperators
18 
19 universe uV uI
20 variable {V : Type uV} {I : Type uI}
21 variable [AddCommGroup V] [Module ℝ V]
22 
23 /-- A mass functional detects every nonzero member of the declared cone. -/
24 def StrictMass (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ) : Prop :=
25   ∀ v ∈ C, v ≠ 0 → 0 < mass v
26 
27 /-- Actual cone preservation of each packet operator. -/
28 def Preserves (C : ConvexCone ℝ V) (P : V →ₗ[ℝ] V) : Prop :=
29   ∀ v ∈ C, P v ∈ C
30 
31 /-- A normalized state is cone membership together with unit mass. -/
32 def IsState (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ) (v : V) : Prop :=
33   v ∈ C ∧ mass v = 1
34 
35 /-- The weight of a packet is its declared mass. -/
36 def weight (mass : V →ₗ[ℝ] ℝ) (P : I → V →ₗ[ℝ] V) (v : V) (i : I) : ℝ :=
37   mass (P i v)
38 
39 /-- The type of indices for which normalization is permitted. -/
40 abbrev PositiveIndex (mass : V →ₗ[ℝ] ℝ) (P : I → V →ₗ[ℝ] V) (v : V) :=
41   {i : I // 0 < weight mass P v i}
42 
43 /-- Normalization is defined only on a positive-weight index. -/
44 def normalized (mass : V →ₗ[ℝ] ℝ) (P : I → V →ₗ[ℝ] V) (v : V)
45     (i : PositiveIndex mass P v) : V :=
46   (weight mass P v i.val)⁻¹ • P i.val v
47 
48 /-- Strict mass entails nonnegative mass, also at zero. -/
49 theorem mass_nonneg (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ)
50     (hm : StrictMass C mass) {v : V} (hv : v ∈ C) : 0 ≤ mass v := by
51   by_cases h : v = 0
52   · simp [h]
53   · exact le_of_lt (hm v hv h)
54 
55 /-- A cone member has zero mass exactly when it is the zero vector. -/
56 theorem mass_zero_iff (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ)
57     (hm : StrictMass C mass) {v : V} (hv : v ∈ C) : mass v = 0 ↔ v = 0 := by
58   constructor
59   · intro hz
60     by_contra hn
61     exact (ne_of_gt (hm v hv hn)) hz
62   · intro hz
63     simp [hz]
64 
65 /-- A cone member has positive mass exactly when it is nonzero. -/
66 theorem mass_pos_iff (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ)
67     (hm : StrictMass C mass) {v : V} (hv : v ∈ C) : 0 < mass v ↔ v ≠ 0 := by
68   constructor
69   · intro h hz
70     simp [hz] at h
71   · exact hm v hv
72 
73 /-- Every actual packet has nonnegative weight. -/
74 theorem weight_nonneg (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ)
75     (hm : StrictMass C mass) (P : I → V →ₗ[ℝ] V)
76     (hp : ∀ i, Preserves C (P i)) {v : V} (hv : v ∈ C) (i : I) :
77     0 ≤ weight mass P v i := mass_nonneg C mass hm (hp i v hv)
78 
79 /-- Zero-weight packets are zero, rather than additional normalized states. -/
80 theorem weight_zero_iff (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ)
81     (hm : StrictMass C mass) (P : I → V →ₗ[ℝ] V)
82     (hp : ∀ i, Preserves C (P i)) {v : V} (hv : v ∈ C) (i : I) :
83     weight mass P v i = 0 ↔ P i v = 0 := mass_zero_iff C mass hm (hp i v hv)
84 
85 /-- Exactly the nonzero packets can be normalized. -/
86 theorem weight_pos_iff (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ)
87     (hm : StrictMass C mass) (P : I → V →ₗ[ℝ] V)
88     (hp : ∀ i, Preserves C (P i)) {v : V} (hv : v ∈ C) (i : I) :
89     0 < weight mass P v i ↔ P i v ≠ 0 := mass_pos_iff C mass hm (hp i v hv)
90 
91 /-- The normalized positive packet belongs to the same cone. -/
92 theorem normalized_mem (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ)
93     (P : I → V →ₗ[ℝ] V) (hp : ∀ i, Preserves C (P i))
94     {v : V} (hv : v ∈ C) (i : PositiveIndex mass P v) :
95     normalized mass P v i ∈ C :=
96   C.smul_mem (inv_pos.mpr i.property) (hp i.val v hv)
97 
98 /-- Its mass is one because its weight is genuinely positive. -/
99 theorem normalized_mass (mass : V →ₗ[ℝ] ℝ) (P : I → V →ₗ[ℝ] V)
100     (v : V) (i : PositiveIndex mass P v) : mass (normalized mass P v i) = 1 := by
101   rw [normalized, map_smul]
102   change (weight mass P v i.val)⁻¹ * weight mass P v i.val = 1
103   exact inv_mul_cancel₀ (ne_of_gt i.property)
104 
105 /-- The normalized packet is an actual state, not an arbitrary division by zero. -/
106 theorem normalized_isState (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ)
107     (P : I → V →ₗ[ℝ] V) (hp : ∀ i, Preserves C (P i))
108     {v : V} (hv : v ∈ C) (i : PositiveIndex mass P v) :
109     IsState C mass (normalized mass P v i) :=
110   ⟨normalized_mem C mass P hp hv i, normalized_mass mass P v i⟩
111 
112 /-- Multiplying a normalized positive packet by its weight recovers the packet. -/
113 theorem weighted_normalized (mass : V →ₗ[ℝ] ℝ) (P : I → V →ₗ[ℝ] V)
114     (v : V) (i : PositiveIndex mass P v) :
115     weight mass P v i.val • normalized mass P v i = P i.val v := by
116   simp [normalized, smul_smul, ne_of_gt i.property]
117 
118 variable [Fintype I]
119 
120 /-- The active index type is finite, with no nonempty-index premise. -/
121 instance positiveIndexFintype (mass : V →ₗ[ℝ] ℝ) (P : I → V →ₗ[ℝ] V) (v : V) :
122     Fintype (PositiveIndex mass P v) := by
123   classical
124   exact Subtype.fintype _
125 
126 /-- Completeness is an identity of the supplied linear operators. -/
127 def Complete (P : I → V →ₗ[ℝ] V) : Prop := ∑ i, P i = LinearMap.id
128 
129 /-- Complete operators reconstruct every vector, not just normalized inputs. -/
130 theorem sum_packets (P : I → V →ₗ[ℝ] V) (hc : Complete P) (v : V) :
131     ∑ i, P i v = v := by
132   simpa only [LinearMap.sum_apply, LinearMap.id_apply] using LinearMap.congr_fun hc v
133 
134 /-- The complete family retains the original mass. -/
135 theorem sum_weights (mass : V →ₗ[ℝ] ℝ) (P : I → V →ₗ[ℝ] V)
136     (hc : Complete P) (v : V) : ∑ i, weight mass P v i = mass v := by
137   unfold weight
138   rw [← map_sum, sum_packets P hc]
139 
140 /-- A normalized input has weights summing exactly to one. -/
141 theorem sum_weights_one (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ)
142     (P : I → V →ₗ[ℝ] V) (hc : Complete P) {v : V} (hv : IsState C mass v) :
143     ∑ i, weight mass P v i = 1 := (sum_weights mass P hc v).trans hv.2
144 
145 /-- Removing the zero packets loses nothing in the reconstruction. -/
146 theorem sum_positive_packets (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ)
147     (hm : StrictMass C mass) (P : I → V →ₗ[ℝ] V)
148     (hp : ∀ i, Preserves C (P i)) (hc : Complete P) {v : V} (hv : v ∈ C) :
149     ∑ i : PositiveIndex mass P v, P i.val v = v := by
150   classical
151   let s : Finset I := Finset.univ.filter (fun i => 0 < weight mass P v i)
152   have hs : ∀ i, i ∈ s ↔ 0 < weight mass P v i := by simp [s]
153   calc
154     (∑ i : PositiveIndex mass P v, P i.val v) = ∑ i ∈ s, P i v :=
155       (Finset.sum_subtype s hs (fun i => P i v)).symm
156     _ = ∑ i, P i v := by
157       apply Finset.sum_subset (Finset.filter_subset _ _)
158       intro i _ hi
159       apply (weight_zero_iff C mass hm P hp hv i).mp
160       have hn : ¬ 0 < weight mass P v i := by simpa [s] using hi
161       exact le_antisymm (le_of_not_gt hn) (weight_nonneg C mass hm P hp hv i)
162     _ = v := sum_packets P hc v
163 
164 /-- The active weights retain the complete mass after all zero packets are removed. -/
165 theorem sum_positive_weights (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ)
166     (hm : StrictMass C mass) (P : I → V →ₗ[ℝ] V)
167     (hp : ∀ i, Preserves C (P i)) (hc : Complete P) {v : V} (hv : v ∈ C) :
168     (∑ i : PositiveIndex mass P v, weight mass P v i.val) = mass v := by
169   unfold weight
170   rw [← map_sum, sum_positive_packets C mass hm P hp hc hv]
171 
172 /-- In a normalized mixture the active weights, not only all weights, sum to one. -/
173 theorem sum_positive_weights_one (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ)
174     (hm : StrictMass C mass) (P : I → V →ₗ[ℝ] V)
175     (hp : ∀ i, Preserves C (P i)) (hc : Complete P) {v : V} (hv : IsState C mass v) :
176     (∑ i : PositiveIndex mass P v, weight mass P v i.val) = 1 :=
177   (sum_positive_weights C mass hm P hp hc hv.1).trans hv.2
178 
179 /-- Exact convex-mixture reconstruction, indexed only by positive weights. -/
180 theorem mixture_reconstruction (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ)
181     (hm : StrictMass C mass) (P : I → V →ₗ[ℝ] V)
182     (hp : ∀ i, Preserves C (P i)) (hc : Complete P) {v : V} (hv : v ∈ C) :
183     (∑ i : PositiveIndex mass P v, weight mass P v i.val • normalized mass P v i) = v := by
184   simp_rw [weighted_normalized]
185   exact sum_positive_packets C mass hm P hp hc hv
186 
187 /-- Source-facing Core 2.5 mixture theorem with all zero-weight and normalization clauses. -/
188 theorem source_core25 (C : ConvexCone ℝ V) (mass : V →ₗ[ℝ] ℝ)
189     (hm : StrictMass C mass) (P : I → V →ₗ[ℝ] V)
190     (hp : ∀ i, Preserves C (P i)) (hc : Complete P) {v : V} (hv : IsState C mass v) :
191     (∀ i, 0 ≤ weight mass P v i) ∧
192     (∑ i, weight mass P v i) = 1 ∧
193     (∀ i, weight mass P v i = 0 ↔ P i v = 0) ∧
194     (∀ i : PositiveIndex mass P v, IsState C mass (normalized mass P v i)) ∧
195     (∑ i : PositiveIndex mass P v, weight mass P v i.val • normalized mass P v i) = v :=
196   ⟨weight_nonneg C mass hm P hp hv.1, sum_weights_one C mass P hc hv,
197     weight_zero_iff C mass hm P hp hv.1, normalized_isState C mass P hp hv.1,
198     mixture_reconstruction C mass hm P hp hc hv.1⟩
199 
200 end
201 end Komorebi.MachineTheory.PositivePackets

Back to source controls