OAI/MeasureTheory/FalconerCompletion/Sphere/ScalarCapPartition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

  1. lemma OAI.CurrentFalconer.scalar_cap_partitionND line 20
  2. def OAI.CurrentFalconer.fullCapGridND line 34
  3. lemma OAI.CurrentFalconer.fullCapGridND_partition line 37
  4. def OAI.CurrentFalconer.capGridPointND line 60
  5. lemma OAI.CurrentFalconer.tensorCapND_support_dist line 63
  6. lemma OAI.CurrentFalconer.tensorCapND_tsupport_dist line 77
  7. def OAI.CurrentFalconer.sphereCapGridND line 86
  8. lemma OAI.CurrentFalconer.sphereCapGridND_partition line 90
  9. def OAI.CurrentFalconer.sphereCapCenterND line 105
  10. lemma OAI.CurrentFalconer.sphereCapCenterND_norm line 108
  11. lemma OAI.CurrentFalconer.sphereCapCenterND_dist line 114