OAI/MeasureTheory/FalconerCompletion/Estimates/AssemblyInnerEnergyMem.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Quantitative estimates for the distance-set construction.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyInner_energy_mem line 26
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assembly_child_two_profile line 44
  3. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblySelfEnergy line 117
  4. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assembly_child_max_bound line 127
  5. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyProfileExponent line 166
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_assembly_child_max line 169
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assembly_profile_zero line 266
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assembly_profile_lower line 270
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assembly_entry_estimates line 279