IntegerLeafTransport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ContingencyTables.IntegerWeightedTransport.raw_leaf_transport line 17
Source documentation
The leaf-clique estimate for raw masses. Invalid removals may have zero mass; no artificial positive weight is assigned to those vertices.
```
theorem raw_leaf_transport (m h H : I → ℝ) (hm : ∀ i, 0 ≤ m i)
    (hbalance : ∑ i, m i * h i = 0) :
    (∑ i, m i * h i * H i) ^ 2 ≤
      (∑ i, m i * h i ^ 2) * cliqueEnergy m (fun _ => 1) H := by
…
```
theorem OAI.ContingencyTables.IntegerWeightedTransport.integer_leaf_transport line 49
Source documentation
Instantiation at the actual one-removal weights of an integer display.
```
theorem integer_leaf_transport (F : (I → ℕ) → ℝ) (z : I → ℕ)
    (h H : I → ℝ) (hF : ∀ p, 0 ≤ F p)
    (hbalance : ∑ i, oneHole F z i * h i = 0) :
    (∑ i, oneHole F z i * h i * H i)^2 ≤
      holePotential F z h * cliqueEnergy (oneHole F z) (fun _ => 1) H := by
…
```
Mentions: OAI.ContingencyTables.IntegerWeightedTransport.oneHole, OAI.ContingencyTables.IntegerWeightedTransport.holePotential