OAI/Combinatorics/ContingencyTables/Dense/CheegerCoarea.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CheegerProof.level line 12
2. lemma OAI.ContingencyTables.CheegerProof.level_eq line 14
3. lemma OAI.ContingencyTables.CheegerProof.level_integrable line 19
4. lemma OAI.ContingencyTables.CheegerProof.level_integral line 25
5. lemma OAI.ContingencyTables.CheegerProof.level_abs_sub line 29
6. lemma OAI.ContingencyTables.CheegerProof.level_abs_integrable line 35
7. lemma OAI.ContingencyTables.CheegerProof.level_abs_integral line 38
8. def OAI.ContingencyTables.CheegerProof.mass line 52
9. def OAI.ContingencyTables.CheegerProof.cut line 53
10. lemma OAI.ContingencyTables.CheegerProof.mass_nonneg line 55
11. lemma OAI.ContingencyTables.CheegerProof.mass_mono line 58
12. lemma OAI.ContingencyTables.CheegerProof.mass_compl line 61
13. lemma OAI.ContingencyTables.CheegerProof.cut_indicator line 67
14. theorem OAI.ContingencyTables.CheegerProof.coarea line 93

    Source documentation

    Coarea on a function supported on a set of stationary mass at most one half.

    theorem coarea (κ : ℝ)
        (hcut : ∀ S : Finset X, κ*min (mass C S) (mass C Sᶜ) ≤ cut C S)
        (g : X → ℝ) (hg : ∀ x, 0 ≤ g x)
        (hsmall : mass C (Finset.univ.filter fun x => 0 < g x) ≤ 1/2) :
        2*κ*(∑ x, C.π x*g x) ≤ ∑ x, ∑ y, C.π x*C.P x y*|g x-g y| := by
    …

    Mentions: OAI.ContingencyTables.CheegerProof.mass, OAI.ContingencyTables.CheegerProof.cut