OAI/MeasureTheory/Falconer/Geometry/NormalizedSpatialFactors.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact restoration of normalized factors under the original endpoint integrals

The positive endpoint sizes are constants in every spatial, spherical and radial variable. Pulling them through the integrals preserves the original measures and gives their exact squared cost in the shell estimate.

  1. theorem OAI.Falconer.endpointTransform_const_mul line 19
  2. theorem OAI.Falconer.spatialEndpointFamily_const_mul line 31
  3. theorem OAI.Falconer.normalizedEndpoint_conj line 42
  4. theorem OAI.Falconer.spatialEndpointFamily_normalized line 48
  5. theorem OAI.Falconer.spatialSharedAmplitude_const_mul line 58
  6. theorem OAI.Falconer.spatialSharedAmplitude_normalized line 71
  7. theorem OAI.Falconer.spatial_normalized_shared_shell_le line 93