CellPruning.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Cell Pruning

theorem OAI.HadwigerCounterexample.sum_pr_tag line 14
theorem OAI.HadwigerCounterexample.pr_on_mono line 27
Source documentation
implication needed only almost surely for finite measures.
```
theorem pr_on_mono {w : Wgt A} (hw : ∀ x,0≤w x) {P Q : A→Prop}
    (h : ∀ x,w x≠0→ P x→ Q x) : pr w P ≤ pr w Q :=
…
```
Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.pr
theorem OAI.HadwigerCounterexample.sum_pr_cells line 34

theorem OAI.HadwigerCounterexample.pair_restore line 41

Source documentation

restore the full pair-event probability in a specified cell.

theorem pair_restore (u : Wgt A) (v : Wgt B) (P : A → Prop) (Q : B → Prop)
    (hP : 0 < pr u P) (hQ : 0 < pr v Q)
    (c : A × B → Prop) :
    pr (pairW u v) (fun x => P x.1 ∧ Q x.2 ∧ c x)=
      pr u P * pr v Q * pr (pairW (onW u P) (onW v Q)) c := by
…

Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.pr, OAI.HadwigerCounterexample.pairW, OAI.HadwigerCounterexample.onW

def OAI.HadwigerCounterexample.memberC line 56

theorem OAI.HadwigerCounterexample.prune_pairs line 60

Source documentation

heavy cells criterion. Loss charged to τ times opposite mass rather than τ alone (key q fixed).

theorem prune_pairs (w : Wgt A) (v : Wgt B) (hw : SubLaw w) (hv : SubLaw v)
    (P : A → Prop) (Q : B→Prop) (f : A→I) (g : B→J)
    (C : A×B→Prop) (H T : ℝ) (hH : 0≤H) (hT : 0<T)
    {L : ℝ} (hi : (Fintype.card I : ℝ) ≤ L)
    (hj : (Fintype.card J : ℝ) ≤ L)
    (h : ∀ i j,T ≤ pr w (memberC P f i) → T ≤ pr v (memberC Q g j) →
      H≤ pr (pairW (onW w (memberC P f i)) (onW v (memberC Q g j))) C) :
    H * (pr w P * pr v Q) ≤ pr (pairW w v) (fun x => P x.1 ∧ Q x.2 ∧ C x) +
      (H*T*L)*(pr w P+pr v Q) := by
…

Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.SubLaw, OAI.HadwigerCounterexample.pr, OAI.HadwigerCounterexample.memberC, OAI.HadwigerCounterexample.pairW, OAI.HadwigerCounterexample.onW