OAI/MeasureTheory/Falconer/Angular/CapAmplitudeDerivatives.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Derivatives of the actual cap-weighted endpoint pair

Scalar product and conjugation rules control the amplitudes and their rotated spherical chart in arbitrary ambient dimension at least three.

  1. theorem OAI.Falconer.capPairAmplitude_chart_smooth line 19
  2. theorem OAI.Falconer.capPairAmplitude_chart_derivatives line 29
  3. theorem OAI.Falconer.capPairAmplitude_cap_support line 70