OAI/MeasureTheory/Falconer/Geometry/SurfaceTestNorm.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Continuous test norms against the actual ambient surface measure. These measure-duality lemmas match the published radial pushforward directly.

  1. def OAI.Falconer.surfaceTestNorm line 17
  2. theorem OAI.Falconer.surfaceTestNorm_test_bound line 23
  3. theorem OAI.Falconer.surfaceTestNorm_measurable_test_bound line 65
  4. theorem OAI.Falconer.surfaceTestNorm_absolutelyContinuous line 104
  5. theorem OAI.Falconer.surfaceTestNorm_bounded_density_lower line 124
  6. theorem OAI.Falconer.surfaceTestNorm_rnDeriv_eLpNorm_le line 189
  7. theorem OAI.Falconer.surfaceTestNorm_exists_Lp_density line 219