LinearClosure.lean

1 import KomorebiLSM.PredictiveClosure
2 import Mathlib.Algebra.Module.Submodule.LinearMap
3 import Mathlib.Tactic.Abel
4 
5 /-! Algebraic P7, with actual linear maps. Orthogonality is not needed;
6 idempotence is required precisely where a retained projection is used.
7 -/
8 set_option autoImplicit false
9 namespace Komorebi.LSM
10 universe u v
11 variable {R : Type u} [Ring R]
12 variable {X : Type v} [AddCommGroup X] [Module R X]
13 
14 def unresolved (P : X →ₗ[R] X) : X →ₗ[R] X := LinearMap.id - P
15 
16 def closureDefect (P L : X →ₗ[R] X) : X →ₗ[R] X :=
17   P.comp (L.comp (unresolved P))
18 
19 theorem unresolved_apply (P : X →ₗ[R] X) (x : X) :
20     unresolved P x = x - P x := rfl
21 
22 theorem unresolved_idempotent (P : X →ₗ[R] X) (idem : ∀ x, P (P x) = P x)
23     (x : X) : unresolved P (unresolved P x) = unresolved P x := by
24   simp only [unresolved_apply, map_sub, idem, sub_self, sub_zero]
25 
26 theorem closure_defect_apply (P L : X →ₗ[R] X) (x : X) :
27     closureDefect P L x = P (L x) - P (L (P x)) := by
28   simp only [closureDefect, LinearMap.comp_apply, unresolved_apply, map_sub]
29 
30 theorem retained_dynamics_split (P L : X →ₗ[R] X) (x : X) :
31     P (L x) = P (L (P x)) + closureDefect P L x := by
32   rw [closure_defect_apply]
33   abel
34 
35 theorem closure_iff_zero_defect (P L : X →ₗ[R] X)
36     (idem : ∀ x, P (P x) = P x) :
37     FiberConstant P (fun x => P (L x)) ↔ closureDefect P L = 0 := by
38   constructor
39   · intro h
40     ext x
41     simp only [LinearMap.zero_apply, closure_defect_apply]
42     exact sub_eq_zero.mpr (h x (P x) (idem x).symm)
43   · intro h x y hxy
44     have hx := congrArg (fun f : X →ₗ[R] X => f x) h
45     have hy := congrArg (fun f : X →ₗ[R] X => f y) h
46     simp only [LinearMap.zero_apply, closure_defect_apply, sub_eq_zero] at hx hy
47     exact hx.trans ((congrArg (fun z => P (L z)) hxy).trans hy.symm)
48 
49 /-- The exact omitted return path PLQMP, with Q = I-P. -/
50 theorem composition_defect (P L M : X →ₗ[R] X)
51     (idem : ∀ x, P (P x) = P x) :
52     P.comp (L.comp (M.comp P)) -
53         (P.comp (L.comp P)).comp (P.comp (M.comp P)) =
54       P.comp (L.comp ((unresolved P).comp (M.comp P))) := by
55   ext x
56   simp only [LinearMap.sub_apply, LinearMap.comp_apply, unresolved_apply,
57     map_sub, idem]
58 
59 theorem zero_defect_exact_composition (P L M : X →ₗ[R] X)
60     (idem : ∀ x, P (P x) = P x) (closed : closureDefect P L = 0) :
61     P.comp (L.comp (M.comp P)) =
62       (P.comp (L.comp P)).comp (P.comp (M.comp P)) := by
63   apply sub_eq_zero.mp
64   rw [composition_defect P L M idem]
65   ext x
66   have h := congrArg (fun f : X →ₗ[R] X => f (M (P x))) closed
67   simpa only [closureDefect, LinearMap.comp_apply, LinearMap.zero_apply] using h
68 
69 end Komorebi.LSM

Back to source controls