BFSLevels.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.PlanarRecursion.median_level line 16
Source documentation
A median BFS level, with both strict exterior sides at most half. This applies to any specified vertex subset, not just the full graph.
```
theorem median_level (U : Finset V) (depth : V → ℕ) :
    ∃ m : ℕ, 2*(U.filter (fun v => depth v < m)).card ≤ U.card ∧
      2*(U.filter (fun v => m < depth v)).card ≤ U.card := by
…
```
lemma OAI.HyperbolicObstruction.PlanarRecursion.sparse_level_in_interval line 41

theorem OAI.HyperbolicObstruction.PlanarRecursion.two_sparse_levels line 58

Source documentation

Two sparse integer levels bracketing an arbitrary median. Negative levels are permitted (their fibers are empty for graph distances), avoiding an endpoint exception at the root.

theorem two_sparse_levels (U : Finset V) (depth : V → ℤ) (m : ℤ) (a : ℕ) :
    ∃ L H : ℤ, L ≤ m ∧ m ≤ H ∧ H-L ≤ 2*a ∧
      (a+1)*(U.filter (fun v => depth v = L)).card ≤ U.card ∧
      (a+1)*(U.filter (fun v => depth v = H)).card ≤ U.card := by
…