ReleaseCoordinatesHilbert.lean

1 import KomorebiVerification.PaperII.NestedRefinement
2 import Mathlib.Analysis.InnerProductSpace.PiL2
3 import Mathlib.Analysis.InnerProductSpace.Symmetric
4 
5 /-!
6 Finite Hilbert packet coordinates use the L2 norm, not the default supremum
7 norm on a function product. Orthogonality is the usual self-adjointness of
8 each idempotent. The maps below retain the independent range and sum maps.
9 -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace Komorebi.PaperII.HilbertCoordinates
13 open Komorebi.Foundation Komorebi.Foundation.LinearProjectorFamily
14 universe u v w x
15 variable {𝕜 : Type u} [RCLike 𝕜]
16 variable {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
17 variable {ι : Type w} {κ : Type x} [Fintype ι] [Fintype κ]
18 
19 /-- The actual finite Hilbert direct sum of projector ranges. -/
20 abbrev HilbertPacketSpace (P : LinearProjectorFamily 𝕜 E ι) :=
21   PiLp 2 (fun i => LinearMap.range (P.proj i))
22 
23 /-- The algebraic packet equivalence, with its codomain carrying the L2 norm. -/
24 def hilbertPacketEquiv (P : LinearProjectorFamily 𝕜 E ι) :
25     E ≃ₗ[𝕜] HilbertPacketSpace P :=
26   P.exactPacketCoordinates.trans (WithLp.linearEquiv 2 𝕜 (PacketSpace P)).symm
27 
28 @[simp] theorem hilbertPacketEquiv_apply (P : LinearProjectorFamily 𝕜 E ι)
29     (x : E) (i : ι) :
30     ((hilbertPacketEquiv P x i : LinearMap.range (P.proj i)) : E) = P.proj i x := rfl
31 
32 @[simp] theorem hilbertPacketEquiv_symm_apply (P : LinearProjectorFamily 𝕜 E ι)
33     (x : HilbertPacketSpace P) :
34     (hilbertPacketEquiv P).symm x = ∑ i, (x i : E) := rfl
35 
36 /-- Self-adjoint idempotents preserve the full inner product under analysis. -/
37 theorem hilbertPacketEquiv_inner (P : LinearProjectorFamily 𝕜 E ι)
38     (hP : ∀ i, (P.proj i).IsSymmetric) (x y : E) :
39     inner 𝕜 (hilbertPacketEquiv P x) (hilbertPacketEquiv P y) = inner 𝕜 x y := by
40   change (∑ i, inner 𝕜 (P.proj i x) (P.proj i y)) = inner 𝕜 x y
41   calc
42     (∑ i, inner 𝕜 (P.proj i x) (P.proj i y)) =
43         ∑ i, inner 𝕜 x (P.proj i y) := by
44       apply Finset.sum_congr rfl
45       intro i _
46       rw [hP i, P.idempotent]
47     _ = inner 𝕜 x (∑ i, P.proj i y) := (inner_sum _ _ _).symm
48     _ = inner 𝕜 x y := by rw [P.complete]
49 
50 /-- Analysis and synthesis are inverse linear isometries for the Hilbert sum. -/
51 def hilbertPacketUnitary (P : LinearProjectorFamily 𝕜 E ι)
52     (hP : ∀ i, (P.proj i).IsSymmetric) : E ≃ₗᵢ[𝕜] HilbertPacketSpace P :=
53   (hilbertPacketEquiv P).isometryOfInner (hilbertPacketEquiv_inner P hP)
54 
55 /-- Parseval's identity in the exact manuscript normalization. -/
56 theorem packet_parseval (P : LinearProjectorFamily 𝕜 E ι)
57     (hP : ∀ i, (P.proj i).IsSymmetric) (x : E) :
58     ‖x‖ ^ 2 = ∑ i, ‖P.proj i x‖ ^ 2 := by
59   have h := (hilbertPacketUnitary P hP).norm_map x
60   rw [← h]
61   exact PiLp.norm_sq_eq_of_L2 _ _
62 
63 /-- Coordinate change is a genuine unitary between the two finite Hilbert sums. -/
64 def hilbertCoordinateChange (P : LinearProjectorFamily 𝕜 E ι)
65     (Q : LinearProjectorFamily 𝕜 E κ)
66     (hP : ∀ i, (P.proj i).IsSymmetric) (hQ : ∀ j, (Q.proj j).IsSymmetric) :
67     HilbertPacketSpace P ≃ₗᵢ[𝕜] HilbertPacketSpace Q :=
68   (hilbertPacketUnitary P hP).symm.trans (hilbertPacketUnitary Q hQ)
69 
70 /-- This unitary has the same synthesis-then-analysis formula as the algebraic map. -/
71 theorem hilbertCoordinateChange_apply (P : LinearProjectorFamily 𝕜 E ι)
72     (Q : LinearProjectorFamily 𝕜 E κ)
73     (hP : ∀ i, (P.proj i).IsSymmetric) (hQ : ∀ j, (Q.proj j).IsSymmetric)
74     (x : HilbertPacketSpace P) (j : κ) :
75     ((hilbertCoordinateChange P Q hP hQ x j : LinearMap.range (Q.proj j)) : E) =
76       Q.proj j (∑ i, (x i : E)) := rfl
77 
78 end Komorebi.PaperII.HilbertCoordinates
79 #print axioms Komorebi.PaperII.HilbertCoordinates.hilbertPacketUnitary
80 #print axioms Komorebi.PaperII.HilbertCoordinates.hilbertCoordinateChange

Back to source controls