OAI/Combinatorics/PlanarL1/Separation.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarL1.Columns.Model.Ambient.taper_of_ball line 16
  2. def OAI.PlanarL1.Columns.Model.OrderedData.incrementField line 33
  3. lemma OAI.PlanarL1.Columns.Model.OrderedData.incrementField_eq line 40
  4. lemma OAI.PlanarL1.Columns.Model.OrderedData.exists_increment_gain line 66

    Source documentation

    Genuine append-only histories have a favorable fair sign. The old field may be arbitrary and is not discarded in this difference calculation.

    lemma exists_increment_gain {root : Fin (k+1)} (x y : M.Point D.band root)
    (hx : ∀ z, dist (A.point x.column x.height) z≤1 → z ∈ region)
    (hy : ∀ z, dist (A.point y.column y.height) z≤1 → z ∈ region)
    (ho : (D.base.transverse (by norm_num) D.lower D.upper).eval x *
      (D.base.transverse (by norm_num) D.lower D.upper).eval y<0)
    (hlx : R/100≤|(D.base.transverse (by norm_num) D.lower D.upper).eval x|)
    (hly : R/100≤|(D.base.transverse (by norm_num) D.lower D.upper).eval y|)
    (hux : |(D.base.transverse (by norm_num) D.lower D.upper).eval x|≤8)
    (huy : |(D.base.transverse (by norm_num) D.lower D.upper).eval y|≤8) :
    ∃ e : Bool, lambda*R/50 ≤
      |(D.incrementField H region hcross e).eval x-(D.incrementField H region hcross e).eval y| := by
…
  5. def OAI.PlanarL1.Columns.Model.SetSystem.separation line 123
  6. lemma OAI.PlanarL1.Columns.Model.SetSystem.separation_nonneg line 126
  7. lemma OAI.PlanarL1.Columns.Model.BState.common_separation line 133
  8. lemma OAI.PlanarL1.Columns.Model.BState.common_separation_height line 140
  9. lemma OAI.PlanarL1.Columns.Model.BState.common_separation_field line 146
  10. lemma OAI.PlanarL1.Columns.Model.BState.fieldUpdate_separation line 155
  11. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.common_separation line 171
  12. def OAI.PlanarL1.Columns.Model.VertexTests.indexA line 207
  13. def OAI.PlanarL1.Columns.Model.VertexTests.indexB line 208
  14. def OAI.PlanarL1.Columns.Model.VertexTests.ordinaryValue line 209
  15. def OAI.PlanarL1.Columns.Model.VertexTests.fullValue line 211
  16. lemma OAI.PlanarL1.Columns.Model.VertexTests.ordinary_value_transport line 215
  17. lemma OAI.PlanarL1.Columns.Model.VertexTests.full_value_transport line 218
  18. def OAI.PlanarL1.Columns.Model.VertexTests.Eligible line 225

    Source documentation

    The actual eligibility test in : both unrestricted closed radius-five balls, with one common identifier in each of the two systems.

    def Eligible (x y : V) : Prop :=
…
  19. def OAI.PlanarL1.Columns.Model.VertexTests.PairTest line 231
  20. def OAI.PlanarL1.Columns.Model.VertexTests.Cutoffs line 234
  21. lemma OAI.PlanarL1.Columns.Model.VertexTests.Eligible.namesA line 239
  22. lemma OAI.PlanarL1.Columns.Model.VertexTests.Eligible.namesB line 241
  23. lemma OAI.PlanarL1.Columns.Model.VertexTests.Eligible.symm line 243
  24. lemma OAI.PlanarL1.Columns.Model.VertexTests.Cutoffs.symm line 247
  25. def OAI.PlanarL1.Columns.Model.VertexTests.cutoffGain line 250
  26. lemma OAI.PlanarL1.Columns.Model.VertexTests.cutoffGain_pos line 251
  27. lemma OAI.PlanarL1.Columns.Model.VertexTests.separation_of_cutoff_failure line 255

    Source documentation

    A failed literal cutoff already supplies an actual cut separation. No rescaling, refinement, or desired probability is hidden in this alternative.

    lemma separation_of_cutoff_failure {x y : V} (h : Eligible A SA SB v x y)
    (hf : ¬Cutoffs A SA SB v x y) :
    cutoffGain≤SA.sets.separation (v x).column (v x).height (v y).column (v y).height ∨
    cutoffGain≤SB.sets.separation (v x).column (v x).height (v y).column (v y).height := by
…

    Mentions: OAI.PlanarL1.Columns.Model.VertexTests.Eligible, OAI.PlanarL1.Columns.Model.VertexTests.Cutoffs, OAI.PlanarL1.Columns.Model.VertexTests.cutoffGain

  28. def OAI.PlanarL1.Columns.Model.VertexTests.eligiblePairs line 302
  29. lemma OAI.PlanarL1.Columns.Model.VertexTests.mem_eligiblePairs line 303