TriangularSolve.lean

1 module
2 public import GraphSchedules
3 import all GraphSchedules
4 public import Mathlib.LinearAlgebra.Pi
5 public import Mathlib.Tactic
6 
7 /-!
8 Author: Komorebi P. Paper VIII item 6.5.
9 Constructs the actual forward-substitution solution in dependent block spaces.
10 Diagonal invertibility is represented by local linear equivalences. Transfers
11 are arbitrary linear maps on graph edges. No solution or solve equation is assumed.
12 -/
13 public section
14 set_option autoImplicit false
15 namespace KomorebiPaperVIII
16 namespace DAG.Graph
17 open scoped BigOperators Classical
18 variable {V K : Type*} [Fintype V] [Field K]
19 variable (G : DAG.Graph V) (X : V → Type*)
20 variable [∀ v, AddCommGroup (X v)] [∀ v, Module K (X v)]
21 variable (D : ∀ v, X v ≃ₗ[K] X v) (T : ∀ b a, X a →ₗ[K] X b)
22 
23 /-- Block diagonal plus the actual graph-edge transfers. -/
24 noncomputable def triangularAction (x : ∀ v, X v) (v : V) : X v :=
25   D v (x v) + ∑ u : {u // G.edge u v}, T v u.val (x u.val)
26 
27 /-- Well-founded forward substitution on the constructed acyclic graph. -/
28 noncomputable def solve (rhs : ∀ v, X v) : ∀ v, X v :=
29   G.wellFounded.fix (fun v rec =>
30     (D v).symm (rhs v - ∑ u : {u // G.edge u v}, T v u.val (rec u.val u.property)))
31 
32 theorem solve_eq (rhs : ∀ v, X v) (v : V) :
33     G.solve X D T rhs v = (D v).symm
34       (rhs v - ∑ u : {u // G.edge u v}, T v u.val (G.solve X D T rhs u.val)) :=
35   WellFounded.fix_eq G.wellFounded _ v
36 
37 /-- The computed vector solves the actual block equations. -/
38 theorem solve_correct (rhs : ∀ v, X v) :
39     G.triangularAction X D T (G.solve X D T rhs) = rhs := by
40   funext v
41   unfold triangularAction
42   rw [G.solve_eq X D T rhs v, LinearEquiv.apply_symm_apply]
43   exact sub_add_cancel _ _
44 
45 /-- A competitor satisfying the equations must equal the constructed solution. -/
46 theorem solve_unique (rhs x : ∀ v, X v)
47     (hx : G.triangularAction X D T x = rhs) : x = G.solve X D T rhs := by
48   funext v
49   induction v using G.wellFounded.induction with
50   | h v ih =>
51     have hv := congrFun hx v
52     change D v (x v) + ∑ u : {u // G.edge u v}, T v u.val (x u.val) = rhs v at hv
53     have hsum : (∑ u : {u // G.edge u v}, T v u.val (x u.val)) =
54         ∑ u : {u // G.edge u v}, T v u.val (G.solve X D T rhs u.val) := by
55       apply Finset.sum_congr rfl
56       intro u _
57       rw [ih u.val u.property]
58     rw [hsum] at hv
59     rw [G.solve_eq X D T rhs v]
60     apply (D v).injective
61     rw [LinearEquiv.apply_symm_apply]
62     exact eq_sub_iff_add_eq.mpr hv
63 
64 /-- In particular, the block triangular operator is bijective. -/
65 theorem triangular_bijective : Function.Bijective (G.triangularAction X D T) := by
66   constructor
67   · intro x y h
68     have hx := G.solve_unique X D T (G.triangularAction X D T y) x h
69     have hy := G.solve_unique X D T (G.triangularAction X D T y) y rfl
70     exact hx.trans hy.symm
71   · intro rhs
72     exact ⟨G.solve X D T rhs, G.solve_correct X D T rhs⟩
73 
74 /-- A single stage only reads strict predecessors. -/
75 theorem local_solve_independent (rhs : ∀ v, X v) (v : V) (x y : ∀ v, X v)
76     (h : ∀ u, G.level u < G.level v → x u = y u) :
77     (D v).symm (rhs v - ∑ u : {u // G.edge u v}, T v u.val (x u.val)) =
78       (D v).symm (rhs v - ∑ u : {u // G.edge u v}, T v u.val (y u.val)) := by
79   congr 2
80   apply Finset.sum_congr rfl
81   intro u _
82   rw [h u.val (G.edge_level u.property)]
83 
84 /-- Stage evaluator: update all tasks whose canonical level is the next stage. -/
85 noncomputable def stagedSolve (rhs : ∀ v, X v) : ℕ → ∀ v, X v
86   | 0 => fun _ => 0
87   | k+1 => fun v => if G.level v = k+1 then
88       (D v).symm (rhs v - ∑ u : {u // G.edge u v}, T v u.val (stagedSolve rhs k u.val))
89       else stagedSolve rhs k v
90 
91 theorem stagedSolve_correct_through (rhs : ∀ v, X v) (k : ℕ) :
92     ∀ v, G.level v ≤ k → G.stagedSolve X D T rhs k v = G.solve X D T rhs v := by
93   induction k with
94   | zero =>
95     intro v hv
96     have := G.level_positive v
97     omega
98   | succ k ih =>
99     intro v hv
100     by_cases he : G.level v = k+1
101     · simp only [stagedSolve,he,ite_true]
102       rw [G.solve_eq X D T rhs v]
103       congr 2
104       apply Finset.sum_congr rfl
105       intro u _
106       have hu := G.edge_level u.property
107       rw [ih u.val (by omega)]
108     · simp only [stagedSolve,he,ite_false]
109       exact ih v (by omega)
110 
111 /-- The concrete parallel-stage evaluator finishes at the optimal DAG depth. -/
112 theorem level_schedule_solves (rhs : ∀ v, X v) :
113     G.triangularAction X D T (G.stagedSolve X D T rhs G.depth) = rhs := by
114   have he : G.stagedSolve X D T rhs G.depth = G.solve X D T rhs := by
115     funext v
116     exact G.stagedSolve_correct_through X D T rhs G.depth v (G.level_le_depth v)
117   rw [he]
118   exact G.solve_correct X D T rhs
119 
120 end DAG.Graph
121 end KomorebiPaperVIII
122 
123 -- FIFTH BLOCK AXIOM AUDIT
124 #print axioms KomorebiPaperVIII.DAG.Graph.solve_eq
125 #print axioms KomorebiPaperVIII.DAG.Graph.solve_correct
126 #print axioms KomorebiPaperVIII.DAG.Graph.solve_unique
127 #print axioms KomorebiPaperVIII.DAG.Graph.triangular_bijective
128 #print axioms KomorebiPaperVIII.DAG.Graph.local_solve_independent
129 #print axioms KomorebiPaperVIII.DAG.Graph.stagedSolve_correct_through
130 #print axioms KomorebiPaperVIII.DAG.Graph.level_schedule_solves
131 #print axioms KomorebiPaperVIII.DAG.Graph.triangularAction
132 #print axioms KomorebiPaperVIII.DAG.Graph.solve
133 #print axioms KomorebiPaperVIII.DAG.Graph.stagedSolve

Back to source controls