ReconciliationHilbert.lean

1 import KomorebiLSM.AtlasReconciliation
2 import KomorebiLSM.PacketApproximation
3 import KomorebiLSM.StrongRefinement
4 import Mathlib.Analysis.InnerProductSpace.PiL2
5 import Mathlib.LinearAlgebra.Matrix.ToLin
6 
7 /-! Actual Hilbert-space adapters for P20 and P21. The matrix coordinates are
8 constructed from an orthonormal basis, not a supplied minimization witness. -/
9 set_option autoImplicit false
10 open scoped BigOperators
11 namespace Komorebi.LSM.Reconciliation
12 universe u v
13 variable {X : Type u} [NormedAddCommGroup X] [InnerProductSpace ℝ X]
14 variable [FiniteDimensional ℝ X]
15 
16 noncomputable def orthonormalOperatorCoordinates :
17     (X →ₗ[ℝ] X) ≃ₗ[ℝ] Matrix (Fin (Module.finrank ℝ X)) (Fin (Module.finrank ℝ X)) ℝ :=
18   (LinearMap.toMatrixAlgEquiv (stdOrthonormalBasis ℝ X).toBasis).toLinearEquiv
19 
20 /-- The Frobenius objective uses actual orthonormal matrix coordinates. -/
21 theorem hilbert_operator_unique_minimizer {I : Type*} [Fintype I]
22     (L : I → X →ₗ[ℝ] X) (w : I → ℝ) (total : ∑ i, w i=1) :
23     ∃! M : X →ₗ[ℝ] X, ∀ N,
24       frobeniusCost w (fun i => orthonormalOperatorCoordinates (L i))
25         (orthonormalOperatorCoordinates M) ≤
26       frobeniusCost w (fun i => orthonormalOperatorCoordinates (L i))
27         (orthonormalOperatorCoordinates N) :=
28   operator_unique_frobenius_minimizer orthonormalOperatorCoordinates L w total
29 
30 /-- The independently fitted atlases are pulled back before the mean is taken.
31 The norm here is the actual continuous-operator norm on the common object space. -/
32 theorem reconciled_target_error {I : Type*} [Fintype I] {C : I → Type v}
33     [∀ i, AddCommGroup (C i)] [∀ i, Module ℝ (C i)]
34     (atlas : (i : I) → LinearAtlas X (C i))
35     (G : (i : I) → C i →ₗ[ℝ] C i) (w : I → ℝ)
36     (positive : ∀ i, 0 ≤ w i) (total : ∑ i, w i=1) (target : X →L[ℝ] X) :
37     ‖(reconciledOperator atlas G w).toContinuousLinearMap-target‖ ≤
38       ∑ i, w i*‖((atlas i).objectFit (G i)).toContinuousLinearMap-target‖ := by
39   have hm : (reconciledOperator atlas G w).toContinuousLinearMap =
40       weightedMean w (fun i => ((atlas i).objectFit (G i)).toContinuousLinearMap) := by
41     simp only [reconciledOperator,weightedMean,map_sum,map_smul]
42   rw [hm]
43   exact weighted_target_error w _ positive total target
44 
45 end Komorebi.LSM.Reconciliation
46 
47 namespace Komorebi.LSM.PacketApproximation
48 variable {X Y : Type*} [NormedAddCommGroup X] [InnerProductSpace ℝ X]
49 variable [NormedAddCommGroup Y] [NormedSpace ℝ Y]
50 variable {I : Type*}
51 
52 /-- Orthogonal subspace projectors discharge the contractivity hypothesis in the
53 multilinear Lipschitz estimate. No extra projection-norm hypothesis is supplied. -/
54 theorem orthogonal_packet_lipschitz_bound
55     (S : I → Submodule ℝ X) [∀ i, (S i).HasOrthogonalProjection]
56     (p : ℕ)
57     (B : (m : Fin p) → ContinuousMultilinearMap ℝ (fun _ : Fin (m.val+1) => X) Y)
58     (keep : (m : Fin p) → Finset (Fin (m.val+1) → I))
59     (beta : (m : Fin p) → (Fin (m.val+1) → I) → ℝ)
60     (hbeta : ∀ m f, 0 ≤ beta m f)
61     (bound : ∀ m f, HasPacketBound (fun i => (S i).starProjection) (B m) f (beta m f))
62     (b : Y) {R : ℝ} (hR : 0 ≤ R) (x y : X) (hx : ‖x‖ ≤ R) (hy : ‖y‖ ≤ R) :
63     ‖retainedPolynomial p (fun i => (S i).starProjection) B keep b x-
64       retainedPolynomial p (fun i => (S i).starProjection) B keep b y‖ ≤
65       (∑ m, ∑ f ∈ keep m, (m.val+1:ℕ)*beta m f*R^m.val)*‖x-y‖ := by
66   apply retained_polynomial_lipschitz_bound p _ _ B keep beta hbeta bound b hR x y hx hy
67   intro i
68   exact (S i).starProjection_norm_le
69 
70 end Komorebi.LSM.PacketApproximation

Back to source controls