OAI/Analysis/LipschitzHilbert/Trees/SourceDensityPowerForest.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

At the manuscript's polynomial density threshold, the selected actual witnesses obey the polynomial radius, precision and area hypotheses used by concentration. The threshold is fixed before all finite data.

  1. theorem OAI.LipschitzHilbert.density_dyadic_length_order line 14
  2. theorem OAI.LipschitzHilbert.densitySpatialBox_radius_le line 21
  3. theorem OAI.LipschitzHilbert.exists_power_density_forest line 27