OAI/Combinatorics/ContingencyTables/Transport/AuxiliaryRepairMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.ExcessContextProfiles.rawExcess_injective line 21
2. abbrev OAI.ContingencyTables.ExcessContextProfiles.ValidAssignments line 30
3. instance OAI.ContingencyTables.ExcessContextProfiles.validAssignmentsFintype line 33
4. lemma OAI.ContingencyTables.ExcessContextProfiles.finite_injective_sum_le line 36
5. theorem OAI.ContingencyTables.ExcessContextProfiles.auxiliary_mass_le_defect_sum line 49

   Source documentation

   Every truncated auxiliary assignment maps injectively into one actual conditional defect profile. The hard weights retain all completions.

   theorem auxiliary_mass_le_defect_sum (small : I → J → Bool) (B : I → J → ℕ)
       (r : I → ℕ) (c : J → ℕ) (L : ℕ) (s : I×J) (hs : small s.1 s.2=true)
       (σ : I×J → ℕ) (U l : ℕ) (hl0 : 1 ≤ l) (hlU : l ≤ U)
       (hB : ∀ i j, small i j=true → B i j=U)
       (hσ : ∀ a : Earlier small s, σ a.val.val ≤ U) {n : ℕ} (e : Fin n ≃ Later small s) :
       let Ms := widths (fun _ : Fin n => U)
   …

6. theorem OAI.ContingencyTables.ExcessContextProfiles.auxiliary_mass_le_adjacent line 84

   Source documentation

   Apply the completion-retaining repair injection and sum over actual later cells. Each repair enters one of the two adjacent children.

   theorem auxiliary_mass_le_adjacent (small : I → J → Bool) (B : I → J → ℕ)
       (r : I → ℕ) (c : J → ℕ) (L : ℕ) (s : I×J) (hs : small s.1 s.2=true)
       (σ : I×J → ℕ) (U l : ℕ) (hl0 : 1 ≤ l) (hlU : l ≤ U)
       (hB : ∀ i j, small i j=true → B i j=U)
       (hσ : ∀ a : Earlier small s, σ a.val.val ≤ U) {n : ℕ} (e : Fin n ≃ Later small s)
       (hcap : ∀ T : ResidualTables small r c
         (fun i => r i+rowLargeCount small i*L) (fun j => c j+columnLargeCount small j*L),
         ∀ i j, T.val.val i j ≤ B i j) :
       let Ms := widths (fun _ : Fin n => U)
   …

   Mentions: OAI.ContingencyTables.ResidualTables