OAI/Combinatorics/ContingencyTables/Transport/IntegerTruncatedTransport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Raw transport with the literal box and degree zero extension

Excess-pair auxiliary sums may visit profiles outside the original box. Their zero extension is therefore retained in the auxiliary count and energy. Balanced endpoint masses and numerators are unchanged.

  1. lemma OAI.ContingencyTables.IntegerBoxTruncation.truncate_nonnegative line 21
  2. lemma OAI.ContingencyTables.IntegerBoxTruncation.truncate_mul line 28
  3. lemma OAI.ContingencyTables.IntegerBoxTruncation.truncate_tendsto line 34
  4. lemma OAI.ContingencyTables.IntegerBoxTruncation.eliminate_truncate line 43
  5. lemma OAI.ContingencyTables.IntegerBoxTruncation.active_removeOne_sum line 51
  6. lemma OAI.ContingencyTables.IntegerBoxTruncation.active_truncate_removal line 66
  7. lemma OAI.ContingencyTables.IntegerBoxTruncation.truncate_all_slices line 89
  8. lemma OAI.ContingencyTables.IntegerBoxTruncation.oneHole_eliminate_truncate line 101
  9. theorem OAI.ContingencyTables.IntegerWeightedTransport.integer_box_root_transport_limit line 126

    Source documentation

    Transport for the literal zero-extended weight. Its endpoint masses and weighted means are still the original physical balanced sums.

    theorem integer_box_root_transport_limit {K : Type*} {l : Filter K} [l.NeBot]
    (Ms : List ℕ) (F : K → (Coordinates Bool Ms → ℕ) → ℝ)
    (f H : (Coordinates Bool Ms → ℕ) → ℝ)
    (hlim : ∀ x, Filter.Tendsto (fun t => F t x) l (nhds (f x)))
    (m z : Bool → ℕ) (R W : ℕ)
    (hlower : ∀ U ∈ Ms, 2 ≤ U) (hupper : ∀ U ∈ Ms, U ≤ W)
    (hsoft : ∀ᶠ t in l, (∀ x, 0 ≤ F t x) ∧
      PositiveSlice (F t) (bounds m Ms) (R+Ms.sum) ∧
      RemovalSlice (F t) (bounds m Ms) (R+Ms.sum))
    (hz : InBox m z) (htotal : (∑ i, z i)=R+1)
    (hs : 0 < oneHole (eliminate Ms f) z false)
    (ht : 0 < oneHole (eliminate Ms f) z true)
…

    Mentions: OAI.ContingencyTables.IntegerWeightedTransport.oneHole