OAI/Combinatorics/ContingencyTables/Transport/FiniteRepairVariance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite variance extension along completion-retaining repairs

  1. lemma OAI.ContingencyTables.FiniteExposureVariance.variance_le_center line 15
  2. lemma OAI.ContingencyTables.FiniteExposureVariance.square_repair_split line 25
  3. lemma OAI.ContingencyTables.FiniteExposureVariance.repair_center_mass line 29
  4. theorem OAI.ContingencyTables.FiniteExposureVariance.variance_sum_repair line 47

    Source documentation

    The actual typewise repair injection extends a transversal variance bound to all states, charging each defect-to-repair difference once.

    theorem variance_sum_repair {B D T : Type*} [Fintype B] [Fintype D] [Fintype T]
    (w : B → ℝ) (v : D → ℝ) (H : B → ℝ) (K : D → ℝ)
    (R : D → B) (label : D → T) (hw : ∀ b,0 ≤ w b) (hv : ∀ d,0 ≤ v d)
    (hdom : ∀ d,v d ≤ w (R d)) (hinj : Function.Injective (fun d => (label d,R d))) :
    variance (Sum.elim w v) (Sum.elim H K) ≤
      (1+2*(Fintype.card T:ℝ))*variance w H+2*∑ d,v d*(K d-H (R d))^2 := by
…

    Mentions: OAI.ContingencyTables.FiniteExposureVariance.variance