RootedTargetTrace.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Selected-root dyadic trace return and explicit warm cap estimates

def OAI.ContingencyTables.RootedTargetTrace.actualTrace line 21
theorem OAI.ContingencyTables.RootedTargetTrace.insideMass_eq line 29
theorem OAI.ContingencyTables.RootedTargetTrace.actualTrace_pi line 38
theorem OAI.ContingencyTables.RootedTargetTrace.insideMass_lower line 47
theorem OAI.ContingencyTables.RootedTargetTrace.warm_div_mass line 59

theorem OAI.ContingencyTables.RootedTargetTrace.warm_cap_error line 77

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) (R : RootedCompletion.Selection A.T) (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 R 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 R j S.val.val) :
    (∑ S,nu S*|(targetChain A R j hp w hw).pathExpectation (n+1) S.val
      (fun xs => phi (returnDefault (plainPredicate pairs) S xs))-
        (∑ T,(targetChain A R j hp w hw).traceMatrix (plainPredicate pairs)
…

Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.CompanionRationalUpdates.Pair

theorem OAI.ContingencyTables.RootedTargetTrace.four_warm_cap_error line 103