OAI/MeasureTheory/FalconerCompletion/Sphere/SphereChartAmplitudeDerivativeBound2.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

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