OAI/Combinatorics/ContingencyTables/Sampling/SmallContextFibres.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.SmallContextFibres.BoundedProfile line 19
2. def OAI.ContingencyTables.SmallContextFibres.naturalProfile line 22
3. lemma OAI.ContingencyTables.SmallContextFibres.naturalProfile_injective line 26
4. lemma OAI.ContingencyTables.SmallContextFibres.naturalProfile_bounded line 33
5. def OAI.ContingencyTables.SmallContextFibres.smallQ line 37
6. def OAI.ContingencyTables.SmallContextFibres.SmallPrefix line 41
7. def OAI.ContingencyTables.SmallContextFibres.BalancedProfiles line 45
8. def OAI.ContingencyTables.SmallContextFibres.DefectProfiles line 52
9. def OAI.ContingencyTables.SmallContextFibres.SmallResidualChild line 59
10. def OAI.ContingencyTables.SmallContextFibres.SmallJointDefectContext line 65
11. instance OAI.ContingencyTables.SmallContextFibres.balancedProfilesFintype line 71
12. instance OAI.ContingencyTables.SmallContextFibres.defectProfilesFintype line 75
13. instance OAI.ContingencyTables.SmallContextFibres.smallResidualChildFintype line 79
14. instance OAI.ContingencyTables.SmallContextFibres.smallJointDefectContextFintype line 86
15. theorem OAI.ContingencyTables.SmallContextFibres.smallContext_card_le line 94

    Source documentation

    The contextual injection fixes only earlier small entries.

    theorem smallContext_card_le [LinearOrder I] [LinearOrder J]
        (small : I → J → Bool) (r rbar : I → ℕ) (c cbar : J → ℕ)
        (s t : I×J) (σ : I×J → ℕ) (l : ℕ)
        (hs : small s.1 s.2=true) (ht : small t.1 t.2=true) (hst : RowMajorBefore s t) :
        Fintype.card (SmallJointDefectContext small r rbar c cbar s t σ l) ≤
          Fintype.card (SmallResidualChild small r rbar c cbar s σ
            (l-1+if t.1=s.1 then 1 else 0)) := by
    …

    Mentions: OAI.ContingencyTables.RowMajorBefore, OAI.ContingencyTables.SmallContextFibres.SmallJointDefectContext, OAI.ContingencyTables.SmallContextFibres.SmallResidualChild

16. lemma OAI.ContingencyTables.SmallContextFibres.balanced_fibre_views line 117

    Source documentation

    A balanced small profile is balanced as a full pair of views.

    lemma balanced_fibre_views {small : I → J → Bool} {B : I → J → ℕ}
        {r rbar : I → ℕ} {c cbar : J → ℕ} {z : SmallProfile small}
        (Z : CompletionFibre small B r rbar c cbar z)
        (hb : ∀ i j, smallView small z false i j=smallQ small B z i j) :
        Z.val.val.1=Z.val.val.2 := by
    …

    Mentions: OAI.ContingencyTables.SmallContextFibres.smallQ

17. lemma OAI.ContingencyTables.SmallContextFibres.defect_fibre_views line 130

    Source documentation

    The defect equation extends over the unchanged large completion.

    lemma defect_fibre_views {small : I → J → Bool} {B : I → J → ℕ}
        {r rbar : I → ℕ} {c cbar : J → ℕ} {z : SmallProfile small} {s t : I×J}
        (Z : CompletionFibre small B r rbar c cbar z)
        (hs : small s.1 s.2=true) (ht : small t.1 t.2=true)
        (hd : IsDefect (smallView small z false) (smallQ small B z) s t) :
        IsDefect Z.val.val.1 Z.val.val.2 s t := by
    …

    Mentions: OAI.ContingencyTables.IsDefect, OAI.ContingencyTables.SmallContextFibres.smallQ

18. theorem OAI.ContingencyTables.SmallContextFibres.sum_hard_eq_sigma_card line 151

    Source documentation

    Summing the literal hard weights is exactly counting the dependent union of completion fibres.

    theorem sum_hard_eq_sigma_card {S : Type*} [Fintype S]
        (small : I → J → Bool) (B : I → J → ℕ) (r : I → ℕ) (c : J → ℕ)
        (L : ℕ) (p : S → SmallProfile small)
        (hbox : ∀ s u, p s u ≤ B u.1.val.1 u.1.val.2) :
        (∑ s, hardMarginal small B r c L (p s))=
          (Fintype.card ((s : S) × CompletionFibre small B r
            (fun i => r i+rowLargeCount small i*L) c
            (fun j => c j+columnLargeCount small j*L) (p s)):ℝ) := by
    …