OAI/MeasureTheory/FalconerCompletion/Measures/RegularizationLabelCount.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Measures and the conditional distance-set completion.

  1. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.regularization_label_count line 17
  2. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.retainedClassLabels line 24
  3. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.retainedClassUnion line 31
  4. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.retainedClassLabels_count line 36
  5. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.retainedClass_mass_lower line 41
  6. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.retainedClassUnion_measurable line 46
  7. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.retainedClassUnion_mass line 50
  8. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.retainedClass_mass_sum_le_one line 64
  9. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.retainedClass_discard_mass line 71
  10. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.exists_bounded_regularization_control line 109
  11. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.regularization_fixed_count_bound line 143
  12. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.fixed_polynomial_subpower line 156
  13. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.regularization_class_count_subpower line 177
  14. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.sourceClass_occupied_comparison line 204
  15. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.sourceProfile_upper line 222
  16. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.normalizedClass_real_le line 232
  17. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.sourceProfile_frostman_lower line 243
  18. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.sourceProfile_affine_on_blocks line 278
  19. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.sourceProfile_adjusted_lipschitz line 291
  20. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.dyadic_rpow_scale line 306
  21. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.fixed_constant_absorbed line 312
  22. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.retained_label_real_mass_lower line 322
  23. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.treeCell_subset_ball line 348
  24. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.dyadic_cell_frostman_profile_bound line 355
  25. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.thin_leaf_loss_identity line 367