OAI/Combinatorics/PlanarL1/RadialTree.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

The actual radial-node tree and its interpolation formulas

The geometric data below use precisely the thin-band constants. Nodes and their parent maps are induced-graph components, not an assumed abstract hierarchy.

  1. structure OAI.PlanarL1.Columns.Model.Point.RadialTree line 22
  2. def OAI.PlanarL1.Columns.Model.Point.RadialTree.Node line 40
  3. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.width_small line 44
  4. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.superlevel_antitone line 48
  5. def OAI.PlanarL1.Columns.Model.Point.RadialTree.parent line 55
  6. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.mem_parent line 58
  7. def OAI.PlanarL1.Columns.Model.Point.RadialTree.portals line 62
  8. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.parent_near line 73
  9. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.parent_separated line 90
  10. def OAI.PlanarL1.Columns.Model.Point.RadialTree.atomName line 108

    Source documentation

    Atom names use depth, portal column and type. Equal portals therefore have one name and one noise, including the root's single tentative atom.

    def atomName (k : ℕ) (v : M.Point J root) (j : Fin 3) : ℕ :=
…
  11. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.atomName_bounds line 111
  12. abbrev OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise line 120

    Source documentation

    A complete noise assignment. Bounds and independence are imposed on the actual probability space later, not assumed properties of the output.

    abbrev Noise := ℕ → Fin n → Fin 3 → ℝ
…
  13. def OAI.PlanarL1.Columns.Model.Point.RadialTree.tentative line 124
  14. def OAI.PlanarL1.Columns.Model.Point.RadialTree.upperCone line 132
  15. def OAI.PlanarL1.Columns.Model.Point.RadialTree.lowerCone line 140
  16. def OAI.PlanarL1.Columns.Model.Point.RadialTree.formula line 149

    Source documentation

    The manuscript's recursive named formulas, on the whole metric component.

    noncomputable def formula (p : M.Point J root → ℝ) (α : Noise (n := n)) :
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  17. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.tentative_names line 156
  18. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.upperCone_names line 166
  19. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.lowerCone_names line 176
  20. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.formula_name_bound line 186
  21. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.tentative_lipschitz line 203
  22. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.upperCone_lipschitz line 211
  23. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.lowerCone_lipschitz line 219
  24. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.formula_lipschitz line 227
  25. def OAI.PlanarL1.Columns.Model.Point.RadialTree.q line 236
  26. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.q_pos line 238
  27. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.q_small line 240
  28. def OAI.PlanarL1.Columns.Model.Point.RadialTree.NoiseBounds line 245
  29. def OAI.PlanarL1.Columns.Model.Point.RadialTree.InputLip line 248
  30. def OAI.PlanarL1.Columns.Model.Point.RadialTree.portalDistance line 251
  31. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.portalDistance_nonneg line 254
  32. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.tentative_bounds line 257
  33. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.cone_bounds line 286
  34. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.tentative_near line 312

    Source documentation

    With the thin-band constants, every nearby tentative value lies in the same three-delta window used in the manuscript's induction.

    lemma tentative_near {p : M.Point J root → ℝ} {α : Noise (n := n)}
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  35. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.formula_collar line 328

    Source documentation

    Exact named inheritance on the genuine entrance collar.

    lemma formula_collar (p : M.Point J root → ℝ) {α : Noise (n := n)}
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  36. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.portal_spacing line 362
  37. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.formula_near_accuracy line 370

    Source documentation

    The complete quantitative induction on the ACTUAL component hierarchy. The second bound applies to child portals; the first applies on the own layer.

    lemma formula_near_accuracy {p : M.Point J root → ℝ} {α : Noise (n := n)}
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  38. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.formula_child_accuracy line 420
  39. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.formula_layer_accuracy line 432
  40. def OAI.PlanarL1.Columns.Model.Point.RadialTree.layerDepth line 447

    Source documentation

    The unique depth of the layer assigned to a column.

    noncomputable def layerDepth (v : M.Point J root) : ℕ :=
