OAI/Combinatorics/ContingencyTables/Rooted/TreeMarginalSignature.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The actual one-tree physical marginal before the equality limit

One physical cell is retained as its doubled Boolean pair. Every other physical cell, including small capacities zero and one, is summed at balance. The resulting positive scalar sequence has the proved raw log-concavity and finite interpolation bounds.

  1. def OAI.ContingencyTables.TreeMarginalSignature.keep line 23
  2. def OAI.ContingencyTables.TreeMarginalSignature.singleView line 25
  3. def OAI.ContingencyTables.TreeMarginalSignature.enumeration line 36
  4. def OAI.ContingencyTables.TreeMarginalSignature.cellWidth line 39
  5. def OAI.ContingencyTables.TreeMarginalSignature.otherWidths line 42
  6. def OAI.ContingencyTables.TreeMarginalSignature.coordinateEquiv line 45
  7. def OAI.ContingencyTables.TreeMarginalSignature.soft line 51
  8. def OAI.ContingencyTables.TreeMarginalSignature.exactMarginal line 58
  9. theorem OAI.ContingencyTables.TreeMarginalSignature.soft_slices line 63
  10. def OAI.ContingencyTables.TreeMarginalSignature.scalarSoft line 77
  11. def OAI.ContingencyTables.TreeMarginalSignature.scalarExact line 80
  12. theorem OAI.ContingencyTables.TreeMarginalSignature.scalar_positive line 83
  13. theorem OAI.ContingencyTables.TreeMarginalSignature.scalar_logConcave line 89
  14. theorem OAI.ContingencyTables.TreeMarginalSignature.scalar_tendsto line 98

    Source documentation

    Every retained tree mass is the finite equality-softening limit of its actual positive physical balanced sum.

    theorem scalar_tendsto (A : Instance I J) (alpha : ℝ) (t : I×J) (k : ℕ) :
    Tendsto (fun L : ℝ => scalarSoft A alpha L t k) atTop (nhds (scalarExact A alpha t k)) := by
…

    Mentions: OAI.ContingencyTables.TreeMarginalSignature.scalarSoft, OAI.ContingencyTables.TreeMarginalSignature.scalarExact