TraceBounds.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Trace mixing for the actual omission-lift Metropolis chain

The finite-chain constructor receives the proved positive completion. Its state weights equal the original valid-degree weights, and the transversal trace has the original normalized factorial-lift law. The trace Poincaré bound uses the proved manuscript-coordinate variance bound, followed by the existing harmonic-extension and spectral arguments.

lemma OAI.ContingencyTables.TraceBounds.completed_trace_pi line 22

theorem OAI.ContingencyTables.TraceBounds.omission_trace_poincare line 32

Source documentation

Exact inverse-gap bound 2p²Cp from the actual two-lift variance theorem.

theorem omission_trace_poincare (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) (hg : DegreePositive g gs.length)
    (hsigf : OmissionProperty f gs.length) (hsigg : AdditionProperty g gs.length)
    (q : ℝ) (hq : 0 ≤ q)
    (hgood : ∀ p ∈ gs, ∀ r ∈ gs, p ≠ r → slotTotal gs f ∅/(4*slotDefect gs f ∅ p r) ≤ w p r)
    (hagree : ∀ S, PlainState gs S → f S = g S)
    (hcompare : ∀ S, ChainState gs S → f S ≤ q*g S)
    (h : PlainIndex gs → ℝ) :
    let T := metropolisTrace gs hgs hne hcover w (completeDegree f gs.length) hw
…

lemma OAI.ContingencyTables.TraceBounds.trace_constant_le_observable line 85

theorem OAI.ContingencyTables.TraceBounds.omission_trace_relative_mixing line 101

Source documentation

Pointwise relative mixing of the actual transversal trace with Kobs. The lower bound m applies to the original normalized lift masses.

theorem omission_trace_relative_mixing (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) (hg : DegreePositive g gs.length)
    (hsigf : OmissionProperty f gs.length) (hsigg : AdditionProperty g gs.length)
    (q : ℝ) (hq : 1 ≤ q)
    (hgood : ∀ p ∈ gs, ∀ r ∈ gs, p ≠ r → slotTotal gs f ∅/(4*slotDefect gs f ∅ p r) ≤ w p r)
    (hagree : ∀ S, PlainState gs S → f S = g S)
    (hcompare : ∀ S, ChainState gs S → f S ≤ q*g S)
    (m : ℝ) (hm : 0 < m) (hmin : ∀ S : PlainIndex gs, m ≤ f S.val.val/slotTotal gs f ∅)
    (s : ℕ) (x y : PlainIndex gs) :
    let T := metropolisTrace gs hgs hne hcover w (completeDegree f gs.length) hw
…

theorem OAI.ContingencyTables.TraceBounds.omission_trace_returnCost line 137

Source documentation

A U-warm trace start costs at most 5p²U original-chain steps per return, with the exact original normalized transversal law.

theorem omission_trace_returnCost (gs : List (Γ × Γ)) (hgs : SlotsFresh gs ∅) (hne : gs ≠ [])
    (hcover : pairSupport gs = Set.univ) (w : (Γ × Γ) → (Γ × Γ) → ℝ)
    (f : Set Γ → ℝ) (hw : ∀ p r, 0 < w p r) (hf : DegreePositive f gs.length)
    (hupper : ∀ p ∈ gs, ∀ r ∈ gs, p ≠ r → w p r ≤ 4*slotTotal gs f ∅/slotDefect gs f ∅ p r)
    (U : ℝ) (hU : 0 ≤ U) (ν : PlainIndex gs → ℝ)
    (hwarm : ∀ S, ν S ≤ U*(f S.val.val/slotTotal gs f ∅)) :
    let F := completeDegree f gs.length
…