OAI/Analysis/LipschitzHilbert/Trees/SourceBoundaryGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Translation-independent radial masses and the literal distance to the nearest angular boundary. Eligibility is retained in every radial set.

  1. def OAI.LipschitzHilbert.AngularGrid.boundaryDistance line 14
  2. def OAI.LipschitzHilbert.AngularGrid.nearbyEligibleTops line 18
  3. def OAI.LipschitzHilbert.AngularGrid.nearbyEligibleMass line 22
  4. theorem OAI.LipschitzHilbert.AngularGrid.boundaryDistance_nonneg line 26
  5. theorem OAI.LipschitzHilbert.AngularGrid.boundaryDistance_le_half line 31
  6. theorem OAI.LipschitzHilbert.AngularGrid.index_eq_of_mem_cell line 38
  7. theorem OAI.LipschitzHilbert.AngularGrid.index_eq_of_dist_lt_boundary line 57
  8. theorem OAI.LipschitzHilbert.AngularGrid.nearbyEligibleTops_subset_cell line 65
  9. theorem OAI.LipschitzHilbert.AngularGrid.nearbyEligibleTops_mono line 75
  10. theorem OAI.LipschitzHilbert.AngularGrid.outsideNearTops_subset_radial line 84