Baseline bilinear extensions retaining all frozen rows and columns
Lax342547.FrozenBaselines · concepts/Lax342547/FrozenBaselines.lean · lax-342547
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Lemma
Split each table space into its stored pin part and a complement, retaining the independent key space. An explicit bilinear formula extends both the table and every actual row or column through a pin or key. No gradient solvability or rank bound is assumed in this extension argument.
Concept map
Evidence
Lean source view on GitHub
| 1 | import Lax342547.MomentSpace |
| 2 | import Mathlib.LinearAlgebra.Basis.VectorSpace |
| 3 | import Mathlib.LinearAlgebra.Projection |
| 4 | import Mathlib.LinearAlgebra.BilinearMap |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Baseline bilinear extensions retaining all frozen rows and columns |
| 9 | type: lemma |
| 10 | --- |
| 11 | Split each table space into its stored pin part and a complement, retaining |
| 12 | the independent key space. An explicit bilinear formula extends both the |
| 13 | table and every actual row or column through a pin or key. No gradient |
| 14 | solvability or rank bound is assumed in this extension argument. |
| 15 | -/ |
| 16 | |
| 17 | namespace Lax342547.FrozenBaselines |
| 18 | |
| 19 | open Lax342547.MomentSpace |
| 20 | |
| 21 | variable {V W : Type} [AddCommGroup V] [Module Binary V] |
| 22 | [AddCommGroup W] [Module Binary W] |
| 23 | |
| 24 | structure Splitting (J D Keys : Submodule Binary V) where |
| 25 | frozen : V →ₗ[Binary] V |
| 26 | table : V →ₗ[Binary] J |
| 27 | frozen_fixed : ∀ v ∈ D ⊔ Keys, frozen v = v |
| 28 | table_zero : ∀ v ∈ D ⊔ Keys, table v = 0 |
| 29 | frozen_table : ∀ v : J, frozen v.val ∈ D |
| 30 | table_sum : ∀ v : J, frozen v.val + (table v.val).val = v.val |
| 31 | |
| 32 | def baseline {J D Keys : Submodule Binary V} {J' D' Keys' : Submodule Binary W} |
| 33 | (S : Splitting J D Keys) (S' : Splitting J' D' Keys') |
| 34 | (A : V →ₗ[Binary] W →ₗ[Binary] Binary) (T : J →ₗ[Binary] J' →ₗ[Binary] Binary) : |
| 35 | V →ₗ[Binary] W →ₗ[Binary] Binary := |
| 36 | A.compl₁₂ S.frozen LinearMap.id + A.compl₁₂ LinearMap.id S'.frozen - |
| 37 | A.compl₁₂ S.frozen S'.frozen + T.compl₁₂ S.table S'.table |
| 38 | |
| 39 | def Compatible (J D : Submodule Binary V) (J' D' : Submodule Binary W) |
| 40 | (A : V →ₗ[Binary] W →ₗ[Binary] Binary) (T : J →ₗ[Binary] J' →ₗ[Binary] Binary) : Prop := |
| 41 | ∀ v : J, ∀ w : J', v.val ∈ D ∨ w.val ∈ D' → T v w = A v.val w.val |
| 42 | |
| 43 | def ExtendsFrozen (D Keys : Submodule Binary V) (D' Keys' : Submodule Binary W) |
| 44 | (A B : V →ₗ[Binary] W →ₗ[Binary] Binary) : Prop := |
| 45 | ∀ v w, v ∈ D ⊔ Keys ∨ w ∈ D' ⊔ Keys' → B v w = A v w |
| 46 | |
| 47 | axiom splitting_exists (J D Keys : Submodule Binary V) (hD : D ≤ J) (hKeys : Disjoint J Keys) : |
| 48 | Nonempty (Splitting J D Keys) |
| 49 | |
| 50 | axiom baseline_properties (J D Keys : Submodule Binary V) (J' D' Keys' : Submodule Binary W) |
| 51 | (hD : D ≤ J) (hD' : D' ≤ J') |
| 52 | (S : Splitting J D Keys) (S' : Splitting J' D' Keys') |
| 53 | (A : V →ₗ[Binary] W →ₗ[Binary] Binary) (T : J →ₗ[Binary] J' →ₗ[Binary] Binary) |
| 54 | (h : Compatible J D J' D' A T) : |
| 55 | ExtendsFrozen D Keys D' Keys' A (baseline S S' A T) ∧ |
| 56 | ∀ v : J, ∀ w : J', baseline S S' A T v.val w.val = T v w |
| 57 | |
| 58 | end Lax342547.FrozenBaselines |
| 59 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments