CompanionTargetTrace.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Warm cap bounds for the actual dyadic companion trace

Holding slowdown leaves the stationary law unchanged. The good multiplier bound therefore gives the same polynomial mean-return and capped-return bounds as the original Metropolis chain.

def OAI.ContingencyTables.CompanionTargetTrace.actualTrace line 23
theorem OAI.ContingencyTables.CompanionTargetTrace.insideMass_eq line 31
theorem OAI.ContingencyTables.CompanionTargetTrace.actualTrace_pi line 40
theorem OAI.ContingencyTables.CompanionTargetTrace.insideMass_lower line 49
theorem OAI.ContingencyTables.CompanionTargetTrace.warm_div_mass line 61

theorem OAI.ContingencyTables.CompanionTargetTrace.warm_cap_error line 79

Source documentation

Four-warm is the incoming bound after an adjacent-parameter restart. More generally this holds for any nonnegative warmness coefficient.

theorem warm_cap_error (A : Instance I J) (j : ℕ) (hp : 0<Fintype.card (Labels A))
    (w : CompanionRationalUpdates.Pair A → CompanionRationalUpdates.Pair A → ℚ)
    (hw : ∀ p q,0<w p q)
    (hgood : GoodMultipliers pairs (weight A j) (fun p q => (w p q:ℝ)))
    (phi : PlainIndex (pairs : List (CompanionRationalUpdates.Pair A)) → ℝ)
    (hphi : ∀ S,0≤phi S ∧ phi S≤1) (n : ℕ) (hn : 0<n)
    (nu : PlainIndex (pairs : List (CompanionRationalUpdates.Pair A)) → ℝ)
    (hnu : ∀ S,0≤nu S) (U : ℝ) (hU : 0≤U)
    (hwarm : ∀ S,nu S≤U*law A j S.val.val) :
    (∑ S,nu S*|(targetChain A j hp w hw).pathExpectation (n+1) S.val
      (fun xs => phi (returnDefault (plainPredicate pairs) S xs))-
        (∑ T,(targetChain A j hp w hw).traceMatrix (plainPredicate pairs)
…

Mentions: OAI.ContingencyTables.CompanionRationalUpdates.Pair

def OAI.ContingencyTables.CompanionTargetTrace.capSteps line 105
theorem OAI.ContingencyTables.CompanionTargetTrace.four_warm_cap_error line 108