FirstPaperImplementedLaw.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The implemented small walk and outer rejection have the three stated errors

def OAI.ContingencyTables.SmallGraphProfiles.implementedSmallKernel line 34
def OAI.ContingencyTables.SmallGraphProfiles.implementedJointLaw line 39
theorem OAI.ContingencyTables.SmallGraphProfiles.implementedSmallKernel_variation line 49
theorem OAI.ContingencyTables.SmallGraphProfiles.implementedJointLaw_variation line 58
Source documentation
All adaptive transition errors and the independent terminal draw add before rejection; the approximate kernel needs no stationarity claim.
```
theorem implementedJointLaw_variation (x : PaperStates r c) (n : ℕ) :
    (variation (implementedJointLaw r c i₀ j₀ e b h hb a fallback x n)
      (stationaryJointLaw r c i₀ j₀):ℝ) ≤
    ((n:ℝ)+1)/(2:ℝ)^h+((stateBound r c+1:ℕ):ℝ)^(2*d)*Real.exp (-(n:ℝ)/(d:ℝ)^160) := by
…
```
Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.SmallGraphProfiles.implementedJointLaw, OAI.ContingencyTables.SmallGraphProfiles.stationaryJointLaw, OAI.ContingencyTables.SmallGraphProfiles.stateBound
theorem OAI.ContingencyTables.SmallGraphProfiles.implementedOuterLaw_variation line 82
Source documentation
This is the manuscript's three-term bound for the actual finite completion subroutine, ideal mixing, and first-success fallback.
```
theorem implementedOuterLaw_variation [Nonempty (Table r c)]
    (htotal : ∑ i,r i=∑ j,c j) (x : PaperStates r c) (n J₀ : ℕ) (z₀ : Table r c) :
    (variation (retryLaw (implementedJointLaw r c i₀ j₀ e b h hb a fallback x n)
      (stateTrial r c) z₀ J₀) (uniformLaw (α := Table r c)):ℝ) ≤
…
```
Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.SmallGraphProfiles.implementedJointLaw, OAI.ContingencyTables.SmallGraphProfiles.stateTrial