OAI/Combinatorics/PlanarL1/Schedule.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarL1.Parameters.persistenceSlope line 10
  2. def OAI.PlanarL1.Parameters.persistenceCount line 14
  3. lemma OAI.PlanarL1.Parameters.persistenceSlope_nonneg line 16
  4. lemma OAI.PlanarL1.Parameters.persistenceCount_pos line 27
  5. lemma OAI.PlanarL1.Parameters.persistenceLoss_eq line 32
  6. def OAI.PlanarL1.Parameters.GoodSpacing line 47

    Source documentation

    A single universal integer spacing. It is independent of the graph, its edge lengths, the number of scales, and every finite random grid.

    def GoodSpacing (Q : ℝ) : Prop :=
…
  7. lemma OAI.PlanarL1.Parameters.exists_goodSpacing line 50
  8. lemma OAI.PlanarL1.Parameters.exists_mesh line 75
  9. lemma OAI.PlanarL1.Execution.bind_assoc line 94
  10. def OAI.PlanarL1.Execution.iterate line 100
  11. lemma OAI.PlanarL1.Execution.iterate_add line 103
  12. lemma OAI.PlanarL1.Execution.Holds.iterate line 110
  13. lemma OAI.PlanarL1.Execution.Holds.and line 116
  14. lemma OAI.PlanarL1.Execution.prob_iterate_monotone line 121
  15. lemma OAI.PlanarL1.Execution.iterate_loss line 131
  16. lemma OAI.PlanarL1.Execution.Holds.prob_compl_zero line 145
  17. def OAI.PlanarL1.Parameters.targetRadius line 156
  18. lemma OAI.PlanarL1.Parameters.targetRadius_nonneg line 157
  19. lemma OAI.PlanarL1.Parameters.targetRadius_self line 160
  20. lemma OAI.PlanarL1.Parameters.targetRadius_succ line 163
  21. lemma OAI.PlanarL1.Parameters.targetRadius_small line 167
  22. lemma OAI.PlanarL1.Parameters.sum_targetRadius line 174
  23. lemma OAI.PlanarL1.Parameters.sum_persistenceLoss line 185
  24. def OAI.PlanarL1.Parameters.survivalBudget line 201
  25. lemma OAI.PlanarL1.Parameters.survivalBudget_zero line 203
  26. lemma OAI.PlanarL1.Parameters.survivalBudget_succ line 206
  27. lemma OAI.PlanarL1.Parameters.survivalBudget_lower line 213
  28. lemma OAI.PlanarL1.Parameters.GoodSpacing.pos line 236
  29. lemma OAI.PlanarL1.Parameters.GoodSpacing.one line 237
  30. lemma OAI.PlanarL1.Parameters.GoodSpacing.gt_one line 238
  31. lemma OAI.PlanarL1.Parameters.GoodSpacing.gap line 239
  32. def OAI.PlanarL1.Columns.Model.World.run line 246
  33. def OAI.PlanarL1.Columns.Model.World.Distances line 249
  34. lemma OAI.PlanarL1.Columns.Model.World.distances_zero line 251
  35. lemma OAI.PlanarL1.Columns.Model.World.next_distances line 252
  36. lemma OAI.PlanarL1.Columns.Model.World.run_distances line 258
  37. def OAI.PlanarL1.Columns.Model.World.TargetGood line 262
  38. lemma OAI.PlanarL1.Columns.Model.World.target_failure line 264
  39. lemma OAI.PlanarL1.Columns.Model.World.run_target_failure line 275
  40. lemma OAI.PlanarL1.Columns.Model.World.run_success_probability line 288
  41. lemma OAI.PlanarL1.Columns.Model.World.run_add line 306
  42. lemma OAI.PlanarL1.Columns.Model.World.run_survival_probability line 309
  43. def OAI.PlanarL1.Parameters.scheduleGain line 330
  44. lemma OAI.PlanarL1.Parameters.scheduleGain_pos line 331
  45. def OAI.PlanarL1.Columns.Model.World.averagedCuts line 338
  46. lemma OAI.PlanarL1.Columns.Model.World.averagedCuts_upper line 340
  47. lemma OAI.PlanarL1.Columns.Model.World.averagedCuts_designated line 347
  48. lemma OAI.PlanarL1.Columns.Model.World.averagedCuts_lower line 374
  49. def OAI.PlanarL1.Columns.Model.World.startAt line 398
  50. lemma OAI.PlanarL1.Columns.Model.World.startAt_distance line 401
  51. lemma OAI.PlanarL1.Columns.Model.World.startAt_coherent line 404
  52. def OAI.PlanarL1.Columns.Model.World.normalizedCuts line 406
  53. lemma OAI.PlanarL1.Columns.Model.World.normalization_cancel line 411
  54. lemma OAI.PlanarL1.Columns.Model.World.normalizedCuts_upper line 416
  55. lemma OAI.PlanarL1.Columns.Model.World.normalizedCuts_lower line 423
  56. lemma OAI.PlanarL1.Parameters.first_scale line 443
  57. lemma OAI.PlanarL1.Parameters.integer_offset line 459
  58. lemma OAI.PlanarL1.Parameters.finite_schedule_cover line 479

    Source documentation

    A finite family of Q offsets covers arbitrary positive distances. Only the number of iterations and the initial units depend on the finite metric.

    lemma finite_schedule_cover {V : Type*} [Fintype V] (d : V → V → ℝ)
    (hd : ∀ x y, 0≤d x y) {q : ℕ} (hq : 1<(q:ℝ)) :
    ∃ ε : ℝ, 0<ε ∧ ∃ N : ℕ, ∀ x y, 0<d x y →
      ∃ i : Fin q, ∃ f : ℕ, f<N ∧
        1≤(q:ℝ)^f*(ε/((i.val+1:ℕ):ℝ))*d x y ∧
        (q:ℝ)^f*(ε/((i.val+1:ℕ):ℝ))*d x y<2 := by
…