OAI/Combinatorics/HadwigerCounterexample/PrimalChannelDecomposition.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Primal Channel Decomposition

  1. structure OAI.HadwigerCounterexample.ProjData line 14

    Source documentation

    Onto projection in coordinates, killing a specified disjoint subspace.

    structure ProjData (S T : Space (Vec I)) (A : Mat I I) : Prop where
…

    Mentions: OAI.HadwigerCounterexample.Space, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.Mat

  2. theorem OAI.HadwigerCounterexample.proj_exists line 19
  3. theorem OAI.HadwigerCounterexample.rank_maps line 39
  4. theorem OAI.HadwigerCounterexample.evmat_addM line 44
  5. theorem OAI.HadwigerCounterexample.evmat_subM line 48
  6. def OAI.HadwigerCounterexample.primal line 55

    Source documentation

    aggregate primal (resp. channel) directions in a unit.

    def primal (p : Shape) (n : ℕ) := colSp (IP p n true) ⊔ colSp (IP p n false)

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.colSp, OAI.HadwigerCounterexample.IP

  7. def OAI.HadwigerCounterexample.channels line 56
  8. theorem OAI.HadwigerCounterexample.ip_le_primal line 58
  9. theorem OAI.HadwigerCounterexample.ih_le_channels line 61
  10. theorem OAI.HadwigerCounterexample.channels_proj line 64
  11. theorem OAI.HadwigerCounterexample.primal_proj line 71
  12. theorem OAI.HadwigerCounterexample.channels_disjoint line 78
  13. def OAI.HadwigerCounterexample.prSmall line 90

    Source documentation

    prSmall a z consists of the pure-primal coordinates kept by the small table.

    def prSmall (a : Plan p n) (z : Place p) :=
…

    Mentions: OAI.HadwigerCounterexample.Plan, OAI.HadwigerCounterexample.Place

  14. theorem OAI.HadwigerCounterexample.prSmall_le line 94
  15. theorem OAI.HadwigerCounterexample.prSmall_dim line 97
  16. theorem OAI.HadwigerCounterexample.prSmall_table line 105
  17. theorem OAI.HadwigerCounterexample.keyPlane line 110