OAI/Analysis/LipschitzHilbert/Trees/SourceDensitySpatialCost.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The number of translated ordinary trees in a density keeper has the small power loss needed for summing the dyadic density thresholds.

  1. def OAI.LipschitzHilbert.densitySpatialCount line 10
  2. theorem OAI.LipschitzHilbert.densitySpatialCount_covers line 12
  3. theorem OAI.LipschitzHilbert.densityRadius_sq_le line 15
  4. theorem OAI.LipschitzHilbert.densitySpatialCost_le line 36