TreeEnergy.lean

1 import KomorebiLSM.PacketTree
2 import Mathlib.Analysis.InnerProductSpace.Basic
3 import Mathlib.Algebra.Module.Submodule.LinearMap
4 
5 /-! P3: exact reconstruction and Pythagoras for arbitrary complete cuts
6 of a finite rooted tree. Only local sums and sibling orthogonality are
7 assumed. The complete-cut sum and energy identity are conclusions. -/
8 set_option autoImplicit false
9 open scoped BigOperators
10 namespace Komorebi.LSM
11 universe u v
12 variable {𝕜 : Type u} [RCLike 𝕜]
13 variable {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
14 
15 /-- Finite Pythagoras derived by expanding the inner product. -/
16 theorem orthogonal_sum_energy {I : Type*} [Fintype I]
17     (f : I → E) (h : ∀ i j, i ≠ j → inner 𝕜 (f i) (f j) = 0) :
18     ‖∑ i, f i‖ ^ 2 = ∑ i, ‖f i‖ ^ 2 := by
19   classical
20   have hs : inner 𝕜 (∑ i, f i) (∑ j, f j) = ∑ i, inner 𝕜 (f i) (f i) := by
21     simp only [sum_inner, inner_sum]
22     apply Finset.sum_congr rfl
23     intro i _
24     exact Finset.sum_eq_single i (fun j _ hji => h j i hji)
25       (fun hi => (hi (Finset.mem_univ i)).elim)
26   simp only [InnerProductSpace.norm_sq_eq_re_inner (𝕜 := 𝕜), hs, map_sum]
27 
28 namespace PacketTree
29 
30 /-- Sibling ranges are orthogonal at every internal node. -/
31 def SiblingOrthogonal : (t : PacketTree) → (Node t → E →ₗ[𝕜] E) → Prop
32   | .leaf, _ => True
33   | .branch _ child, P =>
34       (∀ i j, i ≠ j → ∀ x y,
35         inner 𝕜 (P (Sum.inr ⟨i, root (child i)⟩) x)
36           (P (Sum.inr ⟨j, root (child j)⟩) y) = 0) ∧
37       ∀ i, SiblingOrthogonal (child i) (fun v => P (Sum.inr ⟨i, v⟩))
38 
39 /-- Evaluating a conservative tree of linear maps preserves local sums. -/
40 theorem conservative_apply (t : PacketTree) (P : Node t → E →ₗ[𝕜] E)
41     (hc : Conservative t P) (x : E) : Conservative t (fun v => P v x) := by
42   induction t with
43   | leaf => trivial
44   | branch n child ih =>
45       refine ⟨?_, fun i => ih i _ (hc.2 i)⟩
46       simpa only [LinearMap.sum_apply] using congrArg (fun L : E →ₗ[𝕜] E => L x) hc.1
47 
48 /-- Pythagoras makes squared packet norms a conservative scalar label. -/
49 theorem conservative_energy (t : PacketTree) (P : Node t → E →ₗ[𝕜] E)
50     (hc : Conservative t P) (ho : SiblingOrthogonal t P) (x : E) :
51     Conservative t (fun v => ‖P v x‖ ^ 2) := by
52   induction t with
53   | leaf => trivial
54   | branch n child ih =>
55       refine ⟨?_, fun i => ih i _ (hc.2 i) (ho.2 i)⟩
56       have hp := (conservative_apply (.branch n child) P hc x).1
57       dsimp only at hp ⊢
58       rw [hp]
59       exact orthogonal_sum_energy _ (fun i j hij => ho.1 i j hij x x)
60 
61 /-- P3 operator reconstruction for a complete antichain. -/
62 theorem complete_cut_operator (t : PacketTree) (P : Node t → E →ₗ[𝕜] E)
63     (s : Node t → Bool) (cut : IsCompleteCut t s)
64     (hc : Conservative t P) (hroot : P (root t) = LinearMap.id) :
65     (∑ v, if s v then P v else 0) = LinearMap.id :=
66   (complete_cut_sum t s P cut hc).trans hroot
67 
68 /-- P3 signal reconstruction for a complete antichain. -/
69 theorem complete_cut_reconstruction (t : PacketTree) (P : Node t → E →ₗ[𝕜] E)
70     (s : Node t → Bool) (cut : IsCompleteCut t s)
71     (hc : Conservative t P) (hroot : P (root t) = LinearMap.id) (x : E) :
72     (∑ v, if s v then P v x else 0) = x := by
73   rw [complete_cut_sum t s _ cut (conservative_apply t P hc x), hroot]
74   rfl
75 
76 /-- P3 orthogonal energy identity, obtained from local sibling hypotheses. -/
77 theorem complete_cut_energy (t : PacketTree) (P : Node t → E →ₗ[𝕜] E)
78     (s : Node t → Bool) (cut : IsCompleteCut t s)
79     (hc : Conservative t P) (ho : SiblingOrthogonal t P)
80     (hroot : P (root t) = LinearMap.id) (x : E) :
81     (∑ v, if s v then ‖P v x‖ ^ 2 else 0) = ‖x‖ ^ 2 := by
82   rw [complete_cut_sum t s _ cut (conservative_energy t P hc ho x), hroot]
83   rfl
84 
85 /-- A direct projector formulation supplies sibling range orthogonality. -/
86 theorem range_orthogonal_of_projector_products
87     (P Q : E →ₗ[𝕜] E)
88     (hP : ∀ x y, inner 𝕜 (P x) y = inner 𝕜 x (P y))
89     (hPQ : P.comp Q = 0) (x y : E) : inner 𝕜 (P x) (Q y) = 0 := by
90   rw [hP]
91   have hz : P (Q y) = 0 := by
92     simpa only [LinearMap.comp_apply, LinearMap.zero_apply] using
93       congrArg (fun f : E →ₗ[𝕜] E => f y) hPQ
94   rw [hz, inner_zero_right]
95 
96 end PacketTree
97 end Komorebi.LSM

Back to source controls