IntegerTransportLimit.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The hard-zero limit of the actual integer transport

The final bound contains only finite marginal and auxiliary defect sums, minimum-endpoint graph energies, and the two positive endpoint masses. Thus no limit of recursively defined coefficients is needed.

lemma OAI.ContingencyTables.IntegerWeightedTransport.auxiliaryKernel_tendsto line 21
lemma OAI.ContingencyTables.IntegerWeightedTransport.removal_tendsto line 40
lemma OAI.ContingencyTables.IntegerWeightedTransport.oneHole_tendsto line 50
lemma OAI.ContingencyTables.IntegerWeightedTransport.integerGraphEnergy_tendsto line 59
lemma OAI.ContingencyTables.IntegerWeightedTransport.root_linear_eq line 69

theorem OAI.ContingencyTables.IntegerWeightedTransport.integer_root_graph_transport_limit line 76

Source documentation

The original raw integer transport survives arbitrary hard zeros. Only its two endpoint marginal masses must remain positive.

theorem integer_root_graph_transport_limit [l.NeBot] (Ms : List ℕ)
    (F : K → (Coordinates Bool Ms → ℕ) → ℝ) (f H : (Coordinates Bool Ms → ℕ) → ℝ)
    (hlim : ∀ x, 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) ∧
      BalancedBox.PositiveSlice (F t) (bounds m Ms) (R+Ms.sum) ∧
      BalancedBox.RemovalSlice (F t) (bounds m Ms) (R+Ms.sum))
    (hz : BalancedBox.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)
    (V : Finset (Coordinates Bool Ms → ℕ)) (hV : leafVertices Ms z ⊆ V) :
…

Mentions: OAI.ContingencyTables.BalancedBox.PositiveSlice, OAI.ContingencyTables.BalancedBox.RemovalSlice, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.IntegerWeightedTransport.oneHole, OAI.ContingencyTables.IntegerWeightedTransport.leafVertices