OAI/Combinatorics/ContingencyTables/Counting/CompanionOracleDensity.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.CompanionOracleDensity.dimension line 15
2. def OAI.ContingencyTables.CompanionOracleDensity.index line 17
3. def OAI.ContingencyTables.CompanionOracleDensity.pull line 20
4. def OAI.ContingencyTables.CompanionOracleDensity.binWidth line 23
5. def OAI.ContingencyTables.CompanionOracleDensity.height line 25
6. def OAI.ContingencyTables.CompanionOracleDensity.D line 27
7. lemma OAI.ContingencyTables.CompanionOracleDensity.binWidth_positive line 31
8. lemma OAI.ContingencyTables.CompanionOracleDensity.height_positive line 36
9. theorem OAI.ContingencyTables.CompanionOracleDensity.D_bounds line 41
10. theorem OAI.ContingencyTables.CompanionOracleDensity.D_change line 51
11. theorem OAI.ContingencyTables.CompanionOracleDensity.D_continuous line 64
12. theorem OAI.ContingencyTables.CompanionOracleDensity.D_convex line 68
13. def OAI.ContingencyTables.CompanionOracleDensity.rho line 76
14. def OAI.ContingencyTables.CompanionOracleDensity.V line 79
15. theorem OAI.ContingencyTables.CompanionOracleDensity.rho_continuous line 82
16. theorem OAI.ContingencyTables.CompanionOracleDensity.rho_positive line 85
17. theorem OAI.ContingencyTables.CompanionOracleDensity.rho_logConcave line 88
18. theorem OAI.ContingencyTables.CompanionOracleDensity.exponent_change line 95

    Source documentation

    Every evaluator phase has base-two logarithmic Lipschitz constant at most 1/8; the bin and cut-tube comparisons now apply to the actual forest density.

    theorem exponent_change (A : Instance I J) (C a : ℝ) (hC : 0 < C)
        (ha : 0 ≤ a) (haH : a ≤ height A C) (z : View A → ℕ)
        (v w : Fin (dimension A) → ℝ) (r : ℝ) (hr : 0 ≤ r)
        (hvw : ∀ i,|v i-w i| ≤ r) :
        |(a/height A C)*D A C z v-(a/height A C)*D A C z w| ≤ r/8 := by
    …

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.height, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.CompanionOracleDensity.D

19. theorem OAI.ContingencyTables.CompanionOracleDensity.bin_comparison line 107