OAI/Combinatorics/PlanarL1/CutExtraction.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarL1.Columns.Model.SetSystem.refinedBinary line 17
  2. def OAI.PlanarL1.Columns.Model.SetSystem.cuts line 32
  3. lemma OAI.PlanarL1.Columns.Model.SetSystem.cuts_distance line 34
  4. lemma OAI.PlanarL1.Columns.Model.SetSystem.cuts_upper line 44
  5. lemma OAI.PlanarL1.Columns.Model.SetSystem.cuts_dominates line 47
  6. lemma OAI.PlanarL1.Columns.Model.PairGeometry.Certificate.cuts line 54
  7. def OAI.PlanarL1.Columns.Model.CoupledState.cuts line 76
  8. lemma OAI.PlanarL1.Columns.Model.CoupledState.cuts_upper line 77
  9. lemma OAI.PlanarL1.Columns.Model.CoupledState.Successful.cuts line 80
  10. instance OAI.PlanarL1.Threshold.labelMeasure_sfinite line 97
  11. structure OAI.PlanarL1.Columns.Model.World line 107

    Source documentation

    A state of the actual construction in its current physical units. Both label spaces are enlarged at every step, even in the no-change mode.

    structure World (k : ℕ) (V : Type*) (Q : ℝ) where
…
  12. def OAI.PlanarL1.Columns.Model.World.heightBound line 122
  13. lemma OAI.PlanarL1.Columns.Model.World.height_bounds line 123
  14. def OAI.PlanarL1.Columns.Model.World.after line 128
  15. def OAI.PlanarL1.Columns.Model.World.step line 136
  16. def OAI.PlanarL1.Columns.Model.World.Coherent line 139
  17. def OAI.PlanarL1.Columns.Model.World.Successful line 140
  18. def OAI.PlanarL1.Columns.Model.World.distance line 141
  19. def OAI.PlanarL1.Columns.Model.World.cuts line 142
  20. lemma OAI.PlanarL1.Columns.Model.World.cuts_upper line 143
  21. lemma OAI.PlanarL1.Columns.Model.World.Successful.cuts line 144
  22. lemma OAI.PlanarL1.Columns.Model.World.Successful.mono line 146
  23. lemma OAI.PlanarL1.Columns.Model.World.after_distance line 149
  24. lemma OAI.PlanarL1.Columns.Model.World.after_coherent line 152
  25. lemma OAI.PlanarL1.Columns.Model.World.after_successful line 156
  26. lemma OAI.PlanarL1.Columns.Model.World.step_distances line 159
  27. lemma OAI.PlanarL1.Columns.Model.World.step_survives line 165
  28. lemma OAI.PlanarL1.Columns.Model.World.step_persistence line 171
  29. lemma OAI.PlanarL1.Columns.Model.World.coherent_eligible line 183
  30. lemma OAI.PlanarL1.Columns.Model.World.step_success line 203
  31. def OAI.PlanarL1.Columns.Model.World.initial line 212
  32. lemma OAI.PlanarL1.Columns.Model.World.initial_coherent line 223