OAI/Combinatorics/HadwigerCounterexample/MixerProductVariables.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HadwigerCounterexample.Terms line 13
2. abbrev OAI.HadwigerCounterexample.Parts line 15
3. def OAI.HadwigerCounterexample.formCol line 18
4. theorem OAI.HadwigerCounterexample.formCol_true line 24
5. theorem OAI.HadwigerCounterexample.formCol_false line 27
6. theorem OAI.HadwigerCounterexample.qmix_eq line 31
7. theorem OAI.HadwigerCounterexample.formCol_add line 57
8. theorem OAI.HadwigerCounterexample.formCol_smul line 62
9. def OAI.HadwigerCounterexample.stackL line 72

   Source documentation

   Stacked evaluation of all columns on a batch of free directions.

   def stackL (P Q : Parts p n r) (l : Tag p.g) (W : Mat (Row p n) U) :
       Draw p n →ₗ[F] Mat U (Terms p l r ⊕ Terms p l r) where
   …

   Mentions: OAI.HadwigerCounterexample.Parts, OAI.HadwigerCounterexample.Tag, OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.Row, OAI.HadwigerCounterexample.Draw, OAI.HadwigerCounterexample.F, OAI.HadwigerCounterexample.Terms

10. theorem OAI.HadwigerCounterexample.formCol_onto line 87

    Source documentation

    Well away from the profile factors all the formal variables from a given side can be specified independently.

    theorem formCol_onto (P : Parts p n r) (l : Tag p.g) (W : Mat (Row p n) U)
        (hw : Function.Injective W.mulVec)
        (hP : ∀ i, Function.Injective (P i).mulVec)
        (h : ∀ i, Disjoint (colSp (P i)) (colSp W))
        (A : Mat U (Terms p l r)) :
        ∃ d : MArr p n, Wᵀ * formCol P l d=A := by
    …

    Mentions: OAI.HadwigerCounterexample.Parts, OAI.HadwigerCounterexample.Tag, OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.Row, OAI.HadwigerCounterexample.colSp, OAI.HadwigerCounterexample.Terms, OAI.HadwigerCounterexample.MArr, OAI.HadwigerCounterexample.formCol

11. theorem OAI.HadwigerCounterexample.stack_surj line 119