IntegerRootTransport.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Root transport with the actual auxiliary defect sum

The auxiliary kernel gives one ordinary slot occupancy M+1 and all others their balances. Removing the two special coordinates leaves the special slot negative, exactly the root defects in the manuscript.

def OAI.ContingencyTables.IntegerWeightedTransport.auxiliaryKernel line 21
theorem OAI.ContingencyTables.IntegerWeightedTransport.auxiliaryKernel_nonnegative line 27
lemma OAI.ContingencyTables.IntegerWeightedTransport.weightedFuture_upper line 39
theorem OAI.ContingencyTables.IntegerWeightedTransport.correctionKernel_upper line 55
lemma OAI.ContingencyTables.IntegerWeightedTransport.removal_nonnegative line 70
lemma OAI.ContingencyTables.IntegerWeightedTransport.correction_offdiagonal_upper line 78
lemma OAI.ContingencyTables.IntegerWeightedTransport.root_balance line 88
lemma OAI.ContingencyTables.IntegerWeightedTransport.root_holePotential line 95

theorem OAI.ContingencyTables.IntegerWeightedTransport.recursive_root_potential line 104

Source documentation

The root potential estimate for the actual integer recursion. The only weight-dependent denominators are its two positive endpoint masses.

theorem recursive_root_potential (Ms : List ℕ)
    (F : (Coordinates Bool Ms → ℕ) → ℝ) (m z : Bool → ℕ) (R W : ℕ)
    (hlower : ∀ U ∈ Ms, 2 ≤ U) (hupper : ∀ U ∈ Ms, U ≤ W)
    (hF : ∀ x, 0 ≤ F x)
    (hpos : BalancedBox.PositiveSlice F (bounds m Ms) (R+Ms.sum))
    (hsig : BalancedBox.RemovalSlice F (bounds m Ms) (R+Ms.sum))
    (hz : BalancedBox.InBox m z) (htotal : (∑ i, z i)=R+1)
    (hs : 0 < oneHole (eliminate Ms F) z false)
    (ht : 0 < oneHole (eliminate Ms F) z true) :
    let s := oneHole (eliminate Ms F) z false
…

Mentions: OAI.ContingencyTables.BalancedBox.PositiveSlice, OAI.ContingencyTables.BalancedBox.RemovalSlice, OAI.ContingencyTables.BalancedBox.InBox, OAI.ContingencyTables.IntegerWeightedTransport.oneHole

theorem OAI.ContingencyTables.IntegerWeightedTransport.integer_root_graph_transport line 133

Source documentation

The softened integer transport on the actual exchange graph. All recursive coefficients and future forms have been eliminated.

theorem integer_root_graph_transport (Ms : List ℕ)
    (F H : (Coordinates Bool Ms → ℕ) → ℝ) (m z : Bool → ℕ) (R W : ℕ)
    (hlower : ∀ U ∈ Ms, 2 ≤ U) (hupper : ∀ U ∈ Ms, U ≤ W)
    (hF : ∀ x, 0 ≤ F x)
    (hpos : BalancedBox.PositiveSlice F (bounds m Ms) (R+Ms.sum))
    (hsig : BalancedBox.RemovalSlice F (bounds m Ms) (R+Ms.sum))
    (hz : BalancedBox.InBox m z) (htotal : (∑ i, z i)=R+1)
    (hs : 0 < oneHole (eliminate Ms F) z false)
    (ht : 0 < oneHole (eliminate Ms F) z true)
    (V : Finset (Coordinates Bool Ms → ℕ)) (hV : leafVertices Ms z ⊆ V) :
    let s := oneHole (eliminate Ms F) z false
…