OAI/MeasureTheory/FalconerCompletion/Sphere/SphereChartAmplitudeDerivativeBound.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

  1. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartAmplitudeND_derivative_bound line 20
  2. theorem OAI.GraphLiteralSupport.Attempt4FullFar.sphere_stationaryND_uniform line 40
  3. def OAI.GraphLiteralSupport.Attempt4FullFar.canonicalSphereMeasureND line 95
  4. lemma OAI.GraphLiteralSupport.Attempt4FullFar.canonicalSphereMeasureND_apply line 99
  5. lemma OAI.GraphLiteralSupport.Attempt4FullFar.canonicalSphereMeasureND_linearIsometry line 108
  6. lemma OAI.GraphLiteralSupport.Attempt4FullFar.integral_canonicalSphereMeasureND_isometry line 127
  7. lemma OAI.GraphLiteralSupport.Attempt4FullFar.integral_canonicalSphereMeasureND_neg line 131
  8. lemma OAI.GraphLiteralSupport.Attempt4FullFar.integrable_canonicalSphereMeasureND line 135
  9. lemma OAI.GraphLiteralSupport.Attempt4FullFar.norm_iteratedFDeriv_antipodal_conj line 144
  10. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereNorthCutoffND line 174
  11. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereNorthCutoffND_contDiff line 177
  12. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereNorthCutoffND_zero line 185
  13. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereNorthCutoffND_one line 191
  14. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereNorthPartND line 196
  15. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereReflectedSouthPartND line 199
  16. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereNorthPartND_contDiff line 203
  17. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereReflectedSouthPartND_contDiff line 206
  18. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereNorthPartND_support line 215
  19. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereReflectedSouthPartND_support line 221
  20. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sqrt_three_lt_two line 230
  21. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereOscillationND line 248
  22. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereOscillationND_split line 253