OAI/Analysis/LipschitzHilbert/Trees/SourceDensityKeepers.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Decreasing-length selection of the actual spatial and angular density tests. Keeper witnesses are disjoint even when their spatial boxes overlap.

  1. def OAI.LipschitzHilbert.densitySpatialBox line 14
  2. def OAI.LipschitzHilbert.densityTest line 18
  3. def OAI.LipschitzHilbert.densityConflict line 22
  4. theorem OAI.LipschitzHilbert.densityConflict_symm line 27
  5. theorem OAI.LipschitzHilbert.densityTest_disjoint_of_not_conflict line 32
  6. theorem OAI.LipschitzHilbert.exists_density_keepers line 42
  7. theorem OAI.LipschitzHilbert.density_keeper_area_budget line 95