OAI/Combinatorics/ContingencyTables/Transport/IntegerRootEstimate.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.IntegerWeightedTransport.rootCoefficients line 12
2. lemma OAI.ContingencyTables.IntegerWeightedTransport.root_potential line 15
3. theorem OAI.ContingencyTables.IntegerWeightedTransport.root_future_bound line 23

   Source documentation

   Only the off-diagonal auxiliary defects can increase the root bound; nonnegative diagonal two-hole masses contribute with the opposite sign.

   theorem root_future_bound (B : Matrix Bool Bool ℝ) (s t K c : ℝ)
       (hs : 0<s) (ht : 0<t) (hsymm : B true false = B false true)
       (haa : 0≤B false false) (hbb : 0≤B true true)
       (hab : B false true ≤ K*c) :
       -B.toBilin' (rootCoefficients s t) (rootCoefficients s t) ≤ 2*K*c/(s*t) := by
   …

   Mentions: OAI.ContingencyTables.IntegerWeightedTransport.rootCoefficients

4. theorem OAI.ContingencyTables.IntegerWeightedTransport.root_coefficient_after_repair line 43

   Source documentation

   The manuscript's last scalar step uses the auxiliary repair injection only through c_t<=max(s,t). The two positive endpoint masses are retained through every denominator.

   theorem root_coefficient_after_repair (s t c : ℝ) (U d : ℕ)
       (hs : 0<s) (ht : 0<t) (hc : c ≤ (d:ℝ)*max s t) :
       min s t * (1/s + 1/t + 2*((U:ℝ)+1)^2*c/(s*t)) ≤
         2 + 2*(d:ℝ)*((U:ℝ)+1)^2 := by
   …