MonotoneMeasureMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Positive increments of decreasing finite measures

This is the measure-theoretic telescoping step of asm:monotone-shell. The total variation of each positive decrement is its mass, and those masses are summable. No quantitative convergence rate is introduced.

theorem OAI.Falconer.antitone_measure_sum_decrements line 24
Source documentation
The finite telescoping identity is an equality of measures, not just of masses. Each difference is the positive measure difference.
```
theorem antitone_measure_sum_decrements (α : ℕ → Measure X)
    [∀ n, IsFiniteMeasure (α n)] (hα : Antitone α) (N : ℕ) :
    (∑ n ∈ Finset.range N, (α n - α (n + 1))) + α N = α 0 := by
…
```
theorem OAI.Falconer.summable_antitone_measure_decrements line 36
Source documentation
Monotonicity and finite initial mass supply precisely the summability needed for the variation correction in the shell argument.
```
theorem summable_antitone_measure_decrements (α : ℕ → Measure X)
    [∀ n, IsFiniteMeasure (α n)] (hα : Antitone α) :
    Summable (fun n => (α n - α (n + 1)).real univ) := by
…
```