OAI/Combinatorics/ContingencyTables/Rooted/RootedPhysicalNormalizer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The selected-root factorial normalizer is the literal physical mass

  1. lemma OAI.ContingencyTables.RootedPhysicalNormalizer.finite_sum_congr line 15
  2. def OAI.ContingencyTables.RootedPhysicalNormalizer.physicalMass line 24
  3. lemma OAI.ContingencyTables.RootedPhysicalNormalizer.h_eq_physical_sum line 28
  4. lemma OAI.ContingencyTables.RootedPhysicalNormalizer.physicalMass_eq_split line 44
  5. lemma OAI.ContingencyTables.RootedPhysicalNormalizer.total_eq_raw_profiles line 65
  6. theorem OAI.ContingencyTables.RootedPhysicalNormalizer.normalizer_eq_physical_mass line 82

    Source documentation

    Factorial cancellation and the actual physical partition identify this selected-root normalizer with the mass used in terminal estimates.

    theorem normalizer_eq_physical_mass (A : Instance I J) (R : RootedCompletion.Selection A.T) (alpha : ℝ) :
    slotTotal pairs (RootedFactorialApplication.f A R alpha) ∅=physicalMass A R alpha := by
…

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedFactorialApplication.f, OAI.ContingencyTables.RootedPhysicalNormalizer.physicalMass