IntegerRecursiveFlow.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The actual recursive signed integer demands

Every node exposes an ordinary balanced pair, computes the cumulative coefficients from its actual remaining marginal, and retains the old coefficients. The numerator can include any test function on complete configurations. Its total leaf demand is exactly its root demand.

def OAI.ContingencyTables.IntegerWeightedTransport.recursivePotential line 22
def OAI.ContingencyTables.IntegerWeightedTransport.recursiveDemand line 32
theorem OAI.ContingencyTables.IntegerWeightedTransport.recursiveDemand_eq line 46
Source documentation
All auxiliary ordinary negative-pair divergences cancel in the actual recursion. No limit of recursive coefficients is needed.
```
theorem recursiveDemand_eq : ∀ (Ms : List ℕ) {I : Type u} [Fintype I] [DecidableEq I]
    (F G : (Coordinates I Ms → ℕ) → ℝ) (z : I → ℕ) (h : I → ℝ),
    recursiveDemand Ms F G z h = holeLinear (eliminate Ms G) z h := by
…
```
Mentions: OAI.ContingencyTables.IntegerWeightedTransport.recursiveDemand, OAI.ContingencyTables.IntegerWeightedTransport.holeLinear
theorem OAI.ContingencyTables.IntegerWeightedTransport.recursivePotential_nonnegative line 67
def OAI.ContingencyTables.IntegerWeightedTransport.recursiveEnergy line 88
lemma OAI.ContingencyTables.IntegerWeightedTransport.oneHole_nonnegative line 101
lemma OAI.ContingencyTables.IntegerWeightedTransport.oneHole_mul line 108
theorem OAI.ContingencyTables.IntegerWeightedTransport.recursiveEnergy_nonnegative line 114
def OAI.ContingencyTables.IntegerWeightedTransport.recursivelyBalanced line 138
theorem OAI.ContingencyTables.IntegerWeightedTransport.recursivelyBalanced_of_slice line 150
Source documentation
Positivity only on the valid box and degree supplies every cumulative coefficient denominator and propagates root balance to all actual leaves.
```
theorem recursivelyBalanced_of_slice : ∀ (Ms : List ℕ) {I : Type u} [Fintype I] [DecidableEq I]
    (F : (Coordinates I Ms → ℕ) → ℝ) (m z : I → ℕ) (R : ℕ) (h : I → ℝ),
    BalancedBox.PositiveSlice F (bounds m Ms) (R+Ms.sum) →
    BalancedBox.InBox m z → (∑ i, z i)=R+1 →
    holeLinear (eliminate Ms F) z h=0 → recursivelyBalanced Ms F z h := by
…
```
Mentions: OAI.ContingencyTables.BalancedBox.PositiveSlice, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.IntegerWeightedTransport.holeLinear, OAI.ContingencyTables.IntegerWeightedTransport.recursivelyBalanced
theorem OAI.ContingencyTables.IntegerWeightedTransport.recursive_signed_transport line 193
Source documentation
The full actual recursive signed demands satisfy the leaf energy comparison once their recursively proved balances are supplied.
```
theorem recursive_signed_transport : ∀ (Ms : List ℕ) {I : Type u} [Fintype I] [DecidableEq I]
    (F H : (Coordinates I Ms → ℕ) → ℝ) (z : I → ℕ) (h : I → ℝ),
    (∀ p, 0≤F p) → recursivelyBalanced Ms F z h →
    (recursiveDemand Ms F (fun p => F p*H p) z h)^2 ≤
      recursivePotential Ms F z h * recursiveEnergy Ms F H z h := by
…
```
Mentions: OAI.ContingencyTables.IntegerWeightedTransport.recursivelyBalanced, OAI.ContingencyTables.IntegerWeightedTransport.recursiveDemand, OAI.ContingencyTables.IntegerWeightedTransport.recursivePotential, OAI.ContingencyTables.IntegerWeightedTransport.recursiveEnergy
theorem OAI.ContingencyTables.IntegerWeightedTransport.recursiveEnergy_independent line 231
Source documentation
The recursively accumulated clique energy is independent of all signed coefficients; only the actual display and weight family matter.
```
theorem recursiveEnergy_independent : ∀ (Ms : List ℕ) {I : Type u} [Fintype I] [DecidableEq I]
    (F H : (Coordinates I Ms → ℕ) → ℝ) (z : I → ℕ) (h h' : I → ℝ),
    recursiveEnergy Ms F H z h = recursiveEnergy Ms F H z h' := by
…
```
Mentions: OAI.ContingencyTables.IntegerWeightedTransport.recursiveEnergy
theorem OAI.ContingencyTables.IntegerWeightedTransport.integer_recursive_transport_of_slice line 245
Source documentation
The full recursive comparison with all balances discharged from the literal softened slice, expressed solely using the root numerator.
```
theorem integer_recursive_transport_of_slice {I : Type u} [Fintype I] [DecidableEq I]
    (Ms : List ℕ) (F H : (Coordinates I Ms → ℕ) → ℝ) (m z : I → ℕ)
    (R : ℕ) (h : I → ℝ) (hF : ∀ p, 0 ≤ F p)
    (hpos : BalancedBox.PositiveSlice F (bounds m Ms) (R+Ms.sum))
    (hz : BalancedBox.InBox m z) (htotal : (∑ i, z i)=R+1)
    (hbalance : holeLinear (eliminate Ms F) z h=0) :
    (holeLinear (eliminate Ms (fun p => F p*H p)) z h)^2 ≤
      recursivePotential Ms F z h * recursiveEnergy Ms F H z h := by
…
```
Mentions: OAI.ContingencyTables.BalancedBox.PositiveSlice, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.IntegerWeightedTransport.holeLinear, OAI.ContingencyTables.IntegerWeightedTransport.recursivePotential, OAI.ContingencyTables.IntegerWeightedTransport.recursiveEnergy