PartitionDeletionBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HadwigerCounterexample.joint_trim line 17
Source documentation
power lost on further restriction: measure removed at most error and including normalization does not hurt the lower bound.
```
theorem joint_trim (hw : IsLaw w) (Q : A→Prop) (hq : 0<pr w Q)
    (P : A×A→Prop) :
    pr (pairW w w) P - 2*pr w (fun x=>¬Q x) ≤ pr (pairW (onW w Q) (onW w Q)) P := by
…
```
Mentions: OAI.HadwigerCounterexample.IsLaw, OAI.HadwigerCounterexample.pr, OAI.HadwigerCounterexample.pairW, OAI.HadwigerCounterexample.onW
theorem OAI.HadwigerCounterexample.equity_trim line 54
Source documentation
Compose several restrictions starting from union T. P marks on prior union. T restrict -> P -> V union subset of P in T; user-given skip bound in absolute w.
```
theorem equity_trim (hw : ∀ x,0≤w x) (T V : A→Prop) (P : A→Prop)
    (hf : ∀ x,V x → T x∧P x)
    (hT : 0<pr w T) (hP : 0<pr (onW w T) P)
    {δ : ℝ} (hδ : pr w (fun x=>T x ∧ P x ∧ ¬V x) ≤ δ) :
    let W := onW (onW w T) P; let z := pr w T*pr (onW w T) P
…
```
Mentions: OAI.HadwigerCounterexample.pr, OAI.HadwigerCounterexample.onW
theorem OAI.HadwigerCounterexample.vigor_trim line 89