PairedComplement.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Complementation of paired conditional masses

Complementing a transversal assignment swaps its fixed inclusions and exclusions and reverses the empty/full defect labels. These are identities of the actual finite coefficient sums, used to keep the omission and addition roles of the two factorial lifts separate.

lemma OAI.ContingencyTables.PairedComplement.paired_children line 21

theorem OAI.ContingencyTables.PairedComplement.slotTotal_complement line 41

Source documentation

Exact complement identity for a residual paired choice sum.

theorem slotTotal_complement (ps : List (Γ × Γ)) (f : Set Γ → ℝ)
    (A B : Set Γ) (hAB : Disjoint A B) (hps : SlotsFresh ps (A ∪ B))
    (hcover : A ∪ B ∪ pairSupport ps = Set.univ) :
    slotTotal ps (complementWeight f) A = slotTotal ps f B := by
…

lemma OAI.ContingencyTables.PairedComplement.VarianceNode.cover line 80
lemma OAI.ContingencyTables.PairedComplement.VarianceNode.complement line 98

theorem OAI.ContingencyTables.PairedComplement.slotDefect_complement line 108

Source documentation

Complementation reverses the two distinguished defect labels.

theorem slotDefect_complement (ps : List (Γ × Γ)) (f : Set Γ → ℝ)
    (A B : Set Γ) (hAB : Disjoint A B) (hps : SlotsFresh ps (A ∪ B))
    (hcover : A ∪ B ∪ pairSupport ps = Set.univ)
    (p r : Γ × Γ) (hp : p ∈ ps) (hr : r ∈ ps) (hpr : p ≠ r) :
    slotDefect ps (complementWeight f) A p r = slotDefect ps f B r p := by
…

theorem OAI.ContingencyTables.PairedComplement.complement_defect_pair line 150

Source documentation

The complementary second lift satisfies the same oriented defect inequalities, although its raw signature role is omission rather than addition.

theorem complement_defect_pair (ps : List (Γ × Γ)) (f : Set Γ → ℝ) (k : ℕ)
    (hf : DegreePositive f k) (hsig : AdditionProperty f k)
    (A B : Set Γ) (hAB : Disjoint A B) (hps : SlotsFresh ps (A ∪ B))
    (hcover : A ∪ B ∪ pairSupport ps = Set.univ)
    (hdegree : B.ncard + ps.length = k)
    (p r : Γ × Γ) (hp : p ∈ ps) (hr : r ∈ ps) (hpr : p ≠ r) :
    4 * slotDefect ps (complementWeight f) A p r *
      slotDefect ps (complementWeight f) A r p ≤ (slotTotal ps (complementWeight f) A)^2 := by
…

theorem OAI.ContingencyTables.PairedComplement.complement_defect_triple line 165

Source documentation

Reversing all defect labels preserves the three-pair cross-entry bound.

theorem complement_defect_triple (ps : List (Γ × Γ)) (f : Set Γ → ℝ) (k : ℕ)
    (hf : DegreePositive f k) (hsig : AdditionProperty f k)
    (A B : Set Γ) (hAB : Disjoint A B) (hps : SlotsFresh ps (A ∪ B))
    (hcover : A ∪ B ∪ pairSupport ps = Set.univ)
    (hdegree : B.ncard + ps.length = k)
    (p r t : Γ × Γ) (hp : p ∈ ps) (hr : r ∈ ps) (ht : t ∈ ps)
    (hpr : p ≠ r) (hrt : r ≠ t) (hpt : p ≠ t) :
    slotDefect ps (complementWeight f) A p r * slotDefect ps (complementWeight f) A r t ≤
      slotTotal ps (complementWeight f) A * slotDefect ps (complementWeight f) A p t := by
…