OAI/Combinatorics/ContingencyTables/Counting/CompanionRatioSamples.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompanionOracleDensity.rationalRatioObservable line 20
2. lemma OAI.ContingencyTables.CompanionOracleDensity.rationalRatioObservable_cast line 24
3. lemma OAI.ContingencyTables.CompanionOracleDensity.ratioObservable_bounds line 30
4. lemma OAI.ContingencyTables.CompanionOracleDensity.ratioMean_stationary line 36
5. lemma OAI.ContingencyTables.CompanionOracleDensity.ratioMean_bounds line 45
6. abbrev OAI.ContingencyTables.CompanionOracleDensity.RatioWords line 52
7. def OAI.ContingencyTables.CompanionOracleDensity.ratioSample line 54
8. lemma OAI.ContingencyTables.CompanionOracleDensity.ratioSample_cast line 58
9. lemma OAI.ContingencyTables.CompanionOracleDensity.ratioSample_mean line 64
10. theorem OAI.ContingencyTables.CompanionOracleDensity.ratioSample_mean_bias line 73

    Source documentation

    The actual finite walk has small expectation bias for the literal ratio of consecutive normalizers.

    theorem ratioSample_mean_bias (A : Instance I J) (C a : ℕ) (theta : ℝ)
        (hC : 0 < C) (haH : a ≤ rationalHeight A C) (htheta : 0 < theta)
        (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
        (K Q : ℕ) (hK : 1 ≤ K) (hQ : 0 < Q) (hKB : (K:ℝ) ≤ binWidth A C)
        (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
        (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
    …

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.PublishedInputs.FiniteCheeger

11. theorem OAI.ContingencyTables.CompanionOracleDensity.ratioSamples_failure line 102

    Source documentation

    Independent Boolean arrays give an explicit confidence bound around its exact annealing ratio, including the finite-walk mean bias.

    theorem ratioSamples_failure (A : Instance I J) (C a : ℕ) (theta : ℝ)
        (hC : 0 < C) (haH : a ≤ rationalHeight A C) (htheta : 0 < theta)
        (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
        (K Q N : ℕ) (hK : 1 ≤ K) (hQ : 0 < Q) (hN : 0 < N)
        (hKB : (K:ℝ) ≤ binWidth A C)
        (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
        (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
    …

    Mentions: OAI.ContingencyTables.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.PublishedInputs.FiniteCheeger