OAI/Combinatorics/PlanarL1/Movement.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.full_movement line 17
  2. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.selected_movement line 32
  3. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.old_indicator_inside line 41
  4. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.movement_integrable line 54
  5. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryBatch.movement_bound line 65
  6. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.movement_integrable line 85
  7. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryLayer.movement_bound line 92
  8. lemma OAI.PlanarL1.Columns.Model.SetSystem.separation_survival line 114
  9. lemma OAI.PlanarL1.Columns.Model.PairGeometry.Certificate.survive line 144
  10. def OAI.PlanarL1.Execution.Holds line 205
  11. lemma OAI.PlanarL1.Execution.holds_of_forall line 208
  12. lemma OAI.PlanarL1.Execution.Holds.mono line 212
  13. lemma OAI.PlanarL1.Execution.Holds.bind line 217
  14. lemma OAI.PlanarL1.Execution.holds_bind_of_forall line 223
  15. lemma OAI.PlanarL1.Execution.Holds.mean_mono line 226
  16. lemma OAI.PlanarL1.Execution.Holds.prob_mono line 233
  17. lemma OAI.PlanarL1.Execution.Holds.prob_eq_one line 242
  18. lemma OAI.PlanarL1.Execution.Holds.mean_eq line 247
  19. lemma OAI.PlanarL1.Columns.Model.SetSystem.lift_movement line 263
  20. lemma OAI.PlanarL1.Columns.Model.BState.increment_integrable line 275
  21. def OAI.PlanarL1.Columns.Model.CoupledState.Moves line 297
  22. lemma OAI.PlanarL1.Columns.Model.CoupledState.Moves.successful line 303
  23. lemma OAI.PlanarL1.Columns.Model.CoupledState.unchanged_moves line 319
  24. lemma OAI.PlanarL1.Columns.Model.CoupledState.main_moves line 332
  25. lemma OAI.PlanarL1.Columns.Model.CoupledState.secondary_moves line 339
  26. lemma OAI.PlanarL1.Columns.Model.CoupledState.increment_moves line 347
  27. lemma OAI.PlanarL1.Columns.Model.CoupledState.modes_moves line 363
  28. lemma OAI.PlanarL1.Columns.Model.CoupledState.step_moves line 376
  29. lemma OAI.PlanarL1.FiniteRandom.prob_eq_instances line 390
  30. lemma OAI.PlanarL1.FiniteRandom.prob_bound_of_instances line 394
  31. lemma OAI.PlanarL1.FiniteRandom.prob_prod_bound_any line 397