BinaryFarMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite binary stopping argument for the far-family mass.

theorem OAI.LipschitzHilbert.SelectedFarFamily.binary_mass_bound line 13
theorem OAI.LipschitzHilbert.SelectedFarFamily.strip_mass_bound line 67
Source documentation
A finite far family has uniformly bounded mass in every strip whose length is at least every member's length.
```
theorem strip_mass_bound (F : SelectedFarFamily ι) (c l : ℝ) (hl : 0 < l)
    (hmax : ∀ j ∈ F.members, (F.rectangles j).long ≤ l) :
    stripMass F.rectangles F.members F.refRect c l ≤ 10*volume (F.refRect.stripSlab c l) := by
…
```
Mentions: OAI.LipschitzHilbert.SelectedFarFamily, OAI.LipschitzHilbert.stripMass