DensityIncrementTree.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite density increment for selecting a rich block

A low-density child of a block forces a definite increase in another child. Iterating cannot exceed a fixed upper density, so a block with no low child occurs before a bounded depth.

theorem OAI.Ostmann.density_child_increment line 19

theorem OAI.Ostmann.exists_rich_density_node line 44

Source documentation

The fixed increment forces a rich node before the density ceiling is reached. A node is an actual ordered list of child choices.

theorem exists_rich_density_node {M : ℕ} (hM : 0 < M) (H : ℕ)
    (D : List (Fin M) → ℝ) (d U : ℝ) (hd : 0 < d)
    (hroot : d ≤ D [])
    (hmean : ∀ w, w.length < H → (∑ i, D (w ++ [i])) = M * D w)
    (hupper : ∀ w, w.length ≤ H → D w ≤ U)
    (hdepth : U < d + H * (d / (4 * M))) :
    ∃ w : List (Fin M), w.length < H ∧ ∀ i, d / 2 ≤ D (w ++ [i]) := by
…