SignedTransport.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Signed transport at a leaf and at a paired split

The signed-clique inequality, local potential increment and future quadratic conservation give the counting paper's fixed-degree transport estimate. Positivity of weights at unrelated degrees is unnecessary.

def OAI.ContingencyTables.SignedTransport.cliqueEnergy line 25
Source documentation
The unordered complete exchange energy, expressed as half the ordered sum, with the manuscript's minimum-endpoint conductance.
```
noncomputable def cliqueEnergy (m W H : I → ℝ) : ℝ :=
…
```

lemma OAI.ContingencyTables.SignedTransport.star_energy_le line 30

Source documentation

A star uses each unordered edge once, so its energy is at most the complete unordered exchange energy.

lemma star_energy_le (E : I → I → ℝ)
    (hE : ∀ i j, 0 ≤ E i j) (hsymm : ∀ i j, E i j = E j i)
    (hdiag : ∀ i, E i i = 0) (hub : I) :
    ∑ i, E i hub ≤ (∑ i, ∑ j, E i j) / 2 := by
…

theorem OAI.ContingencyTables.SignedTransport.leaf_signed_transport line 49
Source documentation
A balanced signed demand on the leaf clique has energy controlled by its potential. This proves the squared inequality directly by weighted Cauchy--Schwarz and the hub construction.
```
theorem leaf_signed_transport [Nonempty I] (m W h H : I → ℝ)
    (hm : ∀ i, 0 < m i) (hW : ∀ i, 0 < W i)
    (hbalance : ∑ i, m i * h i = 0) :
    (∑ i, m i * h i * H i) ^ 2 ≤
      (∑ i, m i * h i ^ 2 / W i) * cliqueEnergy m W H := by
…
```
Mentions: OAI.ContingencyTables.SignedTransport.cliqueEnergy

theorem OAI.ContingencyTables.SignedTransport.split_signed_cost line 93

Source documentation

The exact Schur inequality for a paired binary split. The fresh coordinates have zero diagonals and positive mixed entry.

theorem split_signed_cost (B : BilinForm ℝ V)
    (hsymm : ∀ x y, B x y = B y x) (hsig : OnePositiveDirection B)
    (h ea eb : V) (u X : ℝ) (hu : 0 < u)
    (haa : B ea ea = 0) (hbb : B eb eb = 0) (hab : B ea eb = u)
    (hha : B h ea = -X) (hhb : B h eb = X) :
    2 * X ^ 2 / u ≤ -B h h := by
…

Mentions: OAI.ContingencyTables.OnePositiveDirection

theorem OAI.ContingencyTables.SignedTransport.future_form_conservation line 117

Source documentation

Child coefficients of opposite signs preserve the future quadratic form. This is the cancellation that lets each later slot be charged only its root defect mass.

theorem future_form_conservation (Ba Bb : BilinForm ℝ V)
    (haSymm : ∀ x y, Ba x y = Ba y x) (hbSymm : ∀ x y, Bb x y = Bb y x)
    (h ea eb : V) (c parent : ℝ)
    (hold : Ba h h + Bb h h = parent)
    (hcross : Ba h ea = Bb h eb) (haa : Ba ea ea = 0) (hbb : Bb eb eb = 0) :
    Ba (h + c • ea) (h + c • ea) + Bb (h - c • eb) (h - c • eb) = parent := by
…

theorem OAI.ContingencyTables.SignedTransport.split_potential_increment line 139

Source documentation

Splitting old masses and assigning the fresh-hole coefficients gives exactly the manuscript's potential increment 2 X²/(u Wt).

theorem split_potential_increment (sa sb h W : I → ℝ) (u X Wt : ℝ)
    (hu : u ≠ 0) (hWt : Wt ≠ 0) :
    ((∑ i, sa i * h i ^ 2 / W i) + u * (-X / u) ^ 2 / Wt) +
      ((∑ i, sb i * h i ^ 2 / W i) + u * (X / u) ^ 2 / Wt) =
        (∑ i, (sa i + sb i) * h i ^ 2 / W i) + 2 * X ^ 2 / (u * Wt) := by
…

theorem OAI.ContingencyTables.SignedTransport.split_child_balance line 149

Source documentation

The new-hole coefficients balance the two child signed demands.

theorem split_child_balance (sa sb h : I → ℝ) (u : ℝ) (hu : u ≠ 0)
    (hbalance : ∑ i, (sa i + sb i) * h i = 0) :
    let X := ∑ i, sa i * h i
…