OAI/MeasureTheory/Falconer/Geometry/ScalarBallCandidates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite critical radii for maximizing scalar local density.

  1. def OAI.Falconer.scalarBallCandidates line 8
  2. def OAI.Falconer.scalarBallMass line 11
  3. theorem OAI.Falconer.scalarBallCandidates_nonempty line 14
  4. theorem OAI.Falconer.scalarBallCandidate_bounds line 19
  5. theorem OAI.Falconer.scalarBallMass_nonneg line 30
  6. theorem OAI.Falconer.scalarBallMass_at_two line 33
  7. theorem OAI.Falconer.scalarBallMass_majorized_candidate line 42