OAI/Combinatorics/HadwigerCounterexample/OffsetLifting.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.col_follow line 14
2. theorem OAI.HadwigerCounterexample.col_retain line 20
3. theorem OAI.HadwigerCounterexample.trans_surj line 25
4. theorem OAI.HadwigerCounterexample.pull_cols line 29
5. theorem OAI.HadwigerCounterexample.chop_inj_pack line 40
6. theorem OAI.HadwigerCounterexample.frame_image_lift line 50
7. theorem OAI.HadwigerCounterexample.projected_unique line 61
8. structure OAI.HadwigerCounterexample.FrameProduct line 74
9. theorem OAI.HadwigerCounterexample.frame_extend line 81
10. theorem OAI.HadwigerCounterexample.frame_products line 108
11. theorem OAI.HadwigerCounterexample.diff_into line 137
12. theorem OAI.HadwigerCounterexample.one_offsets line 158

    Source documentation

    δ expansion at one component: S*T offsets bases plus paired companions Z for either reference endpoint. Cost recorded in actual offset widths kp/km and kernel matrices.

    theorem one_offsets (M : Bool → Mat I I) (S T : Space (Vec I))
        (a b : Bool → Space (Vec I))
        (h : ∀ i,M i∈box (a i) (b i)) (hg : vanish S T (M true+M false))
        (ha : ∀ i,Disjoint S (a i)) (hb : ∀ i,Disjoint T (b i)) :
        ∃ (kp km : ℕ) (A : Mat (Fin (dim S)) (Fin kp)) (B : Mat (Fin (dim T)) (Fin km))
          (H : Mat (Fin kp) (Fin km)),
          let X := pack S * A
    …

    Mentions: OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.Space, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.box, OAI.HadwigerCounterexample.vanish, OAI.HadwigerCounterexample.dim, OAI.HadwigerCounterexample.pack