IntegerChildVariance.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Between-child variance from raw integer transport

The no-valley bound for child masses turns adjacent transport into a bound on every pair of child means. Finite Cauchy--Schwarz and the exact weighted pair formula then bound the between-child variance.

lemma OAI.ContingencyTables.IntegerWeightedTransport.range_difference_sum line 17
lemma OAI.ContingencyTables.IntegerWeightedTransport.path_square line 23
lemma OAI.ContingencyTables.IntegerWeightedTransport.minimum_pair_coefficient line 31
lemma OAI.ContingencyTables.IntegerWeightedTransport.child_pair_path_bound line 39
lemma OAI.ContingencyTables.IntegerWeightedTransport.finite_pair_square line 85

lemma OAI.ContingencyTables.IntegerWeightedTransport.finite_weighted_variance_pair line 98

Source documentation

Exact unnormalized weighted variance pair formula.

lemma finite_weighted_variance_pair {X : Type*} [Fintype X] (w H : X → ℝ)
    (hZ : 0 < ∑ x, w x) :
    (∑ x, w x*(H x-(∑ y, w y*H y)/(∑ y, w y))^2)=
      (∑ x, ∑ y, w x*w y/(∑ k, w k)*(H x-H y)^2)/2 := by
…

theorem OAI.ContingencyTables.IntegerWeightedTransport.child_variance_bound line 111

Source documentation

The paper's between-child estimate, including zero-mass children.

theorem child_variance_bound (z H : ℕ → ℝ) (U : ℕ) (A E : ℝ)
    (hz : ∀ j ≤ U, 0 ≤ z j) (hZ : 0 < ∑ j : Fin (U+1), z j.val)
    (hA : 0 ≤ A) (hE : 0 ≤ E)
    (hminimum : ∀ a j b, a ≤ j → j ≤ b → b ≤ U → min (z a) (z b) ≤ z j)
    (hadj : ∀ j, j < U → min (z j) (z (j+1))*(H j-H (j+1))^2 ≤ A*E) :
    (∑ j : Fin (U+1), z j.val*(H j.val-
      (∑ k : Fin (U+1), z k.val*H k.val)/(∑ k : Fin (U+1), z k.val))^2) ≤
      ((U:ℝ)+1)^4*A*E := by
…