OAI/MeasureTheory/Falconer/Measures/PrefixMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

All-dimensional PrefixMass for regularized original measures

  1. theorem OAI.Falconer.Regularization.descendant_subset_take line 14
  2. theorem OAI.Falconer.Regularization.leafUnion_inter_prefix line 21
  3. theorem OAI.Falconer.Regularization.restriction_prefix_mass line 44
  4. theorem OAI.Falconer.Regularization.restriction_prefix_mass_real line 53
  5. theorem OAI.Falconer.Regularization.restriction_prefix_mass_bounds line 63
  6. theorem OAI.Falconer.Regularization.restriction_total_mass_real line 83
  7. theorem OAI.Falconer.Regularization.restriction_total_mass_bounds line 90