OAI/MeasureTheory/FalconerCompletion/Sphere/SphereMeasure.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

  1. def OAI.Attempt4FullFar.canonicalSphereMeasureND line 15
  2. lemma OAI.Attempt4FullFar.canonicalSphereMeasureND_apply line 19
  3. lemma OAI.Attempt4FullFar.canonicalSphereMeasureND_linearIsometry line 28
  4. lemma OAI.Attempt4FullFar.integral_canonicalSphereMeasureND_isometry line 47
  5. lemma OAI.Attempt4FullFar.integral_canonicalSphereMeasureND_neg line 51
  6. lemma OAI.Attempt4FullFar.integrable_canonicalSphereMeasureND line 55
  7. instance OAI.Attempt4FullFar.canonicalSphereMeasureND_finite line 75
  8. lemma OAI.Attempt4FullFar.canonicalSphereMeasureND_ae_norm line 79
  9. def OAI.Attempt4FullFar.skewFlowND line 86
  10. lemma OAI.Attempt4FullFar.skewFlowND_apply line 94
  11. lemma OAI.Attempt4FullFar.skewFlowND_zero line 98
  12. lemma OAI.Attempt4FullFar.skewFlowND_hasDerivAt line 102
  13. theorem OAI.Attempt4FullFar.integral_sphere_skew_derivative_zero line 108
  14. def OAI.Attempt4FullFar.angularDerivativeND line 165
  15. lemma OAI.Attempt4FullFar.angularDerivativeND_contDiff line 169
  16. lemma OAI.Attempt4FullFar.angularDerivativeND_mul line 174
  17. lemma OAI.Attempt4FullFar.sphere_angular_integration_by_parts line 183