InverseSupport.lean

1 module
2 public import TransferSupport
3 import all TransferSupport
4 import all PacketIR
5 import all QuantumPacketCore
6 public import Mathlib.LinearAlgebra.FiniteDimensional.Basic
7 public import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
8 public import Mathlib.Tactic
9 
10 /-!
11 Author: Komorebi P. Paper VIII item 6.7.
12 The inverse preserves the actual reachable packet subspace because its forward
13 restriction is injective and finite dimensional, hence surjective. Includes
14 zero-length paths. The result uses invertibility, not an assumed inverse sparsity.
15 -/
16 public section
17 set_option autoImplicit false
18 namespace KomorebiPaperVIII
19 open scoped BigOperators Classical
20 open KomorebiPaperVII
21 variable {K R I : Type*} [Field K] [Ring R] [Algebra K R]
22 variable [Fintype I] [DecidableEq I]
23 variable (P : PacketFamily R I)
24 
25 def Reachable (A : R) (b a : I) : Prop := ∃ n, TransferPath P A n b a
26 
27 theorem reachable_refl (A : R) (a : I) : Reachable P A a a := ⟨0,rfl⟩
28 
29 theorem reachable_step (A : R) {b c a : I}
30     (he : P.block A b c ≠ 0) (h : Reachable P A c a) : Reachable P A b a := by
31   obtain ⟨n,hn⟩ := h
32   exact ⟨n+1,c,he,hn⟩
33 
34 /-- The subspace consisting of vectors with no unreachable packet component. -/
35 def reachableSpace (A : R) (a : I) : Submodule K R where
36   carrier := {x | ∀ b, ¬ Reachable P A b a → P.proj b * x = 0}
37   zero_mem' := by simp
38   add_mem' := by
39     intro x y hx hy b hb
40     rw [mul_add,hx b hb,hy b hb,add_zero]
41   smul_mem' := by
42     intro c x hx b hb
43     rw [mul_smul_comm,hx b hb,smul_zero]
44 
45 theorem seed_mem_reachableSpace (A : R) (a : I) :
46     P.proj a ∈ reachableSpace (K := K) P A a := by
47   intro b hb
48   have hba : b ≠ a := by
49     intro he; subst b
50     exact hb (reachable_refl P A a)
51   rw [P.mul_proj]
52   simp only [hba,ite_false]
53 
54 theorem reachableSpace_invariant (A : R) (a : I) (x : R)
55     (hx : x ∈ reachableSpace (K := K) P A a) :
56     A*x ∈ reachableSpace (K := K) P A a := by
57   intro b hb
58   have he : P.proj b * (A*x) = ∑ c, P.block A b c * x := by
59     simp only [PacketFamily.block,← Finset.sum_mul,← Finset.mul_sum]
60     rw [P.sum_proj,mul_one,mul_assoc]
61   rw [he]
62   apply Finset.sum_eq_zero
63   intro c _
64   by_cases hc : P.block A b c = 0
65   · rw [hc,zero_mul]
66   · have hn : ¬ Reachable P A c a := fun hp => hb (reachable_step P A hc hp)
67     change (P.proj b*A*P.proj c)*x = 0
68     rw [mul_assoc, hx c hn,mul_zero]
69 
70 variable [FiniteDimensional K R]
71 
72 /-- Finite-dimensional injectivity makes the restriction onto its invariant range. -/
73 theorem invariant_space_inverse (A B : R) (hBA : B*A = 1) (W : Submodule K R)
74     (hW : ∀ x ∈ W, A*x ∈ W) (x : R) (hx : x ∈ W) : B*x ∈ W := by
75   let f : W →ₗ[K] W :=
76     { toFun := fun y => ⟨A*y.val,hW y.val y.property⟩
77       map_add' := by intro y z; apply Subtype.ext; exact mul_add A y.val z.val
78       map_smul' := by intro c y; apply Subtype.ext; exact mul_smul_comm c A y.val }
79   have hinj : Function.Injective f := by
80     intro y z he
81     have he' : A*y.val = A*z.val := congrArg Subtype.val he
82     apply Subtype.ext
83     have hh := congrArg (fun t => B*t) he'
84     simpa only [← mul_assoc,hBA,one_mul] using hh
85   obtain ⟨y,hy⟩ := LinearMap.surjective_of_injective hinj ⟨x,hx⟩
86   have hy' : A*y.val = x := congrArg Subtype.val hy
87   have hbx : B*x = y.val := by rw [←hy',←mul_assoc,hBA,one_mul]
88   rw [hbx]
89   exact y.property
90 
91 include K
92 
93 /-- No reachable path from a to b forces a zero block of the actual inverse. -/
94 theorem inverse_block_zero_of_no_path (A B : R) (hBA : B*A = 1) (b a : I)
95     (h : ¬ Reachable P A b a) : P.block B b a = 0 := by
96   have hm := invariant_space_inverse (K := K) A B hBA
97     (reachableSpace (K := K) P A a) (reachableSpace_invariant P A a)
98     (P.proj a) (seed_mem_reachableSpace P A a)
99   have hz := hm b h
100   simpa only [PacketFamily.block,mul_assoc] using hz
101 
102 theorem inverse_support_inclusion (A B : R) (hBA : B*A = 1) (b a : I)
103     (h : P.block B b a ≠ 0) : Reachable P A b a := by
104   by_contra hn
105   exact h (inverse_block_zero_of_no_path (K := K) P A B hBA b a hn)
106 
107 /-- Unit notation specializes the theorem to a genuine algebraic inverse. -/
108 theorem unit_inverse_support (A : Rˣ) (b a : I)
109     (h : P.block (↑(A⁻¹) : R) b a ≠ 0) : Reachable P (↑A : R) b a := by
110   exact inverse_support_inclusion (K := K) P A ↑(A⁻¹) (by simp) b a h
111 
112 section Matrix
113 variable {X : Type*} [Fintype X] [DecidableEq X]
114 
115 /-- Matrix specialization uses Mathlib's actual nonsingular matrix inverse. -/
116 theorem matrix_inverse_support (Q : PacketFamily (Matrix X X K) I)
117     (A : Matrix X X K) (hA : IsUnit A.det) (b a : I)
118     (h : Q.block A⁻¹ b a ≠ 0) : Reachable Q A b a := by
119   exact inverse_support_inclusion (K := K) Q A A⁻¹
120     (Matrix.nonsing_inv_mul A hA) b a h
121 end Matrix
122 end KomorebiPaperVIII
123 
124 -- FIFTH BLOCK AXIOM AUDIT
125 #print axioms KomorebiPaperVIII.reachable_refl
126 #print axioms KomorebiPaperVIII.reachable_step
127 #print axioms KomorebiPaperVIII.seed_mem_reachableSpace
128 #print axioms KomorebiPaperVIII.reachableSpace_invariant
129 #print axioms KomorebiPaperVIII.invariant_space_inverse
130 #print axioms KomorebiPaperVIII.inverse_block_zero_of_no_path
131 #print axioms KomorebiPaperVIII.inverse_support_inclusion
132 #print axioms KomorebiPaperVIII.unit_inverse_support
133 #print axioms KomorebiPaperVIII.matrix_inverse_support
134 #print axioms KomorebiPaperVIII.reachableSpace

Back to source controls