OAI/Combinatorics/ContingencyTables/Transport/ObservableVariance.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.ObservableVariance.choiceVertices_plain_node line 22
2. lemma OAI.ContingencyTables.ObservableVariance.choiceVertices_defect_node line 36
3. lemma OAI.ContingencyTables.ObservableVariance.slotTotal_node_agreement line 86
4. lemma OAI.ContingencyTables.ObservableVariance.slotDefect_node_comparison line 93
5. lemma OAI.ContingencyTables.ObservableVariance.complement_global_pair_bound line 111
6. lemma OAI.ContingencyTables.ObservableVariance.complement_global_triple_bound line 124
7. lemma OAI.ContingencyTables.ObservableVariance.twoLift_scores_sink line 140

   Source documentation

   The sink is proved from the second lift's two- and three-pair inequalities; its raw signature is in the complementary coordinates.

   lemma twoLift_scores_sink (gs ps : List (Γ × Γ)) (g : Set Γ → ℝ)
       (hg : ∀ S, 0 < g S) (hsig : HasSlotSignature (complementWeight g))
       (hgs : SlotsFresh gs ∅) (hcover : pairSupport gs = Set.univ)
       (A B : Set Γ) (hnode : VarianceNode gs ps A B) (hne : ps ≠ []) :
       ∃ p ∈ ps, ∀ r ∈ ps, p ≠ r →
         slotDefect ps g A r p * slotDefect gs g ∅ p r ≤ slotTotal ps g A * slotTotal gs g ∅ := by
   …

8. theorem OAI.ContingencyTables.ObservableVariance.transport_node_variance_twoLift line 179

   Source documentation

   One transport split costs at most 1+8s q².

   theorem transport_node_variance_twoLift (ps : List (Γ × Γ)) (f H : Set Γ → ℝ)
       (A : Set Γ) (p d : Γ) (W : Γ → ℝ) (q : ℝ)
       (hf : ∀ S, 0 < f S) (hSig : HasSlotSignature f)
       (hpd : p ≠ d) (hpA : p ∉ A) (hdA : d ∉ A)
       (hps : SlotsFresh ps (A ∪ Set.range (rootEmbedding p d)))
       (hW : ∀ i, 0 < W i) (hw : ∀ p ∈ ps, W p.1 = W p.2)
       (hWp : W p = 1) (hWd : W d = 1)
       (hsink : ∀ x ∈ slotPunctures ps,
         slotTotal x.2 f (insert p (insert d A))/W x.1.1 ≤
           4*q^2*(slotTotal ps f (insert p A)+slotTotal ps f (insert d A))) :
       let sp := slotTotal ps f (insert p A)
   …

9. lemma OAI.ContingencyTables.ObservableVariance.twoLift_variance_node line 238
10. theorem OAI.ContingencyTables.ObservableVariance.twoLift_transversal_variance line 339

    Source documentation

    Actual adaptive variance bound with the paper's Cp=p(1+8p q²). No variance, sink, or transport estimate is an input to this theorem.

    theorem twoLift_transversal_variance (gs : List (Γ × Γ)) (f g H : Set Γ → ℝ)
        (w : (Γ × Γ) → (Γ × Γ) → ℝ) (q : ℝ) (hq : 0 ≤ q)
        (hf : ∀ S, 0 < f S) (hg : ∀ S, 0 < g S)
        (hsigf : HasSlotSignature f) (hsigg : HasSlotSignature (complementWeight g))
        (hgs : SlotsFresh gs ∅) (hcover : pairSupport gs = Set.univ)
        (hw : ∀ p r, 0 < w p r)
        (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) :
        slotVariance gs f H ∅ ≤ (gs.length : ℝ)*(1+8*(gs.length : ℝ)*q^2)*
          restrictedEnergy (chainEdges gs) (chainConductance gs w f) H ∅ ∅ := by
    …

11. lemma OAI.ContingencyTables.ObservableVariance.slotVariance_completeDegree line 359
12. lemma OAI.ContingencyTables.ObservableVariance.restrictedEnergy_completeDegree line 371
13. theorem OAI.ContingencyTables.ObservableVariance.validDegree_twoLift_transversal_variance line 388

    Source documentation

    Completion is eliminated from the genuine fixed-degree variance bound. Only the transport lift's addition signature and the other lift's omission signature in these encoded coordinates are assumed.

    theorem validDegree_twoLift_transversal_variance (gs : List (Γ × Γ)) (f g H : Set Γ → ℝ)
        (w : (Γ × Γ) → (Γ × Γ) → ℝ) (q : ℝ) (hq : 0 ≤ q)
        (hf : DegreePositive f gs.length) (hg : DegreePositive g gs.length)
        (hsigf : AdditionProperty f gs.length) (hsigg : OmissionProperty g gs.length)
        (hgs : SlotsFresh gs ∅) (hcover : pairSupport gs = Set.univ)
        (hw : ∀ p r, 0 < w p r)
        (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) :
        slotVariance gs f H ∅ ≤ (gs.length : ℝ)*(1+8*(gs.length : ℝ)*q^2)*
          restrictedEnergy (chainEdges gs) (chainConductance gs w f) H ∅ ∅ := by
    …