OAI/Combinatorics/ContingencyTables/Transport/IntegerTransportCoefficient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Eliminating the actual auxiliary-defect coefficient

Conditional repair bounds each auxiliary defect fibre by one endpoint child. The elementary reciprocal calculation below converts their sum into the manuscript's uniform adjacent-mean transport constant.

  1. lemma OAI.ContingencyTables.IntegerWeightedTransport.root_coefficient_bound line 14
  2. theorem OAI.ContingencyTables.IntegerWeightedTransport.repaired_root_transport line 31

    Source documentation

    The hard root transport and the proved repair domination give the uniform adjacent-mean estimate used in exposure variance.

    theorem repaired_root_transport (s t c d W E Δ : ℝ)
    (hs : 0 < s) (ht : 0 < t) (hE : 0 ≤ E)
    (hc : c ≤ d*max s t)
    (htransport : Δ^2 ≤ (1/s+1/t+2*(W+1)^2*c/(s*t))*E) :
    min s t*Δ^2 ≤ (2+2*d*(W+1)^2)*E := by
…