OAI/Combinatorics/ContingencyTables/Transport/IntegerPairRecursion.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.IntegerWeightedTransport.oneHole line 14
2. lemma OAI.ContingencyTables.IntegerWeightedTransport.profile_removeOne_old line 18
3. lemma OAI.ContingencyTables.IntegerWeightedTransport.profile_removeOne_a line 24
4. lemma OAI.ContingencyTables.IntegerWeightedTransport.profile_removeOne_b line 30
5. lemma OAI.ContingencyTables.IntegerWeightedTransport.old_hole_sum line 36
6. lemma OAI.ContingencyTables.IntegerWeightedTransport.child_hole_a line 47
7. lemma OAI.ContingencyTables.IntegerWeightedTransport.child_hole_b line 60
8. lemma OAI.ContingencyTables.IntegerWeightedTransport.child_old_signed_mass line 73
9. theorem OAI.ContingencyTables.IntegerWeightedTransport.integer_child_balance line 92

   Source documentation

   The cumulative coefficients balance every integer child, including zero-capacity endpoint removals.

   theorem integer_child_balance
       (F : ((I ⊕ Bool) → ℕ) → ℝ) (z : I → ℕ) (U j : ℕ) (hj : j ≤ U)
       (h : I → ℝ)
       (hpos : ∀ k, 0 < k → k < U+1 → 0 < innerWeight F (U+1) z k)
       (hbal : pairCumulative (cross F (U+1) z) h (U+1) = 0) :
       let g := pairCoefficient (cross F (U+1) z) (innerWeight F (U+1) z) h
   …

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

10. def OAI.ContingencyTables.IntegerWeightedTransport.holePotential line 110
11. lemma OAI.ContingencyTables.IntegerWeightedTransport.child_potential line 113
12. theorem OAI.ContingencyTables.IntegerWeightedTransport.integer_potential_increment line 125

    Source documentation

    The old potential partitions and the two fresh-hole contributions have identical sums, including both invalid endpoint holes.

    theorem integer_potential_increment
        (F : ((I ⊕ Bool) → ℕ) → ℝ) (z : I → ℕ) (U : ℕ)
        (h : I → ℝ) (g : ℕ → ℝ) :
        (∑ j ∈ Finset.range (U+1),
          holePotential F (profile z j (U-j)) (extendCoefficients h (g j) (g (j+1)))) =
          holePotential (marginal F U) z h +
            2 * ∑ j ∈ Finset.range (U+2), innerWeight F (U+1) z j * g j ^ 2 := by
    …

    Mentions: OAI.ContingencyTables.IntegerWeightedTransport.holePotential, OAI.ContingencyTables.IntegerWeightedTransport.extendCoefficients

13. theorem OAI.ContingencyTables.IntegerWeightedTransport.integer_split_potential_bound line 161

    Source documentation

    A split is controlled by the actual D'=U+1 integer removal forms. These are precisely the interior signatures available in the manuscript.

    theorem integer_split_potential_bound
        (F : ((I ⊕ Bool) → ℕ) → ℝ) (z : I → ℕ) (U : ℕ) (h : I → ℝ)
        (hsig : ∀ j, 0 < j → j < U+1 →
          OnePositiveDirection (integerRemovalMatrix F (profile z j (U+1-j))).toBilin')
        (hpos : ∀ j, 0 < j → j < U+1 → 0 < F (profile z (j-1) (U-j)))
        (hbalance : pairCumulative (cross F (U+1) z) h (U+1) = 0) :
        let g := pairCoefficient (cross F (U+1) z) (innerWeight F (U+1) z) h
    …

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

14. def OAI.ContingencyTables.IntegerWeightedTransport.holeLinear line 181
15. theorem OAI.ContingencyTables.IntegerWeightedTransport.integer_demand_conservation line 186

    Source documentation

    Equal resulting one-hole states cancel across adjacent branches. The numerator family G may already include the arbitrary test function H.

    theorem integer_demand_conservation
        (G : ((I ⊕ Bool) → ℕ) → ℝ) (z : I → ℕ) (U : ℕ)
        (h : I → ℝ) (g : ℕ → ℝ) :
        (∑ j ∈ Finset.range (U+1),
          holeLinear G (profile z j (U-j)) (extendCoefficients h (g j) (g (j+1)))) =
          holeLinear (marginal G U) z h := by
    …

    Mentions: OAI.ContingencyTables.IntegerWeightedTransport.holeLinear, OAI.ContingencyTables.IntegerWeightedTransport.extendCoefficients

16. theorem OAI.ContingencyTables.IntegerWeightedTransport.cumulative_eq_parent_demand line 220

    Source documentation

    Parent balance is exactly the zero cumulative cross mass required by the weighted pair theorem.

    theorem cumulative_eq_parent_demand
        (F : ((I ⊕ Bool) → ℕ) → ℝ) (z : I → ℕ) (U : ℕ) (h : I → ℝ) :
        pairCumulative (cross F (U+1) z) h (U+1) =
          holeLinear (marginal F U) z h := by
    …

    Mentions: OAI.ContingencyTables.pairCumulative, OAI.ContingencyTables.IntegerWeightedTransport.holeLinear