OAI/MeasureTheory/FalconerCompletion/Sphere/SphereAreaAeNorm2.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

  1. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sphereAreaND_ae_norm line 19
  2. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.sphereChartND_mem_image_ball line 25
  3. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.integral_sphereAreaND_eq_quadratic line 30
  4. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.norm_exp_I_mul_real line 57
  5. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.sphere_stationaryND_chart line 60