OAI/MeasureTheory/FalconerCompletion/Sphere/ScalarCapPartition2.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.scalar_cap_partitionND line 22
  2. def OAI.GraphLiteralSupport.CurrentFalconer.fullCapGridND line 36
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.fullCapGridND_partition line 39
  4. def OAI.GraphLiteralSupport.CurrentFalconer.capGridPointND line 62
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.tensorCapND_support_dist line 65
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.tensorCapND_tsupport_dist line 79
  7. def OAI.GraphLiteralSupport.CurrentFalconer.sphereCapGridND line 88
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.sphereCapGridND_partition line 92
  9. def OAI.GraphLiteralSupport.CurrentFalconer.sphereCapCenterND line 107
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.sphereCapCenterND_norm line 110
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.sphereCapCenterND_dist line 116