OAI/MeasureTheory/FalconerCompletion/Shells/RegularizationLeaves.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Dyadic shells and prefix decompositions.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.regularizationLeaves line 19
  2. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.regularizationLabel line 22
  3. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.sourceProfile line 26
  4. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.sourceClass line 29
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.regularizationLeaves_subset line 33
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.regularization_weight_bounds line 36
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.normalizedClass_real line 46
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.sourceClass_probability line 54
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.sourceClass_grid_comparison line 77
  10. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.normalizedClass_occupied_prefix line 101