OAI/MeasureTheory/FalconerCompletion/Measures/AssemblyPositiveEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Measures and the conditional distance-set completion.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyPositiveEnergy line 20
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyEnergy_integrable line 23
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assembly_norm_weighted_sum_sq_le line 27
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assembly_charFun_weighted_sum line 43
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyPositiveEnergy_weighted_sum line 54
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyPositiveEnergy_sum line 76
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyEnergy_two_sided line 105