RootedOracleDraw.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Actual fixed-word corrected draws for the selected-root count

def OAI.ContingencyTables.RootedOracleDensity.stationaryIntegerLaw line 18
theorem OAI.ContingencyTables.RootedOracleDensity.stationaryIntegerLaw_cast line 24
Source documentation
The stationary bin draw followed by the actual uniform integer interval draw is precisely the corrected mass used in the exact h identity.
```
theorem stationaryIntegerLaw_cast (A : Instance I J) (R : RootedCompletion.Selection A.T) (C a : ℕ) (z : View A → ℕ)
    (K : ℕ) (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (f : FreeIndex A.small A.T A.b) :
    ((stationaryIntegerLaw A R C a z K hK hW).mass f:ℝ)=correctedMass A R C a z K (by omega) f := by
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedOracleDensity.stationaryIntegerLaw, OAI.ContingencyTables.RootedOracleDensity.correctedMass
def OAI.ContingencyTables.RootedOracleDensity.sampledIntegerLaw line 40

theorem OAI.ContingencyTables.RootedOracleDensity.sampledIntegerLaw_variation line 47

Source documentation

Both errors are accounted for once: mixing of the actual bin walk, then bounded quotient sampling inside its selected bin.

theorem sampledIntegerLaw_variation (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 h : ℕ) (hK : 1 ≤ K) (hQ : 0 < Q) (hW : 100*A.d*K ≤ A.W)
    (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

def OAI.ContingencyTables.RootedOracleDensity.flatOracleWalk line 68
lemma OAI.ContingencyTables.RootedOracleDensity.flatOracleWalk_law line 73
def OAI.ContingencyTables.RootedOracleDensity.oracleIntegerDraw line 81
theorem OAI.ContingencyTables.RootedOracleDensity.oracleIntegerDraw_law line 90
Source documentation
One fixed Boolean word drives the bin walk and then the integer draw. The bin-dependent interval length never changes the reserved word length.
```
theorem oracleIntegerDraw_law (A : Instance I J) (R : RootedCompletion.Selection A.T) (C a : ℕ) (z : View A → ℕ)
    (K : ℕ) (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W)
    (v : Grid (I := Fin (dimension A)) K) (n h : ℕ) :
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection