OAI/Combinatorics/ContingencyTables/Transport/ContextAdjacentTransport.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.ExcessContextProfiles.rootDisplay line 22
2. lemma OAI.ContingencyTables.ExcessContextProfiles.rootDisplay_inBox line 24
3. lemma OAI.ContingencyTables.ExcessContextProfiles.rootDisplay_total line 32
4. lemma OAI.ContingencyTables.ExcessContextProfiles.rootDisplay_remove_false line 37
5. lemma OAI.ContingencyTables.ExcessContextProfiles.rootDisplay_remove_true line 43
6. lemma OAI.ContingencyTables.ExcessContextProfiles.rootDisplay_remove_two line 48
7. lemma OAI.ContingencyTables.ExcessContextProfiles.rootDisplay_oneHole_false line 53
8. lemma OAI.ContingencyTables.ExcessContextProfiles.rootDisplay_oneHole_true line 59
9. lemma OAI.ContingencyTables.ExcessContextProfiles.rootDisplay_removal line 64
10. lemma OAI.ContingencyTables.ExcessContextProfiles.widths_constant_mem line 71
11. lemma OAI.ContingencyTables.ExcessContextProfiles.prefixRaw_inBox line 79
12. lemma OAI.ContingencyTables.ExcessContextProfiles.graphEnergy_nonnegative line 87
13. theorem OAI.ContingencyTables.ExcessContextProfiles.adjacent_context_transport line 100

    Source documentation

    The actual adjacent conditional means satisfy the uniform repaired transport estimate, with precisely the box-valid leaf exchange energy.

    theorem adjacent_context_transport (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 : ℕ) (hU : 2 ≤ U) (hl0 : 1 ≤ l) (hlU : l ≤ U)
        (hB : ∀ i j, small i j=true → B i j=U)
        (hlarge : ∀ i j, small i j=false → 2 ≤ B i j)
        (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)
        (H : (Coordinates Bool (widths (fun _ : Fin n => U)) → ℕ) → ℝ)
        (hleft : 0 < eliminate (widths (fun _ : Fin n => U))
          (contextHard small B r c L _ (contextEquiv small s hs e U) (prefixRaw small s σ U))
    …

    Mentions: OAI.ContingencyTables.ResidualTables