OAI/Combinatorics/HadwigerCounterexample/MixedImageBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Mixed Image Bounds

  1. def OAI.HadwigerCounterexample.mixImage line 18
  2. def OAI.HadwigerCounterexample.mixImageLin line 20
  3. theorem OAI.HadwigerCounterexample.mixed_cap line 36

    Source documentation

    Exact image tests under a translate-stable minus (or plus) pair law cost dim T bits per vector. Directions mix both endpoints in one direct sum.

    theorem mixed_cap {w w' : Wgt (Mat U I)} (hw : SubLaw w) (hw' : SubLaw w')
    (T : Space (Vec U)) (hT : columnInv (w:=w) T) (hT' : columnInv (w:=w') T)
…

    Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.Mat, OAI.HadwigerCounterexample.SubLaw, OAI.HadwigerCounterexample.Space, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.columnInv

  4. theorem OAI.HadwigerCounterexample.kerTr_dim line 78
  5. theorem OAI.HadwigerCounterexample.two_kerTr line 88
  6. def OAI.HadwigerCounterexample.weakMinus line 102
  7. theorem OAI.HadwigerCounterexample.weak_shift line 104
  8. theorem OAI.HadwigerCounterexample.minus_le_weak line 116
  9. theorem OAI.HadwigerCounterexample.plus_le_unif line 136
  10. theorem OAI.HadwigerCounterexample.pair_cap_aux line 146
  11. theorem OAI.HadwigerCounterexample.comp_image_cap line 152