OAI/Combinatorics/PlanarL1/FamilyPersistence.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PlanarL1.Columns.Model.SecondaryCell.mem_domain_iff_distance line 15
  2. lemma OAI.PlanarL1.Columns.Model.SecondaryCell.point_eq line 23
  3. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullNamed_at line 32
  4. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullNamed_boundary_ball line 39

    Source documentation

    A crossed seed-domain is identically old on the small ball, including its actual deterministic branch name. No independence or pruning assumption.

    lemma fullNamed_boundary_ball (x y : M.Point J root) {ρ : ℝ}
    (hsmall : 18*ρ≤(199/1000:ℝ)*U.radius) (hy : dist x y≤ρ)
    (hout : y.height ∉ SecondaryCell.domain U.seeds U.radius y.column)
    (z : M.Point J root) (hz : dist x z≤ρ) :
    U.fullNamed z.column ⟨z.height,U.sub_old z.inBand⟩=⟨0,U.old z⟩ := by
…

    Mentions: OAI.PlanarL1.Columns.Model.SecondaryCell.domain

  5. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.group_touched_band line 76
  6. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.group_touched_envelope line 81
  7. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.group_local_center line 87
  8. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.ball_domain_touch line 93
  9. lemma OAI.PlanarL1.Columns.Model.Field.ball_variation line 127
  10. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.point_dist line 145
  11. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullNamed_boundary_global line 160

    Source documentation

    Crossing the domain anywhere on the ambient small ball makes this actual proposal identically old on that ball. Intrinsic paths are derived by height padding, rather than silently identified with ambient paths.

    lemma fullNamed_boundary_global (x y z : M.Point Set.univ r) {ρ : ℝ} (hρ : 0≤ρ)
    (hJ : ∀ H, |H-x.height|≤ρ → H ∈ J)
    (hsmall : 18*ρ≤(199/1000:ℝ)*U.radius) (hy : dist x y≤ρ)
    (hout : y.height ∉ SecondaryCell.domain U.seeds U.radius y.column)
    (hz : dist x z≤ρ) (hZ : z.height ∈ U.data.band) :
    U.fullNamed z.column ⟨z.height,hZ⟩=⟨0,U.comparison.value z.column ⟨z.height,hZ⟩⟩ := by
…

    Mentions: OAI.PlanarL1.Columns.Model.SecondaryCell.domain

  12. def OAI.PlanarL1.Parameters.secondaryK line 189
  13. def OAI.PlanarL1.Parameters.secondaryQ line 190
  14. def OAI.PlanarL1.Parameters.secondaryRadius line 191
  15. def OAI.PlanarL1.Parameters.secondaryN line 192
  16. def OAI.PlanarL1.Parameters.secondaryTestLoss line 193
  17. lemma OAI.PlanarL1.Parameters.secondaryTestLoss_nonneg line 195
  18. abbrev OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.Offset line 208
  19. def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.sampledStep line 209
  20. abbrev OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.Ball line 214
  21. def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.ballCenter line 215
  22. def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.oldOnBall line 217
  23. def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.sampledOnBall line 219
  24. lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.sampledStep_seeds line 222
  25. lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.sampledStep_radius line 224
  26. lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.component_local_list line 227
  27. def OAI.PlanarL1.Interpolation.scaleNamed line 294
  28. lemma OAI.PlanarL1.Interpolation.maxNamed_scale line 295
  29. lemma OAI.PlanarL1.Interpolation.maxSelection_scale line 299
  30. lemma OAI.PlanarL1.Interpolation.familySelection_scale line 306
  31. abbrev OAI.PlanarL1.Columns.Model.SecondaryGeometry.Coordinate line 329
  32. abbrev OAI.PlanarL1.Columns.Model.SecondaryGeometry.Offsets line 330
  33. instance OAI.PlanarL1.Columns.Model.SecondaryGeometry.(instance at line 331) line 331
  34. def OAI.PlanarL1.Columns.Model.SecondaryGeometry.flatSample line 333
  35. def OAI.PlanarL1.Columns.Model.SecondaryGeometry.fixedSample line 334
  36. def OAI.PlanarL1.Columns.Model.SecondaryGeometry.slot line 335
  37. def OAI.PlanarL1.Columns.Model.SecondaryGeometry.coord line 337
  38. lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.coord_injective line 339
  39. lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.flat_actingStep line 345
  40. lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.coord_index line 350
  41. lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.slot_band line 352
  42. lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.selected_flat line 358
  43. lemma OAI.PlanarL1.Interpolation.maxSelection_map line 380
  44. lemma OAI.PlanarL1.Interpolation.familySelection_map line 386
  45. lemma OAI.PlanarL1.Interpolation.maxSelection_eq_fold line 392
  46. lemma OAI.PlanarL1.Interpolation.familySelection_congr_at line 398
  47. abbrev OAI.PlanarL1.Columns.Model.SecondaryGeometry.Slot line 424
  48. def OAI.PlanarL1.Columns.Model.SecondaryGeometry.ballOld line 426
  49. lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.ball_slot_band line 429
  50. def OAI.PlanarL1.Columns.Model.SecondaryGeometry.ballFamily line 432
  51. lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.ballOld_eq line 436
  52. lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.selected_ball line 447
  53. def OAI.PlanarL1.Columns.Model.SecondaryGeometry.wholeBallSlots line 456
  54. lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.persistence_flat line 460
  55. lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.component_eq_of_domain line 515
  56. def OAI.PlanarL1.Columns.Model.RetainedSelection.centerActs line 549
  57. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.centerActs_card line 554
  58. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.center_point_of_domain line 601
  59. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.wholeBallSlots_card line 614
  60. def OAI.PlanarL1.Parameters.mainK line 654
  61. def OAI.PlanarL1.Parameters.mainQ line 655
  62. def OAI.PlanarL1.Parameters.mainRadius line 656
  63. def OAI.PlanarL1.Parameters.mainN line 657
  64. def OAI.PlanarL1.Parameters.mainTestLoss line 658
  65. def OAI.PlanarL1.Parameters.mainLoss line 660
  66. def OAI.PlanarL1.Parameters.secondaryLoss line 661
  67. lemma OAI.PlanarL1.Parameters.mainQ_pos line 663
  68. lemma OAI.PlanarL1.Parameters.mainRadius_pos line 664
  69. lemma OAI.PlanarL1.Parameters.secondaryQ_pos line 665
  70. lemma OAI.PlanarL1.Parameters.secondaryRadius_pos line 666
  71. def OAI.PlanarL1.Parameters.persistenceRadius line 667
  72. lemma OAI.PlanarL1.Parameters.persistenceRadius_pos line 669
  73. lemma OAI.PlanarL1.Parameters.persistence_main_small line 672
  74. lemma OAI.PlanarL1.Parameters.persistence_main_radius line 676
  75. lemma OAI.PlanarL1.Parameters.persistence_secondary_small line 678
  76. lemma OAI.PlanarL1.Parameters.persistence_secondary_radius line 681
  77. lemma OAI.PlanarL1.Columns.Model.MainFamily.localLoss_eq line 689
  78. lemma OAI.PlanarL1.Columns.Model.MainFamily.radius_eq line 691