HardZeroTransport.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite softened-weight transport limits

The explicit root coefficient has only the two endpoint masses in its weight-dependent denominators. All puncture masses and edge energies are finite sums of continuous functions of weights. Thus the actual proved one-hole transport survives zero internal weights when the two limiting endpoint masses are positive.

lemma OAI.ContingencyTables.HardZeroTransport.coeffDerivs_tendsto line 24
lemma OAI.ContingencyTables.HardZeroTransport.slotTotal_tendsto line 37
lemma OAI.ContingencyTables.HardZeroTransport.slotTotal_weighted_tendsto line 42
lemma OAI.ContingencyTables.HardZeroTransport.list_sum_tendsto line 48
lemma OAI.ContingencyTables.HardZeroTransport.rootCoefficient_tendsto line 55
lemma OAI.ContingencyTables.HardZeroTransport.slotGraphEnergy_tendsto line 73

theorem OAI.ContingencyTables.HardZeroTransport.transport_graph_bound_degree_limit line 87

Source documentation

The original finite transport inequality at nonnegative limiting weights. Only the two actual endpoint masses need to stay positive.

theorem transport_graph_bound_degree_limit
    [l.NeBot]
    (ps : List (Γ × Γ)) (F : K → Set Γ → ℝ) (f H : Set Γ → ℝ)
    (hlim : ∀ S, Tendsto (fun t => F t S) l (nhds (f S)))
    (A : Set Γ) (p d : Γ) (W : Γ → ℝ) (k : ℕ)
    (hsoft : ∀ᶠ t in l, DegreePositive (F t) k ∧ AdditionProperty (F t) k)
    (hdegree : A.ncard+ps.length+1=k) (hpd : p≠d) (hpA : p∉A) (hdA : d∉A)
    (hps : SlotsFresh ps (A ∪ Set.range (rootEmbedding p d)))
    (hW : ∀ i, 0 < W i) (hw : ∀ p∈ps, W p.1=W p.2)
    (hsp : 0 < slotTotal ps f (insert p A)) (hsd : 0 < slotTotal ps f (insert d A)) :
    (slotTotal ps (fun S => f S*H S) (insert p A)/slotTotal ps f (insert p A) -
      slotTotal ps (fun S => f S*H S) (insert d A)/slotTotal ps f (insert d A))^2 ≤
…

theorem OAI.ContingencyTables.HardZeroTransport.one_hole_transport_limit line 114

Source documentation

Hard-zero transport in the manuscript's original omission convention, obtained from the actual positive softened lifts and finite limits.

theorem one_hole_transport_limit
    [l.NeBot]
    (ps : List (Γ × Γ)) (F : K → Set Γ → ℝ) (f H : Set Γ → ℝ)
    (hlim : ∀ S, Tendsto (fun t => F t S) l (nhds (f S)))
    (A : Set Γ) (p d : Γ) (W : Γ → ℝ) (k : ℕ) (hk : k ≤ Fintype.card Γ)
    (hsoft : ∀ᶠ t in l, DegreePositive (F t) k ∧ OmissionProperty (F t) k)
    (hdegree : A.ncard+ps.length+1=Fintype.card Γ-k)
    (hpd : p≠d) (hpA : p∉A) (hdA : d∉A)
    (hps : SlotsFresh ps (A ∪ Set.range (rootEmbedding p d)))
    (hW : ∀ i, 0 < W i) (hw : ∀ p∈ps, W p.1=W p.2)
    (hsp : 0 < slotTotal ps (complementWeight f) (insert p A))
    (hsd : 0 < slotTotal ps (complementWeight f) (insert d A)) :
…