OAI/Combinatorics/ContingencyTables/Transport/FinitePartitionVariance.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Exact variance decomposition for finite physical prefix partitions

  1. def OAI.ContingencyTables.FiniteExposureVariance.fibreWeight line 13
  2. lemma OAI.ContingencyTables.FiniteExposureVariance.fibreWeight_mul line 17
  3. lemma OAI.ContingencyTables.FiniteExposureVariance.fibreWeight_nonnegative line 22
  4. theorem OAI.ContingencyTables.FiniteExposureVariance.variance_partition line 31
  5. def OAI.ContingencyTables.FiniteExposureVariance.partitionVariance line 45
  6. def OAI.ContingencyTables.FiniteExposureVariance.partitionContribution line 48
  7. lemma OAI.ContingencyTables.FiniteExposureVariance.fibreWeight_pair line 53
  8. theorem OAI.ContingencyTables.FiniteExposureVariance.partition_refinement line 63

    Source documentation

    Refining a physical prefix adds exactly its between-child variance. All zero fibres are retained and contribute zero.

    theorem partition_refinement (w H : X → ℝ) (hw : ∀ x,0 ≤ w x)
    (π : X → C) (ρ : X → D) :
    partitionVariance w H π=partitionVariance w H (fun x => (π x,ρ x))+
      partitionContribution w H π ρ := by
…

    Mentions: OAI.ContingencyTables.FiniteExposureVariance.partitionVariance, OAI.ContingencyTables.FiniteExposureVariance.partitionContribution

  9. lemma OAI.ContingencyTables.FiniteExposureVariance.partitionVariance_reindex line 75
  10. lemma OAI.ContingencyTables.FiniteExposureVariance.variance_singleton_fibre line 87
  11. lemma OAI.ContingencyTables.FiniteExposureVariance.partitionVariance_identity line 97