OAI/Analysis/LipschitzHilbert/Trees/SourceHighDensityForest.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

High ordinary density supplies concrete tests and then a finite popular forest. Every tile receives a keeper whose direction belongs to the tile's original dyadic interval.

  1. theorem OAI.LipschitzHilbert.densitySpatialBox_mono line 13
  2. theorem OAI.LipschitzHilbert.exists_high_density_forest line 19