ObservableTrajectory.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Warm trajectory averages of the paper's class observables

The dual estimate is derived from the proved original-coordinate observable Poincaré inequality. The existing finite-chain covariance and warm moment lemmas then give the paper's 2UKobs Var/N mean-square bound. Completion is absent from the observable mean, variance, and warm-start law.

theorem OAI.ContingencyTables.ObservableTrajectory.omission_chain_dual line 22

Source documentation

Dual observable bound for the genuine omission-lift chain.

theorem omission_chain_dual (gs : List (Γ × Γ)) (hgs : SlotsFresh gs ∅) (hne : gs ≠ [])
    (hcover : pairSupport gs = Set.univ) (w : (Γ × Γ) → (Γ × Γ) → ℝ)
    (f G : Set Γ → ℝ) (hw : ∀ p r, 0 < w p r)
    (hf : DegreePositive f gs.length) (hsig : OmissionProperty f gs.length)
    (q : ℝ) (hq : 1 ≤ q) (hG : ClassObservable gs G)
    (hlower : ∀ p ∈ gs, ∀ r ∈ gs, p ≠ r → slotTotal gs f ∅/(4*slotDefect gs f ∅ p r) ≤ w p r)
    (hupper : ∀ p ∈ gs, ∀ r ∈ gs, p ≠ r → w p r ≤ 4*slotTotal gs f ∅/slotDefect gs f ∅ p r)
    (H : ChainIndex gs → ℝ) :
    let C := metropolisChain gs hgs hne hcover w (completeDegree f gs.length) hw
…

theorem OAI.ContingencyTables.ObservableTrajectory.omission_chain_timeAverage line 81

Source documentation

The manuscript's trajectory mean-square estimate, using its original conditional class observable, stationary variance, and warm-start density.

theorem omission_chain_timeAverage (gs : List (Γ × Γ)) (hgs : SlotsFresh gs ∅) (hne : gs ≠ [])
    (hcover : pairSupport gs = Set.univ) (w : (Γ × Γ) → (Γ × Γ) → ℝ)
    (f G : Set Γ → ℝ) (hw : ∀ p r, 0 < w p r)
    (hf : DegreePositive f gs.length) (hsig : OmissionProperty f gs.length)
    (q : ℝ) (hq : 1 ≤ q) (hG : ClassObservable gs G)
    (hlower : ∀ p ∈ gs, ∀ r ∈ gs, p ≠ r → slotTotal gs f ∅/(4*slotDefect gs f ∅ p r) ≤ w p r)
    (hupper : ∀ p ∈ gs, ∀ r ∈ gs, p ≠ r → w p r ≤ 4*slotTotal gs f ∅/slotDefect gs f ∅ p r)
    (U : ℝ) (hU : 0 ≤ U) (ν : ChainIndex gs → ℝ)
    (hwarm : ∀ S, ν S ≤ U*chainWeight gs w f S.val/chainTotal gs w f)
    (N : ℕ) (hN : 0 < N) :
    let C := metropolisChain gs hgs hne hcover w (completeDegree f gs.length) hw
…