OAI/MeasureTheory/FalconerCompletion/Shells/LeafUnion.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Dyadic shells and prefix decompositions.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.leafUnion line 17
  2. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.leafUnion_measurable line 20
  3. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.leafUnion_mono line 24
  4. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.leafUnion_disjoint line 30
  5. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.measure_leafUnion line 44
  6. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.retainedLeaves line 54
  7. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.discarded_leaves_mass line 59
  8. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.classMeasure line 77
  9. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.classLeaves_disjoint line 81
  10. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.leafUnion_classes line 89
  11. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.class_mass_sum line 104
  12. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.discarded_classes_mass line 118
  13. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.normalizedClass line 137
  14. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.normalizedClass_probability line 141
  15. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.normalizedClass_apply line 152
  16. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.leafUnion_inter_prefix line 162
  17. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.restriction_prefix_mass line 184
  18. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.restriction_prefix_mass_real line 193
  19. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.restriction_prefix_mass_bounds line 202
  20. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.restriction_total_mass_real line 221
  21. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.restriction_total_mass_bounds line 227
  22. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.leafUnion_all line 242