OAI/MeasureTheory/FalconerCompletion/Measures/CompletionPolynomialSubpower.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Measures and the conditional distance-set completion.

  1. lemma OAI.CurrentFalconer.AssemblyCompletion.completion_polynomial_subpower line 19
  2. def OAI.CurrentFalconer.AssemblyCompletion.completionPoly line 31
  3. def OAI.CurrentFalconer.AssemblyCompletion.completionError line 32
  4. lemma OAI.CurrentFalconer.AssemblyCompletion.completionError_nonneg line 35
  5. lemma OAI.CurrentFalconer.AssemblyCompletion.completionError_decay line 37
  6. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assembly_profile_regularization_uniform line 99
  7. abbrev OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyRetainedIndex line 174
  8. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualAssemblyClassFamily line 176
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actualAssemblyClassFamily_union line 203
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.assemblyRetainedIndex_card line 212
  11. abbrev OAI.CurrentFalconer.AssemblyCompletion.Space line 224
  12. def OAI.CurrentFalconer.AssemblyCompletion.direction line 225
  13. def OAI.CurrentFalconer.AssemblyCompletion.productFilter line 226
  14. def OAI.CurrentFalconer.AssemblyCompletion.originalDistances line 228
  15. def OAI.CurrentFalconer.AssemblyCompletion.StartingPairFilters line 231
  16. lemma OAI.CurrentFalconer.AssemblyCompletion.root_of_coordinates line 254
  17. lemma OAI.CurrentFalconer.AssemblyCompletion.productFilter_measurable line 256
  18. lemma OAI.CurrentFalconer.AssemblyCompletion.productFilter_subset line 260
  19. lemma OAI.CurrentFalconer.MonotoneShell.complex_positive_sub_variation line 272
  20. lemma OAI.CurrentFalconer.MonotoneShell.complexVariationError_positive line 286
  21. lemma OAI.CurrentFalconer.MonotoneShell.complexShellEnergy_positive line 290
  22. lemma OAI.CurrentFalconer.AssemblyCompletion.completion_of_eventual_positive_approximants line 312
  23. lemma OAI.CurrentFalconer.AssemblyCompletion.restoration_scalar_bound line 353