OAI/MeasureTheory/FalconerCompletion/Measures/MeasureRealSub.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Measures and the conditional distance-set completion.

  1. lemma OAI.CurrentFalconer.MonotoneShell.measureReal_sub line 13
  2. lemma OAI.CurrentFalconer.MonotoneShell.monotone_limit_le line 18
  3. lemma OAI.CurrentFalconer.MonotoneShell.monotone_drop_mass_summable line 27
  4. lemma OAI.CurrentFalconer.MonotoneShell.monotone_tail_mass_tendsto_zero line 37