ObservableBounds.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Observable and trace bounds on the actual valid-degree chain

Positive completion is used only to instantiate the existing finite-chain constructor. All its state weights, conductances, and conditional projections are proved equal to the original valid-degree quantities.

def OAI.ContingencyTables.ObservableBounds.observableConstant line 21
Source documentation
The manuscript's observable constant.
```
def observableConstant (p q : ℝ) : ℝ :=
…
```
lemma OAI.ContingencyTables.ObservableBounds.observableConstant_lower line 24

theorem OAI.ContingencyTables.ObservableBounds.observable_poincare_sharp line 39

Source documentation

A sharper direct consequence of the existing proved projection bound. The finite defect-type count is retained until its last numerical estimate.

theorem observable_poincare_sharp (gs : List (Γ × Γ)) (hgs : SlotsFresh gs ∅) (hne : gs ≠ [])
    (hcover : pairSupport gs = Set.univ) (w : (Γ × Γ) → (Γ × Γ) → ℝ)
    (hw : ∀ p r, 0 < w p r) (f H : Set Γ → ℝ) (hf : ∀ S, 0 < f S)
    (hsig : HasSlotSignature f)
    (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) :
    chainVariance gs w f (observableProjection gs f H) ≤
      338*(gs.length:ℝ)^5*chainDirichlet gs w f H := by
…

lemma OAI.ContingencyTables.ObservableBounds.slotDefect_completion_mul line 79
lemma OAI.ContingencyTables.ObservableBounds.observableProjection_completion line 94
lemma OAI.ContingencyTables.ObservableBounds.chainTotal_completion line 105
lemma OAI.ContingencyTables.ObservableBounds.chainMean_completion line 114
lemma OAI.ContingencyTables.ObservableBounds.chainVariance_completion line 125
lemma OAI.ContingencyTables.ObservableBounds.chainDirichlet_completion line 137

theorem OAI.ContingencyTables.ObservableBounds.validDegree_observable_poincare line 146

Source documentation

Observable Poincaré on the original valid-degree weights, with the exact manuscript constant. Off-degree positivity is absent from its assumptions.

theorem validDegree_observable_poincare (gs : List (Γ × Γ)) (hgs : SlotsFresh gs ∅) (hne : gs ≠ [])
    (hcover : pairSupport gs = Set.univ) (w : (Γ × Γ) → (Γ × Γ) → ℝ)
    (hw : ∀ p r, 0 < w p r) (f H : Set Γ → ℝ)
    (hf : DegreePositive f gs.length) (hsig : AdditionProperty f gs.length)
    (q : ℝ) (hq : 1 ≤ q)
    (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) :
    chainVariance gs w f (observableProjection gs f H) ≤
      observableConstant gs.length q * chainDirichlet gs w f H := by
…

Mentions: OAI.ContingencyTables.ObservableBounds.observableConstant