PacketTransport.lean

1 import MachineTheory.PositivePackets
2 
3 /-!
4 # Transporting the cone, mass and packets together
5 
6 An invertible real-linear change of coordinates preserves mixture meaning only
7 when the cone and mass are transported with the operators. Coordinate signs
8 alone have no invariant probability meaning.
9 -/
10 namespace Komorebi.MachineTheory.PositivePackets.Transport
11 
12 noncomputable section
13 
14 open scoped BigOperators
15 
16 universe uV uW uI
17 variable {V : Type uV} {W : Type uW} {I : Type uI}
18 variable [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W]
19 
20 /-- The transported cone is the actual image of the original cone. -/
21 def cone (e : V ≃ₗ[ℝ] W) (C : ConvexCone ℝ V) : ConvexCone ℝ W :=
22   C.map e.toLinearMap
23 
24 /-- Mass is read after applying the inverse coordinate map. -/
25 def mass (e : V ≃ₗ[ℝ] W) (m : V →ₗ[ℝ] ℝ) : W →ₗ[ℝ] ℝ :=
26   m.comp e.symm.toLinearMap
27 
28 /-- The actual conjugated operation. -/
29 def operator (e : V ≃ₗ[ℝ] W) (P : V →ₗ[ℝ] V) : W →ₗ[ℝ] W :=
30   e.toLinearMap.comp (P.comp e.symm.toLinearMap)
31 
32 @[simp] theorem cone_mem (e : V ≃ₗ[ℝ] W) (C : ConvexCone ℝ V) (v : V) :
33     e v ∈ cone e C ↔ v ∈ C := by
34   simp [cone, ConvexCone.mem_map]
35 
36 @[simp] theorem mass_apply (e : V ≃ₗ[ℝ] W) (m : V →ₗ[ℝ] ℝ) (v : V) :
37     mass e m (e v) = m v := by simp [mass]
38 
39 @[simp] theorem operator_apply (e : V ≃ₗ[ℝ] W) (P : V →ₗ[ℝ] V) (v : V) :
40     operator e P (e v) = e (P v) := by simp [operator]
41 
42 /-- Strict positivity survives actual coordinate transport. -/
43 theorem strictMass (e : V ≃ₗ[ℝ] W) (C : ConvexCone ℝ V) (m : V →ₗ[ℝ] ℝ)
44     (hm : StrictMass C m) : StrictMass (cone e C) (mass e m) := by
45   intro w hw hn
46   obtain ⟨v, rfl⟩ := e.surjective w
47   rw [mass_apply]
48   apply hm v ((cone_mem e C v).mp hw)
49   intro hz
50   apply hn
51   simp [hz]
52 
53 /-- Cone preservation is transported, not replaced by coordinate nonnegativity. -/
54 theorem preserves (e : V ≃ₗ[ℝ] W) (C : ConvexCone ℝ V) (P : V →ₗ[ℝ] V)
55     (hp : Preserves C P) : Preserves (cone e C) (operator e P) := by
56   intro w hw
57   obtain ⟨v, rfl⟩ := e.surjective w
58   rw [operator_apply, cone_mem]
59   exact hp v ((cone_mem e C v).mp hw)
60 
61 /-- Normalized state membership is equivalent in the two coordinate systems. -/
62 theorem state_iff (e : V ≃ₗ[ℝ] W) (C : ConvexCone ℝ V) (m : V →ₗ[ℝ] ℝ) (v : V) :
63     IsState (cone e C) (mass e m) (e v) ↔ IsState C m v := by
64   simp [IsState]
65 
66 /-- Each packet retains exactly its old weight. -/
67 theorem weight_eq (e : V ≃ₗ[ℝ] W) (m : V →ₗ[ℝ] ℝ)
68     (P : I → V →ₗ[ℝ] V) (v : V) (i : I) :
69     weight (mass e m) (fun j => operator e (P j)) (e v) i = weight m P v i := by
70   simp [weight]
71 
72 /-- An original active index is active after transport. -/
73 def index (e : V ≃ₗ[ℝ] W) (m : V →ₗ[ℝ] ℝ) (P : I → V →ₗ[ℝ] V) (v : V)
74     (i : PositiveIndex m P v) : PositiveIndex (mass e m) (fun j => operator e (P j)) (e v) :=
75   ⟨i.val, by simpa only [weight_eq] using i.property⟩
76 
77 /-- Positive-weight normalization commutes with the coordinate transformation. -/
78 theorem normalized_eq (e : V ≃ₗ[ℝ] W) (m : V →ₗ[ℝ] ℝ)
79     (P : I → V →ₗ[ℝ] V) (v : V) (i : PositiveIndex m P v) :
80     normalized (mass e m) (fun j => operator e (P j)) (e v) (index e m P v i) =
81       e (normalized m P v i) := by
82   simp [normalized, index, weight_eq]
83 
84 /-- Idempotence, when present, is preserved by conjugation. -/
85 theorem idempotent (e : V ≃ₗ[ℝ] W) (P : V →ₗ[ℝ] V) (h : P.comp P = P) :
86     (operator e P).comp (operator e P) = operator e P := by
87   apply LinearMap.ext
88   intro w
89   obtain ⟨v, rfl⟩ := e.surjective w
90   simp only [LinearMap.comp_apply, operator_apply]
91   exact congrArg e (LinearMap.congr_fun h v)
92 
93 variable [Fintype I]
94 
95 /-- Completeness is also transported as an identity of actual linear maps. -/
96 theorem complete (e : V ≃ₗ[ℝ] W) (P : I → V →ₗ[ℝ] V) (hc : Complete P) :
97     Complete (fun i => operator e (P i)) := by
98   apply LinearMap.ext
99   intro w
100   obtain ⟨v, rfl⟩ := e.surjective w
101   simpa only [LinearMap.sum_apply, LinearMap.id_apply, operator_apply, ← map_sum] using
102     congrArg e (sum_packets P hc v)
103 
104 /-- Source coordinate-change clause: the complete mixture hypotheses move together. -/
105 theorem source_coordinate_change (e : V ≃ₗ[ℝ] W) (C : ConvexCone ℝ V)
106     (m : V →ₗ[ℝ] ℝ) (hm : StrictMass C m) (P : I → V →ₗ[ℝ] V)
107     (hp : ∀ i, Preserves C (P i)) (hc : Complete P) {v : V} (hv : IsState C m v) :
108     StrictMass (cone e C) (mass e m) ∧
109     (∀ i, Preserves (cone e C) (operator e (P i))) ∧
110     Complete (fun i => operator e (P i)) ∧
111     IsState (cone e C) (mass e m) (e v) ∧
112     (∀ i, weight (mass e m) (fun j => operator e (P j)) (e v) i = weight m P v i) :=
113   ⟨strictMass e C m hm, fun i => preserves e C (P i) (hp i), complete e P hc,
114     (state_iff e C m v).mpr hv, weight_eq e m P v⟩
115 
116 end
117 end Komorebi.MachineTheory.PositivePackets.Transport

Back to source controls