OAI/Combinatorics/PlanarL1/CoupledState.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarL1.Parameters.heightLoss line 10
  2. lemma OAI.PlanarL1.Parameters.heightLoss_nonneg line 12
  3. def OAI.PlanarL1.Columns.Model.VertexBands.HeightPadded line 27
  4. lemma OAI.PlanarL1.Columns.Model.VertexBands.height_padding_loss line 31
  5. lemma OAI.PlanarL1.Columns.Model.VertexBands.conditional_persistence line 73
  6. lemma OAI.PlanarL1.Columns.Model.SetSystem.lift_separation line 95
  7. lemma OAI.PlanarL1.Columns.Model.PairGeometry.Certificate.mono line 108
  8. lemma OAI.PlanarL1.Columns.Model.PairGeometry.Certificate.lift line 112
  9. structure OAI.PlanarL1.Columns.Model.CoupledState line 125

    Source documentation

    The two literal cut/chart systems together with every B chart's recorded increment history. The radius bound is an invariant, not a separation promise.

    structure CoupledState (A : Ambient M) (Ω Ξ : Type*) [MeasurableSpace Ω] [MeasurableSpace Ξ]
    (μ : Measure Ω) (ν : Measure Ξ) (t : ℝ) where
…

    Mentions: OAI.PlanarL1.Columns.Model.Ambient

  10. def OAI.PlanarL1.Columns.Model.CoupledState.lift line 133
  11. def OAI.PlanarL1.Columns.Model.CoupledState.weaken line 138
  12. def OAI.PlanarL1.Columns.Model.CoupledState.dilate line 142
  13. def OAI.PlanarL1.Columns.Model.CoupledState.Successful line 149
  14. lemma OAI.PlanarL1.Columns.Model.CoupledState.Successful.mono line 153
  15. lemma OAI.PlanarL1.Columns.Model.CoupledState.Successful.lift line 159
  16. lemma OAI.PlanarL1.Execution.choose_lower line 175
  17. lemma OAI.PlanarL1.Execution.choose4_lower line 180
  18. lemma OAI.PlanarL1.Execution.prob_pure line 184
  19. lemma OAI.PlanarL1.Execution.prob_pure_of line 188
  20. lemma OAI.PlanarL1.Columns.Model.CoupledState.cross line 203
  21. abbrev OAI.PlanarL1.Columns.Model.CoupledState.Next line 207
  22. def OAI.PlanarL1.Columns.Model.CoupledState.unchanged line 210
  23. def OAI.PlanarL1.Columns.Model.CoupledState.main line 218
  24. def OAI.PlanarL1.Columns.Model.CoupledState.groups line 224
  25. def OAI.PlanarL1.Columns.Model.CoupledState.secondary line 226
  26. def OAI.PlanarL1.Columns.Model.CoupledState.increment line 233
  27. def OAI.PlanarL1.Columns.Model.CoupledState.branches line 240
  28. def OAI.PlanarL1.Columns.Model.CoupledState.modes line 245
  29. def OAI.PlanarL1.Columns.Model.CoupledState.step line 248