OAI/Analysis/LipschitzHilbert/Trees/SourceDensityModel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The ordinary density is the supremum of the manuscript's actual weighted box tests. Exceeding a threshold supplies a concrete test, which can then be fed to the finite keeper construction.

  1. structure OAI.LipschitzHilbert.OrdinaryDensityTile line 12
  2. structure OAI.LipschitzHilbert.OrdinaryDensityTest line 17
  3. def OAI.LipschitzHilbert.densityAverage line 29
  4. theorem OAI.LipschitzHilbert.densityAverage_nonneg line 32
  5. theorem OAI.LipschitzHilbert.densityAverage_le line 37
  6. def OAI.LipschitzHilbert.OrdinaryDensityTile.densityValues line 48
  7. def OAI.LipschitzHilbert.OrdinaryDensityTile.density line 53
  8. theorem OAI.LipschitzHilbert.OrdinaryDensityTile.densityValues_nonempty line 57
  9. theorem OAI.LipschitzHilbert.OrdinaryDensityTile.densityValues_bddAbove line 61
  10. theorem OAI.LipschitzHilbert.OrdinaryDensityTile.density_nonneg line 70
  11. theorem OAI.LipschitzHilbert.OrdinaryDensityTile.density_le line 74
  12. theorem OAI.LipschitzHilbert.OrdinaryDensityTile.exists_test_of_lt_density line 83
  13. theorem OAI.LipschitzHilbert.OrdinaryDensityTile.density_mono line 97