OAI/Combinatorics/PlanarL1/MainFamily.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PlanarL1.Columns.Model.MainFamily.BandIndex line 19
  2. def OAI.PlanarL1.Columns.Model.MainFamily.lower line 20
  3. abbrev OAI.PlanarL1.Columns.Model.MainFamily.BandComponent line 21
  4. instance OAI.PlanarL1.Columns.Model.MainFamily.(instance at line 22) line 22
  5. abbrev OAI.PlanarL1.Columns.Model.MainFamily.CellIndex line 24
  6. instance OAI.PlanarL1.Columns.Model.MainFamily.(instance at line 27) line 27
  7. abbrev OAI.PlanarL1.Columns.Model.MainFamily.tree line 32
  8. def OAI.PlanarL1.Columns.Model.MainFamily.radial line 33
  9. abbrev OAI.PlanarL1.Columns.Model.MainFamily.anchor line 34
  10. def OAI.PlanarL1.Columns.Model.MainFamily.domain line 35
  11. def OAI.PlanarL1.Columns.Model.MainFamily.neighborhood line 39

    Source documentation

    Availability is the manuscript's entire closed radius-one neighborhood of this full-column cell, not just tests at the finite original vertices.

    def neighborhood : Set (M.Point Set.univ A.root) :=
…
  12. def OAI.PlanarL1.Columns.Model.MainFamily.Available line 41
  13. def OAI.PlanarL1.Columns.Model.MainFamily.index line 44
  14. lemma OAI.PlanarL1.Columns.Model.MainFamily.same_name line 45
  15. lemma OAI.PlanarL1.Columns.Model.MainFamily.sub_old line 49
  16. def OAI.PlanarL1.Columns.Model.MainFamily.step line 60

    Source documentation

    Every kept, available cell becomes an actual MainStep, including its old chart and exact interpolation tree. All parameters are the fixed constants.

    noncomputable def step (hc : Available A S phase c)
    (noise : Point.RadialTree.Noise (n := k+1)) (hn : (tree phase c).NoiseBounds noise)
…

    Mentions: OAI.PlanarL1.Columns.Model.MainFamily.Available, OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise, OAI.PlanarL1.Columns.Model.MainFamily.tree

  17. lemma OAI.PlanarL1.Columns.Model.MainFamily.cell_column_component line 87
  18. lemma OAI.PlanarL1.Columns.Model.MainFamily.unique_in_band line 92
  19. lemma OAI.PlanarL1.Columns.Model.MainFamily.domain_band line 110
  20. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainStep.endpoint_old line 122
  21. abbrev OAI.PlanarL1.Columns.Model.MainFamily.CellSample line 146
  22. abbrev OAI.PlanarL1.Columns.Model.MainFamily.Sample line 148
  23. instance OAI.PlanarL1.Columns.Model.MainFamily.(instance at line 149) line 149
  24. instance OAI.PlanarL1.Columns.Model.MainFamily.(instance at line 150) line 150
  25. def OAI.PlanarL1.Columns.Model.MainFamily.kept line 154
  26. abbrev OAI.PlanarL1.Columns.Model.MainFamily.Kept line 155
  27. instance OAI.PlanarL1.Columns.Model.MainFamily.(instance at line 156) line 156
  28. lemma OAI.PlanarL1.Columns.Model.MainFamily.shield_bound line 159
  29. def OAI.PlanarL1.Columns.Model.MainFamily.keptStep line 166
  30. lemma OAI.PlanarL1.Columns.Model.MainFamily.overlap line 172
  31. def OAI.PlanarL1.Columns.Model.MainFamily.batch line 197

    Source documentation

    The simultaneous main mode is now genuinely defined for every old state and every finite sample. Its family contains exactly the available kept cells.

    noncomputable def batch : OrdinaryState.MainBatch S where
…

    Mentions: OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch

  32. def OAI.PlanarL1.Columns.Model.MainFamily.result line 210
  33. def OAI.PlanarL1.Columns.Model.MainFamily.execution line 215

    Source documentation

    Fresh offsets and cell coins are sampled as a finite product, after the bands and radial origins; unavailable cells simply discard their sample.

    noncomputable def execution [SFinite μ] :
    Execution (OrdinaryState M kappaA (Ω × Bool) (μ.prod Threshold.fair)) :=
…

    Mentions: OAI.PlanarL1.Execution, OAI.PlanarL1.Columns.Model.OrdinaryState, OAI.PlanarL1.Threshold.fair

  34. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.point_description line 232
  35. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.apply_sets line 248
  36. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.movement_integrable line 250
  37. lemma OAI.PlanarL1.Columns.Model.OrdinaryState.MainBatch.movement_bound line 264

    Source documentation

    The number of simultaneous cells never enters the movement bound.

    lemma movement_bound (hκ : 0≤κ) (i : Fin n) (H : ℝ) :
    (∫ ω, |(B.sets.activity ω).indicator i H-
      (S.lift.sets.activity ω).indicator i H| ∂(μ.prod Threshold.fair)) ≤ κ*(1+(1:ℝ)/100) := by
…

    Mentions: OAI.PlanarL1.Threshold.fair

  38. lemma OAI.PlanarL1.Columns.Model.BandTrees.main_cover line 291
  39. lemma OAI.PlanarL1.Columns.Model.MainFamily.cover line 321
  40. lemma OAI.PlanarL1.Columns.Model.MainFamily.ambient_dist_le line 332
  41. lemma OAI.PlanarL1.Columns.Model.MainFamily.cell_diameter line 339
  42. lemma OAI.PlanarL1.Columns.Model.MainFamily.available_of_ball line 351

    Source documentation

    The full-neighborhood availability test is derived from a common old radius-20 ball; it is not an extra hypothesis on the random execution.

    lemma available_of_ball (c : CellIndex q L U phase) (x : M.Point Set.univ A.root)
    (hx : x.height ∈ domain phase c x.column)
    (hname : ∃ a : Fin (S.count+1), ∀ y : M.Point Set.univ A.root,
      dist x y≤20 → S.name y.column y.height=a) : Available A S phase c := by
…

    Mentions: OAI.PlanarL1.Columns.Model.MainFamily.CellIndex, OAI.PlanarL1.Columns.Model.MainFamily.domain, OAI.PlanarL1.Columns.Model.MainFamily.Available