OAI/Combinatorics/HadwigerCounterexample/GradientRealization.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Gradient Realization

  1. def OAI.HadwigerCounterexample.Rorth line 12
  2. def OAI.HadwigerCounterexample.qorth line 13
  3. def OAI.HadwigerCounterexample.rankInit line 14
  4. def OAI.HadwigerCounterexample.rankRes line 15
  5. def OAI.HadwigerCounterexample.rankAll line 16
  6. structure OAI.HadwigerCounterexample.realizeAssum line 19
  7. theorem OAI.HadwigerCounterexample.Volley.realize_one line 27
  8. def OAI.HadwigerCounterexample.addChan line 77

    Source documentation

    Lift the derivative changes into one actual abstract cross Gram (on column channel arguments only).

    def addChan (p : Shape) {n} (D : Bool → ChanOut p n) : Cross p n :=
…

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.ChanOut, OAI.HadwigerCounterexample.Cross

  9. theorem OAI.HadwigerCounterexample.addChan_val line 80
  10. def OAI.HadwigerCounterexample.zeroRow line 89
  11. theorem OAI.HadwigerCounterexample.row_add line 92
  12. theorem OAI.HadwigerCounterexample.addChan_zero line 99
  13. theorem OAI.HadwigerCounterexample.recip_effect line 117
  14. theorem OAI.HadwigerCounterexample.delta_frozen line 124
  15. theorem OAI.HadwigerCounterexample.recip_add line 129
  16. theorem OAI.HadwigerCounterexample.Volley.realized_changes line 134
  17. theorem OAI.HadwigerCounterexample.gradient_realization line 148