Formal forward and reverse rows of a unary mixer test
Lax342547.UnaryMixer · concepts/Lax342547/UnaryMixer.lean · lax-342547
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Lemma
For a fixed rank profile, each forward and reverse product receives its own pair of formal row vectors. The substitution map records the actual mixer restrictions. Its restriction to the Z direction matrix is chosen before any non-Z coordinates or flavor are fixed.
Concept map
Evidence
This concept declares 10 statements. Each proof establishes one of them relative to its assumptions.
1 formal_rank proven
2 incident_card proven
3 mixer_atom_expansion proven
4 row_space_dimension proven
5 substitution_rank proven
6 unary_affine_quadratic proven
7 unary_depends_on_rows proven
8 unary_polar proven
9 unary_rank_bound proven
10 unary_rank_lower proven
Lean source view on GitHub
| 1 | import Lax342547.FormalQuadratic |
| 2 | import Lax342547.RestrictionRank |
| 3 | import Lax342547.AtomDirections |
| 4 | import Lax342547.Atoms |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Formal forward and reverse rows of a unary mixer test |
| 9 | type: lemma |
| 10 | --- |
| 11 | For a fixed rank profile, each forward and reverse product receives |
| 12 | its own pair of formal row vectors. The substitution map records the |
| 13 | actual mixer restrictions. Its restriction to the Z direction matrix |
| 14 | is chosen before any non-Z coordinates or flavor are fixed. |
| 15 | -/ |
| 16 | |
| 17 | namespace Lax342547.UnaryMixer |
| 18 | |
| 19 | open Lax342547.MomentSpace |
| 20 | |
| 21 | variable {E I : Type} [Fintype E] [Fintype I] |
| 22 | |
| 23 | abbrev Block (inc : Finset E) (J : ℕ) := |
| 24 | (Fin J × E × {f : E // f ∈ inc}) ⊕ (Fin J × {e : E // e ∈ inc} × E) |
| 25 | |
| 26 | def blockRank (r : E → ℕ) {inc : Finset E} {J : ℕ} : Block inc J → ℕ |
| 27 | | .inl (_, e, _) => r e |
| 28 | | .inr (_, _, f) => r f |
| 29 | |
| 30 | abbrev Rows (r : E → ℕ) (inc : Finset E) (J : ℕ) := |
| 31 | FormalQuadratic.Rows (fun t : Block inc J => Fin (blockRank r t) → Binary) |
| 32 | |
| 33 | noncomputable def middle {r : E → ℕ} {inc : Finset E} {J : ℕ} |
| 34 | (H : ∀ e, Matrix (Fin (r e)) (Fin (r e)) Binary) : |
| 35 | ∀ t : Block inc J, LinearMap.BilinForm Binary (Fin (blockRank r t) → Binary) |
| 36 | | .inl (_, e, _) => (H e).toBilin' |
| 37 | | .inr (_, _, f) => (H f).toBilin' |
| 38 | |
| 39 | noncomputable def rowMap {r : E → ℕ} (inc : Finset E) {J : ℕ} |
| 40 | (Z : ∀ e, Matrix I (Fin (r e)) Binary) |
| 41 | (L R : Fin J → E → E → Matrix I I Binary) : (I → Binary) →ₗ[Binary] Rows r inc J := |
| 42 | LinearMap.pi fun t => match t with |
| 43 | | .inl (j, e, f) => |
| 44 | ((Z e).transpose * L j e f.val).mulVecLin.prod |
| 45 | ((Z e).transpose * R j e f.val).mulVecLin |
| 46 | | .inr (j, e, f) => |
| 47 | ((L j e.val f * Z f).transpose).mulVecLin.prod |
| 48 | ((R j e.val f * Z f).transpose).mulVecLin |
| 49 | |
| 50 | noncomputable def formalQuadratic {r : E → ℕ} (inc : Finset E) (J : ℕ) |
| 51 | (H : ∀ e, Matrix (Fin (r e)) (Fin (r e)) Binary) : QuadraticForm Binary (Rows r inc J) := |
| 52 | FormalQuadratic.quadratic (middle H) |
| 53 | |
| 54 | axiom formal_rank {r : E → ℕ} (inc : Finset E) (J : ℕ) |
| 55 | (H : ∀ e, Matrix (Fin (r e)) (Fin (r e)) Binary) |
| 56 | (hH : ∀ e, Function.Injective (H e).mulVec) : |
| 57 | Module.finrank Binary (LinearMap.range (formalQuadratic inc J H).polarBilin) = |
| 58 | 4 * J * inc.card * ∑ e, r e |
| 59 | |
| 60 | axiom substitution_rank {r : E → ℕ} (inc : Finset E) (J : ℕ) |
| 61 | (H : ∀ e, Matrix (Fin (r e)) (Fin (r e)) Binary) |
| 62 | (hH : ∀ e, Function.Injective (H e).mulVec) |
| 63 | {U : Type} [AddCommGroup U] [Module Binary U] |
| 64 | (A : U →ₗ[Binary] Rows r inc J) (s : ℕ) |
| 65 | (hA : Module.finrank Binary (Rows r inc J) ≤ |
| 66 | Module.finrank Binary (LinearMap.range A) + s) : |
| 67 | 4 * J * inc.card * ∑ e, r e ≤ |
| 68 | Module.finrank Binary (LinearMap.range (LinearMap.compl₁₂ |
| 69 | (formalQuadratic inc J H).polarBilin A A)) + 2 * s |
| 70 | |
| 71 | open Lax342547.TagGeometry Lax342547.ConcreteGeometry Lax342547.ConcreteCut |
| 72 | open Lax342547.CutProfiles Lax342547.Atoms |
| 73 | |
| 74 | noncomputable def incident {k : ℕ} (l : Tag k) : Finset (Component (Tag k)) := by |
| 75 | classical |
| 76 | exact Finset.univ.filter (fun e => l ∈ e.val) |
| 77 | |
| 78 | axiom incident_card {k : ℕ} (l : Tag k) : (incident l).card = 2 * k |
| 79 | |
| 80 | noncomputable def zRows {k n b degree J : ℕ} {r : Component (Tag k) → ℕ} |
| 81 | (Z : ∀ e, Matrix (Coordinate k n b degree) (Fin (r e)) Binary) |
| 82 | (L R : Fin J → Component (Tag k) → Component (Tag k) → Moment k n b degree) |
| 83 | (l : Tag k) (s : Fin b → Binary) : (Fin n → Binary) →ₗ[Binary] Rows r (incident l) J := |
| 84 | (rowMap (incident l) Z L R).comp (AtomDirections.blockDirections s free).mulVecLin |
| 85 | |
| 86 | noncomputable def zRowSpace {k n b degree J : ℕ} {r : Component (Tag k) → ℕ} |
| 87 | (Z : ∀ e, Matrix (Coordinate k n b degree) (Fin (r e)) Binary) |
| 88 | (L R : Fin J → Component (Tag k) → Component (Tag k) → Moment k n b degree) |
| 89 | (l : Tag k) (s : Fin b → Binary) : Submodule Binary (Module.Dual Binary (Fin n → Binary)) := |
| 90 | LinearMap.range (zRows Z L R l s).dualMap |
| 91 | |
| 92 | axiom row_space_dimension {k n b degree J K : ℕ} {r : Component (Tag k) → ℕ} |
| 93 | (Z : ∀ e, Matrix (Coordinate k n b degree) (Fin (r e)) Binary) |
| 94 | (L R : Fin J → Component (Tag k) → Component (Tag k) → Moment k n b degree) |
| 95 | (l : Tag k) (s : Fin b → Binary) (hrank : ∑ e, r e ≤ K) : |
| 96 | Module.finrank Binary (zRowSpace Z L R l s) ≤ 4 * J * (2 * k) * K |
| 97 | |
| 98 | def testerTerm {k n b degree r : ℕ} {hr : 2 * r ≤ n} |
| 99 | (D : Testers (k := k) (b := b) (degree := degree) hr) : |
| 100 | LinearMap.BilinForm Binary (Profile k n b degree) := |
| 101 | GradientForm.form D.role D.aTag D.bTag 0 |
| 102 | |
| 103 | noncomputable def atomAlongZ {k n b degree : ℕ} |
| 104 | (l : Tag k) (s : Fin b → Binary) (z : Base k n → Binary) |
| 105 | (hz : ∀ i, i ∉ allowedBase k n l → z i = 0) |
| 106 | (v : Fin n → Binary) : Profile k n b degree := |
| 107 | atom l s (AtomDirections.varyBlock z free v) (by |
| 108 | classical |
| 109 | intro i hi |
| 110 | cases i with |
| 111 | | inl i => simpa [AtomDirections.varyBlock, free] using hz (.inl i) hi |
| 112 | | inr i => exact False.elim (hi trivial)) |
| 113 | |
| 114 | axiom unary_affine_quadratic {k n b degree r₀ J : ℕ} {hr : 2 * r₀ ≤ n} |
| 115 | (D : Testers (k := k) (b := b) (degree := degree) hr) |
| 116 | (x : Profile k n b degree) {r : Component (Tag k) → ℕ} |
| 117 | (Z : ∀ e, Matrix (Coordinate k n b degree) (Fin (r e)) Binary) |
| 118 | (H : ∀ e, Matrix (Fin (r e)) (Fin (r e)) Binary) |
| 119 | (hfactor : ∀ e, Z e * H e * (Z e).transpose = x.val e) |
| 120 | (L R : Fin J → Component (Tag k) → Component (Tag k) → Moment k n b degree) |
| 121 | (l : Tag k) (s : Fin b → Binary) (z : Base k n → Binary) |
| 122 | (hz : ∀ i, i ∉ allowedBase k n l → z i = 0) (v : Fin n → Binary) : |
| 123 | gradient D L R x (atomAlongZ l s z hz v) = |
| 124 | testerTerm D x (atom l s z hz) + formalQuadratic (incident l) J H |
| 125 | (rowMap (incident l) Z L R (point selectorEval s z) + zRows Z L R l s v) |
| 126 | |
| 127 | axiom unary_polar {k n b degree r₀ J : ℕ} {hr : 2 * r₀ ≤ n} |
| 128 | (D : Testers (k := k) (b := b) (degree := degree) hr) |
| 129 | (x : Profile k n b degree) {r : Component (Tag k) → ℕ} |
| 130 | (Z : ∀ e, Matrix (Coordinate k n b degree) (Fin (r e)) Binary) |
| 131 | (H : ∀ e, Matrix (Fin (r e)) (Fin (r e)) Binary) |
| 132 | (hfactor : ∀ e, Z e * H e * (Z e).transpose = x.val e) |
| 133 | (L R : Fin J → Component (Tag k) → Component (Tag k) → Moment k n b degree) |
| 134 | (l : Tag k) (s : Fin b → Binary) (z : Base k n → Binary) |
| 135 | (hz : ∀ i, i ∉ allowedBase k n l → z i = 0) (u v : Fin n → Binary) : |
| 136 | FormalQuadratic.affinePolar (fun w => gradient D L R x (atomAlongZ l s z hz w)) u v = |
| 137 | (formalQuadratic (incident l) J H).polarBilin (zRows Z L R l s u) (zRows Z L R l s v) |
| 138 | |
| 139 | axiom unary_depends_on_rows {k n b degree r₀ J : ℕ} {hr : 2 * r₀ ≤ n} |
| 140 | (D : Testers (k := k) (b := b) (degree := degree) hr) |
| 141 | (x : Profile k n b degree) {r : Component (Tag k) → ℕ} |
| 142 | (Z : ∀ e, Matrix (Coordinate k n b degree) (Fin (r e)) Binary) |
| 143 | (H : ∀ e, Matrix (Fin (r e)) (Fin (r e)) Binary) |
| 144 | (hfactor : ∀ e, Z e * H e * (Z e).transpose = x.val e) |
| 145 | (L R : Fin J → Component (Tag k) → Component (Tag k) → Moment k n b degree) |
| 146 | (l : Tag k) (s : Fin b → Binary) (z : Base k n → Binary) |
| 147 | (hz : ∀ i, i ∉ allowedBase k n l → z i = 0) (u v : Fin n → Binary) |
| 148 | (hrows : ∀ a ∈ zRowSpace Z L R l s, a u = a v) : |
| 149 | gradient D L R x (atomAlongZ l s z hz u) = gradient D L R x (atomAlongZ l s z hz v) |
| 150 | |
| 151 | axiom mixer_atom_expansion {k n b degree J : ℕ} |
| 152 | (x : Profile k n b degree) {r : Component (Tag k) → ℕ} |
| 153 | (Z : ∀ e, Matrix (Coordinate k n b degree) (Fin (r e)) Binary) |
| 154 | (H : ∀ e, Matrix (Fin (r e)) (Fin (r e)) Binary) |
| 155 | (hfactor : ∀ e, Z e * H e * (Z e).transpose = x.val e) |
| 156 | (L R : Fin J → Component (Tag k) → Component (Tag k) → Moment k n b degree) |
| 157 | (l : Tag k) (s : Fin b → Binary) (z : Base k n → Binary) |
| 158 | (hz : ∀ i, i ∉ allowedBase k n l → z i = 0) : |
| 159 | mixingForm L R x (atom l s z hz) + mixingForm L R (atom l s z hz) x = |
| 160 | formalQuadratic (incident l) J H (rowMap (incident l) Z L R (point selectorEval s z)) |
| 161 | |
| 162 | axiom unary_rank_bound {k n b degree r₀ J : ℕ} {hr : 2 * r₀ ≤ n} |
| 163 | (D : Testers (k := k) (b := b) (degree := degree) hr) |
| 164 | (x : Profile k n b degree) {r : Component (Tag k) → ℕ} |
| 165 | (Z : ∀ e, Matrix (Coordinate k n b degree) (Fin (r e)) Binary) |
| 166 | (H : ∀ e, Matrix (Fin (r e)) (Fin (r e)) Binary) |
| 167 | (hfactor : ∀ e, Z e * H e * (Z e).transpose = x.val e) |
| 168 | (hH : ∀ e, Function.Injective (H e).mulVec) |
| 169 | (L R : Fin J → Component (Tag k) → Component (Tag k) → Moment k n b degree) |
| 170 | (l : Tag k) (s : Fin b → Binary) (z : Base k n → Binary) |
| 171 | (hz : ∀ i, i ∉ allowedBase k n l → z i = 0) (s₀ : ℕ) |
| 172 | (hA : Module.finrank Binary (Rows r (incident l) J) ≤ |
| 173 | Module.finrank Binary (LinearMap.range (zRows Z L R l s)) + s₀) : |
| 174 | 4 * J * (incident l).card * ∑ e, r e ≤ |
| 175 | (FormalQuadratic.polarMatrix (fun w => gradient D L R x (atomAlongZ l s z hz w))).rank + 2 * s₀ |
| 176 | |
| 177 | axiom unary_rank_lower {k n b degree r₀ J : ℕ} {hr : 2 * r₀ ≤ n} (hk : 0 < k) |
| 178 | (D : Testers (k := k) (b := b) (degree := degree) hr) |
| 179 | (x : Profile k n b degree) (hx : x ≠ 0) {r : Component (Tag k) → ℕ} |
| 180 | (Z : ∀ e, Matrix (Coordinate k n b degree) (Fin (r e)) Binary) |
| 181 | (H : ∀ e, Matrix (Fin (r e)) (Fin (r e)) Binary) |
| 182 | (hfactor : ∀ e, Z e * H e * (Z e).transpose = x.val e) |
| 183 | (hH : ∀ e, Function.Injective (H e).mulVec) |
| 184 | (L R : Fin J → Component (Tag k) → Component (Tag k) → Moment k n b degree) |
| 185 | (l : Tag k) (s : Fin b → Binary) (z : Base k n → Binary) |
| 186 | (hz : ∀ i, i ∉ allowedBase k n l → z i = 0) (s₀ : ℕ) |
| 187 | (hA : Module.finrank Binary (Rows r (incident l) J) ≤ |
| 188 | Module.finrank Binary (LinearMap.range (zRows Z L R l s)) + s₀) : |
| 189 | 2 * (J - s₀) ≤ |
| 190 | (FormalQuadratic.polarMatrix (fun w => gradient D L R x (atomAlongZ l s z hz w))).rank |
| 191 | |
| 192 | end Lax342547.UnaryMixer |
| 193 |
Used by
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments