IntegerWeightedTransport.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual weighted integer pair estimate

For first-paper transport the pair display has total B+1 and capacity B, so only the interior matrices are valid. The potential identity uses exactly those matrices and the actual cumulative cross entries; it never assumes an endpoint matrix signature.

theorem OAI.ContingencyTables.IntegerWeightedTransport.weighted_pair_potential line 23

Source documentation

The D'=B+1 weighted estimate for the actual raw integer removal forms. The required balance is the zero total signed cross flow at the pair.

theorem weighted_pair_potential
    (F : ((I ⊕ Bool) → ℕ) → ℝ) (M : ℕ) (z : I → ℕ) (v : I → ℝ)
    (hsig : ∀ j, 0 < j → j < M →
      OnePositiveDirection (integerRemovalMatrix F (profile z j (M-j))).toBilin')
    (hpos : ∀ j, 0 < j → j < M → 0 < F (profile z (j-1) (M-1-j)))
    (hbalance : pairCumulative (cross F M z) v M = 0) :
    2*(∑ j ∈ Finset.range (M+1), innerWeight F M z j *
      pairCoefficient (cross F M z) (innerWeight F M z) v j ^ 2) ≤
      -(∑ j ∈ Finset.range (M+1), (j:ℝ)*((M:ℝ)-j)*
        (pairMatrix F M z j).toBilin' (old v) (old v)) := by
…

Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.pairCumulative, OAI.ContingencyTables.pairCoefficient