OAI/Combinatorics/ContingencyTables/Counting/CompanionPhysicalNormalizer.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual companion normalizer equals the full physical balanced mass

  1. lemma OAI.ContingencyTables.CompanionPhysicalNormalizer.finite_sum_congr line 16
  2. def OAI.ContingencyTables.CompanionPhysicalNormalizer.physicalMass line 25
  3. lemma OAI.ContingencyTables.CompanionPhysicalNormalizer.small_width line 30
  4. def OAI.ContingencyTables.CompanionPhysicalNormalizer.smallInterval line 38
  5. def OAI.ContingencyTables.CompanionPhysicalNormalizer.smallProfilesEquiv line 45
  6. lemma OAI.ContingencyTables.CompanionPhysicalNormalizer.small_display_eq line 50
  7. lemma OAI.ContingencyTables.CompanionPhysicalNormalizer.h_eq_physical_sum line 61
  8. lemma OAI.ContingencyTables.CompanionPhysicalNormalizer.physicalMass_eq_split line 82
  9. theorem OAI.ContingencyTables.CompanionPhysicalNormalizer.normalizer_eq_physical_mass line 108

    Source documentation

    Exact cancellation and actual small/large product partition identify the manuscript's normalizer with the physical mass used in the terminal root and tree contamination estimates.

    theorem normalizer_eq_physical_mass (A : Instance I J) (alpha : ℝ) :
    slotTotal pairs (f A alpha) ∅=physicalMass A alpha := by
…

    Mentions: OAI.ContingencyTables.CompanionPhysicalNormalizer.physicalMass