OAI/MeasureTheory/FalconerCompletion/Sphere/SphereChartScale.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

  1. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartScaleND line 18
  2. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartND line 19
  3. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartScaleND_pos line 23
  4. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartScaleND_sq line 29
  5. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartND_norm line 34
  6. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartND_mem_sphere line 45
  7. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartND_phase line 49
  8. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartND_north line 53
  9. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartND_snd_gt_neg_one line 56
  10. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartInvND line 61
  11. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartND_left_inv line 64
  12. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartND_injOn line 72
  13. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartInvND_norm_sq line 79
  14. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartInvND_mem_ball line 95
  15. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartND_right_inv line 101
  16. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartScaleND_contDiffOn line 120
  17. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartND_contDiffOn line 129
  18. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereChartScaleND_hasStrictFDerivAt line 135
  19. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereConeND line 154
  20. def OAI.GraphLiteralSupport.Attempt4FullFar.sphereConeDerivND line 157
  21. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereConeND_hasStrictFDerivAt line 167
  22. lemma OAI.GraphLiteralSupport.Attempt4FullFar.sphereConeDerivND_apply line 188