OAI/Analysis/LipschitzHilbert/Trees/SourceOrdinaryDensityForest.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The ordinary density selection, retaining its sharp witness radius and original angular cells. Empty packet sets require no dummy keeper.

  1. structure OAI.LipschitzHilbert.SourceLabeledLattice.OrdinaryDensityForest line 16
  2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_ordinary_density_forest line 39