OAI/MeasureTheory/FalconerCompletion/Sphere/SphereMeasureAeNorm.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Canonical spherical measures and differential identities.

  1. lemma OAI.CurrentFalconer.TreeND.canonicalSphereMeasureND_ae_norm line 18
  2. def OAI.CurrentFalconer.TreeND.cellCapEnergy line 25
  3. def OAI.CurrentFalconer.TreeND.ImposesParallelTest line 31
  4. def OAI.CurrentFalconer.TreeND.eligibleCells line 37
  5. lemma OAI.CurrentFalconer.TreeND.cellCapEnergy_pos_witness line 42
  6. lemma OAI.CurrentFalconer.TreeND.cellCapEnergy_pos_occupied line 58
  7. theorem OAI.CurrentFalconer.TreeND.eligibleCells_tested line 67