…
  41. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.layerDepth_bounds line 450
  42. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.layerDepth_eq line 461
  43. def OAI.PlanarL1.Columns.Model.Point.RadialTree.nodeOf line 470
  44. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.mem_nodeOf line 475
  45. def OAI.PlanarL1.Columns.Model.Point.RadialTree.layerNode line 480
  46. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.mem_layerNode line 483
  47. def OAI.PlanarL1.Columns.Model.Point.RadialTree.pasted line 488

    Source documentation

    The actual pasted named output on representatives.

    noncomputable def pasted (p : M.Point J root → ℝ) (α : Noise (n := n)) (v : M.Point J root) : NamedValue :=
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  48. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.pasted_eq_of_layer line 491
  49. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.pasted_accuracy line 502
  50. def OAI.PlanarL1.Columns.Model.Point.RadialTree.radius line 507
  51. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.radius_pos line 509
  52. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.radius_bounds line 511
  53. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.common_formula line 522

    Source documentation

    One deterministic node formula, with identical atom names, represents the pasted output on the whole small ball (including every zero-distance copy). The node exists independently of the noises and the input.

    lemma common_formula (x : M.Point J root) {ρ : ℝ} (hρ : 0 ≤ ρ) (hs : ρ ≤ R.radius) :
    ∃ k : ℕ, ∃ C : R.Node k,
      (∀ z : M.Point J root, dist x z ≤ ρ →
        (k : ℝ) * R.δ ≤ dist R.base (z.withHeight R.base.height R.base.inBand)) ∧
      (∀ (p : M.Point J root → ℝ) (α : Noise (n := n)), R.NoiseBounds α →
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  54. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.formula_congr_zero line 562
  55. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.pasted_congr_zero line 577
  56. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.pasted_local_lipschitz line 584
  57. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.pasted_lipschitz line 593

    Source documentation

    Uniform local unit bounds extend globally by genuine shortest-path interpolation. No length-space axiom has been added.

    lemma pasted_lipschitz (p : M.Point J root → ℝ) {α : Noise (n := n)} (hα : R.NoiseBounds α) :
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  58. def OAI.PlanarL1.Columns.Model.Point.RadialTree.ancestor line 623

    Source documentation

    Ancestors are constructed by inclusion of actual superlevel components.

    def ancestor {k : ℕ} (C : R.Node k) (j : ℕ) (hj : j ≤ k) : R.Node j :=
…
  59. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.mem_ancestor line 626
  60. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.ancestor_self line 630
  61. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.ancestor_parent line 634
  62. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.parent_ancestor line 641
  63. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.formula_inherits line 650

    Source documentation

    A name older than a chosen depth is inherited literally all the way back through the actual hierarchy. Intercepts are not re-evaluated or renamed.

    lemma formula_inherits (p : M.Point J root → ℝ) (α : Noise (n := n))
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  64. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.formula_far_name line 676

    Source documentation

    A far node cannot output an accurate value carrying an earlier name.

    lemma formula_far_name {p : M.Point J root → ℝ} {α : Noise (n := n)}
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  65. def OAI.PlanarL1.Columns.Model.Point.RadialTree.lookback line 701

    Source documentation

    The source's lookback constant, independent of diameter and tree depth.

    noncomputable def lookback : ℕ := ⌈15 / R.ζ⌉₊ + 3
  66. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.lookback_large line 703
  67. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.ancestor_distance line 712
  68. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.far_after_lookback line 726
  69. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.formula_recent_bound line 737

    Source documentation

    Selected names of an accurate node at high radial points originate no more than lookback generations earlier. This is not an assumed depth bound.

    lemma formula_recent_bound {p : M.Point J root → ℝ} {α : Noise (n := n)}
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  70. def OAI.PlanarL1.Columns.Model.Point.RadialTree.portalAt line 767

    Source documentation

    The fixed enumeration remembers whichever portal occurrence generated a name. Duplicated portals still produce the same name.

    noncomputable def portalAt {k : ℕ} (C : R.Node k) (i : Fin 2) : M.Point J root :=
…
  71. def OAI.PlanarL1.Columns.Model.Point.RadialTree.nodeNames line 770
  72. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.nodeNames_card line 773
  73. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.nodeNames_mem line 778
  74. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.nodeNames_left line 782
  75. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.nodeNames_right line 786
  76. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.nodeNames_bounds line 790
  77. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.tentative_name_mem line 795
  78. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.upperCone_name_mem line 802
  79. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.lowerCone_name_mem line 809
  80. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.formula_name_origin line 816
  81. def OAI.PlanarL1.Columns.Model.Point.RadialTree.recentNames line 843

    Source documentation

    The deterministic, diameter-independent list at a node.

    noncomputable def recentNames {k : ℕ} (C : R.Node k) (L : ℕ) : Finset ℕ :=
…
  82. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.recentNames_card line 847
  83. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.mem_recentNames line 859
  84. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.formula_name_recent line 864
  85. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.local_name_list line 883

    Source documentation

    The source's bounded local name theorem, derived from the actual tree and from actual metric balls. Its list is fixed before input/noise sampling.

    lemma local_name_list (x : M.Point J root) {ρ : ℝ} (hρ : 0 ≤ ρ) (hs : ρ ≤ R.radius) :
    ∃ S : Finset ℕ, S.card ≤ 6 * (R.lookback + 1) ∧
      ∀ (p : M.Point J root → ℝ) (α : Noise (n := n)),
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  86. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.portalAt_height line 896
  87. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.portalAt_eq_of_column line 903
  88. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.atomName_same_depth line 914
  89. def OAI.PlanarL1.Columns.Model.Point.RadialTree.parentValue line 923

    Source documentation

    A node's parent intercept uses no noise from the current depth. The root convention below merely fills unused clamping slots with the fixed input.

    noncomputable def parentValue (p : M.Point J root → ℝ) (α : Noise (n := n)) :
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  90. def OAI.PlanarL1.Columns.Model.Point.RadialTree.atomIntercept line 928
  91. def OAI.PlanarL1.Columns.Model.Point.RadialTree.nodeAtom line 933
  92. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.tentative_eq_atom line 939
  93. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.upperCone_eq_atom line 950
  94. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.lowerCone_eq_atom line 961
  95. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.formula_eq_atom line 973

    Source documentation

    Selection is of literal named functions, not just numerical atom names.

    lemma formula_eq_atom (p : M.Point J root → ℝ) (α : Noise (n := n))
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  96. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.formula_noise_congr line 995
  97. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.parentValue_noise_congr line 1005
  98. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.atomIntercept_noise_congr line 1013
  99. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.nodeAtom_lipschitz line 1019
  100. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.nodeAtom_eq_of_name line 1040
  101. abbrev OAI.PlanarL1.Columns.Model.Point.RadialTree.ChainIndex line 1051

    Source documentation

    Explicit positions in the ancestor chain. The name, not this occurrence, is the randomized identity; opposite portal occurrences may coincide.

    abbrev ChainIndex (k : ℕ) := Fin (k + 1) × Fin 2 × Fin 3
  102. def OAI.PlanarL1.Columns.Model.Point.RadialTree.chainName line 1053
  103. def OAI.PlanarL1.Columns.Model.Point.RadialTree.chainAtom line 1056
  104. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.chainName_bounds line 1060
  105. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.chainAtom_eq_of_name line 1064
  106. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.recentNames_representation line 1084
  107. def OAI.PlanarL1.Columns.Model.Point.RadialTree.representative line 1090
  108. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.representative_name line 1094
  109. def OAI.PlanarL1.Columns.Model.Point.RadialTree.listedAtom line 1100

    Source documentation

    A fixed representation for each name, chosen from geometry before noises. Off the list the harmless zero branch makes this a total function.

    noncomputable def listedAtom (p : M.Point J root → ℝ) (α : Noise (n := n))
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  110. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.listedAtom_name line 1105
  111. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.listedAtom_lipschitz line 1113
  112. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.formula_eq_listed line 1121
  113. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.local_atom_list line 1137

    Source documentation

    The complete local list, including the actual named Lipschitz functions. At most six atoms per recent ancestor survive.

    lemma local_atom_list (x : M.Point J root) {ρ : ℝ} (hρ : 0 ≤ ρ) (hs : ρ ≤ R.radius) :
    ∃ k : ℕ, ∃ C : R.Node k,
      ∀ (p : M.Point J root → ℝ) (α : Noise (n := n)),
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  114. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.stable_names_of_no_tie line 1156

    Source documentation

    Off the finite near-tie event the selected name is constant. Direct Lipschitz comparison proves this on the entire ball without a topological selection argument, and also covers zero-distance representatives.

    lemma stable_names_of_no_tie (x : M.Point J root) {ρ : ℝ} (hρ : 0 ≤ ρ)
    {k : ℕ} (C : R.Node k) (p : M.Point J root → ℝ) (α : Noise (n := n))
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  115. def OAI.PlanarL1.Columns.Model.Point.RadialTree.replaceNoise line 1184

    Source documentation

    Replacement of exactly one current interpolation noise.

    noncomputable def replaceNoise (α : Noise (n := n)) (d : ℕ) (c : Fin n) (t : Fin 3) (r : ℝ) :
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  116. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.replaceNoise_self line 1187
  117. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.replaceNoise_other line 1190
  118. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.atomIntercept_replace line 1194
  119. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.nodeAtom_replace_self line 1202
  120. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.nodeAtom_replace_other line 1209
  121. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.chainPair_fresh line 1219

    Source documentation

    Every distinct pair on the ancestor chain has a fresh coordinate: after all other noises are fixed, their difference is affine with slope ±1 in it.

    lemma chainPair_fresh (p : M.Point J root → ℝ) {k : ℕ} (C : R.Node k)
    (u u' : ChainIndex k) (hne : R.chainName C u ≠ R.chainName C u') (v : M.Point J root) :
    ∃ d ≤ k, ∃ c : Fin n, ∃ s : Fin 3,
      ∀ α : Noise (n := n), ∃ b : ℝ,
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.ChainIndex, OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise

  122. abbrev OAI.PlanarL1.Columns.Model.Point.RadialTree.GridSample line 1277

    Source documentation

    The finite noise sample space used by the construction.

    abbrev GridSample (cap m : ℕ) := (Fin cap × Fin n × Fin 3) → Fin (m + 1)
  123. def OAI.PlanarL1.Columns.Model.Point.RadialTree.gridNoise line 1279
  124. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.gridNoise_bounds line 1282
  125. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.gridNoise_update line 1298
  126. def OAI.PlanarL1.Columns.Model.Point.RadialTree.depthCap line 1323

    Source documentation

    The radial profile has only finitely many values, one per reachable column. This explicit cap bounds every node ever used by the pasted field.

    noncomputable def depthCap : ℕ := by
…
  127. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.layerDepth_lt_cap line 1329
  128. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.depth_le_layerDepth line 1341
  129. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.chainPair_probability line 1348
  130. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.listedPair_probability line 1372
  131. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.local_name_probability line 1389

    Source documentation

    Actual finite-grid anti-concentration for a changed interpolation atom name anywhere on the closed ball. Its list and depth cap were constructed strictly from the geometry before sampling the fresh independent coordinates.

    lemma local_name_probability (p : M.Point J root → ℝ) (hp : R.InputLip p)
    (x : M.Point J root) {ρ : ℝ} (hρ : 0 ≤ ρ) (hs : ρ ≤ R.radius)
    (m : ℕ) (hm : 0 < m) :
    FiniteRandom.prob (fun ω : GridSample (n := n) R.depthCap m =>
…

    Mentions: OAI.PlanarL1.FiniteRandom.prob, OAI.PlanarL1.Columns.Model.Point.RadialTree.GridSample

  132. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.chainConstant_probability line 1465

    Source documentation

    Comparison with a fixed old field uses the current atom's own offset, not an unjustified independence assertion about its inherited intercept.

    lemma chainConstant_probability (p : M.Point J root → ℝ) {k : ℕ}
    (C : R.Node k) (u : ChainIndex k) (v : M.Point J root) (c : ℝ)
    (cap m : ℕ) (hk : k < cap) (hm : 0 < m) {t : ℝ} (ht : 0 ≤ t) :
    FiniteRandom.prob (fun ω : GridSample (n := n) cap m =>
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.ChainIndex, OAI.PlanarL1.FiniteRandom.prob, OAI.PlanarL1.Columns.Model.Point.RadialTree.GridSample

  133. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.listedConstant_probability line 1490
  134. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.listedIndependent_probability line 1502

    Source documentation

    Between independent interpolations, conditioning on the other full sample still leaves the chosen atom's fresh coordinate available.

    lemma listedIndependent_probability {Ω : Type*} [Fintype Ω] [Nonempty Ω]
    (p : M.Point J root → ℝ) {k : ℕ} (C : R.Node k) (L i : ℕ)
    (hi : i ∈ R.recentNames C L) (v : M.Point J root) (other : Ω → ℝ)
    (cap m : ℕ) (hk : k < cap) (hm : 0 < m) {t : ℝ} (ht : 0 ≤ t) :
    FiniteRandom.prob (fun ω : GridSample (n := n) cap m × Ω =>
…

    Mentions: OAI.PlanarL1.FiniteRandom.prob, OAI.PlanarL1.Columns.Model.Point.RadialTree.GridSample