OAI/Geometry/RCD/Metric/DyadicDistanceSources.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A fixed dyadic family of actual squared-distance sources

  1. def OAI.RegularPointCoordinates.distanceSourceRadius line 13
  2. theorem OAI.RegularPointCoordinates.distanceSourceRadius_pos line 15
  3. theorem OAI.RegularPointCoordinates.distanceSourceRadius_succ line 18
  4. theorem OAI.RegularPointCoordinates.distanceSourceRadius_outer_le line 23
  5. theorem OAI.RegularPointCoordinates.distanceSourceRadius_four_sq line 31
  6. structure OAI.RegularPointCoordinates.DyadicDistanceSources line 45

    Source documentation

    Each source is the genuine positive Laplacian defect on four times its testing radius. The same scalar source value is used at all centers.

    structure DyadicDistanceSources (n : ℕ) (κ : ℝ) (p : X) (r0 : ℝ) where
…
  7. theorem OAI.RegularPointCoordinates.dyadic_distance_sources_of_published line 59
  8. theorem OAI.RegularPointCoordinates.DyadicDistanceSources.mass_le line 72