OAI/Combinatorics/PlanarL1/Persistence.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.persistence_fixed line 31
  2. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.persistence_probability line 59
  3. lemma OAI.PlanarL1.Execution.choose_upper line 84
  4. lemma OAI.PlanarL1.Parameters.mainLoss_nonneg line 95
  5. lemma OAI.PlanarL1.Parameters.secondaryLoss_nonneg line 98
  6. def OAI.PlanarL1.Parameters.persistenceLoss line 100
  7. def OAI.PlanarL1.Columns.Model.CoupledState.Coherent line 113
  8. lemma OAI.PlanarL1.Columns.Model.CoupledState.Coherent.lift line 118
  9. lemma OAI.PlanarL1.Columns.Model.CoupledState.main_persistence line 131
  10. lemma OAI.PlanarL1.Columns.Model.CoupledState.secondary_persistence line 150
  11. lemma OAI.PlanarL1.Columns.Model.CoupledState.modes_persistence line 168
  12. lemma OAI.PlanarL1.Columns.Model.CoupledState.step_persistence line 199
  13. lemma OAI.PlanarL1.Columns.Model.SetSystem.dilate_separation line 218
  14. lemma OAI.PlanarL1.Columns.Model.PairGeometry.Certificate.dilate line 226
  15. lemma OAI.PlanarL1.Columns.Model.CoupledState.Successful.dilate line 245
  16. lemma OAI.PlanarL1.Columns.Model.CoupledState.coherent_dilate line 257