RootedRatioSamples.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Concrete rational observations of the companion annealing ratios

lemma OAI.ContingencyTables.RootedOracleDensity.floor_step line 21
theorem OAI.ContingencyTables.RootedOracleDensity.ratioObservable_cases line 30
Source documentation
The actual phase observable takes exactly the two source values, since one annealing step changes its integer exponent by zero or one.
```
theorem ratioObservable_cases (A : Instance I J) (R : RootedCompletion.Selection A.T) (C : ℝ) (hC : 0 < C)
    (a : ℕ) (z : View A → ℕ) (hz : BalancedBox.InBox (bounds A) z)
    {K : ℕ} (hKB : (K:ℝ) ≤ binWidth A C) (v : Grid (I := Fin (dimension A)) K) :
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.BalancedBox.InBox
def OAI.ContingencyTables.RootedOracleDensity.rationalRatioObservable line 68
lemma OAI.ContingencyTables.RootedOracleDensity.rationalRatioObservable_cast line 72
lemma OAI.ContingencyTables.RootedOracleDensity.ratioObservable_bounds line 78
lemma OAI.ContingencyTables.RootedOracleDensity.ratioMean_stationary line 84
lemma OAI.ContingencyTables.RootedOracleDensity.ratioMean_bounds line 93
def OAI.ContingencyTables.RootedOracleDensity.ratioSample line 100
lemma OAI.ContingencyTables.RootedOracleDensity.ratioSample_cast line 104
lemma OAI.ContingencyTables.RootedOracleDensity.ratioSample_mean line 110

theorem OAI.ContingencyTables.RootedOracleDensity.ratioSample_mean_bias line 119

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) (R : RootedCompletion.Selection A.T) (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.RootedCompletion.Selection, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger

theorem OAI.ContingencyTables.RootedOracleDensity.ratioSamples_failure line 148

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) (R : RootedCompletion.Selection A.T) (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))
…