OAI/Combinatorics/ContingencyTables/Transport/ExcessContextProfiles.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.ExcessContextProfiles.assemble line 19
2. lemma OAI.ContingencyTables.ExcessContextProfiles.assemble_apply line 24
3. lemma OAI.ContingencyTables.ExcessContextProfiles.assemble_prefix line 32
4. lemma OAI.ContingencyTables.ExcessContextProfiles.assemble_special line 40
5. lemma OAI.ContingencyTables.ExcessContextProfiles.assemble_later line 49
6. def OAI.ContingencyTables.ExcessContextProfiles.auxRoot line 58
7. lemma OAI.ContingencyTables.ExcessContextProfiles.auxRoot_inBox line 60
8. def OAI.ContingencyTables.ExcessContextProfiles.rawExcess line 66
9. lemma OAI.ContingencyTables.ExcessContextProfiles.bounds_constant line 71
10. lemma OAI.ContingencyTables.ExcessContextProfiles.rawExcess_bounded line 81
11. lemma OAI.ContingencyTables.ExcessContextProfiles.rawExcess_pair_total line 103

    Source documentation

    The auxiliary profile has exactly the negative current pair and one positive later pair required by the manuscript's conditional repair.

    lemma rawExcess_pair_total (small : I → J → Bool) (s : I×J) (hs : small s.1 s.2=true)
        (σ : I×J → ℕ) (U l : ℕ) (hl0 : 1 ≤ l) (hlU : l ≤ U)
        (hσ : ∀ a : Earlier small s, σ a.val.val ≤ U) {n : ℕ} (e : Fin n ≃ Later small s)
        (q : ExcessAssignments (widths (fun _ : Fin n => U))) (a : Cells small) :
        rawExcess small s hs σ U l e q (a,false)+rawExcess small s hs σ U l e q (a,true)=
          if a=⟨s,hs⟩ then U-1 else
          if a=(e (excessIndex (fun _ : Fin n => U) q)).val then U+1 else U := by
    …

    Mentions: OAI.ContingencyTables.ExcessContextProfiles.rawExcess