RootedTreeMarginal.lean`

9 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.

def OAI.ContingencyTables.RootedTreeMarginal.soft line 25
def OAI.ContingencyTables.RootedTreeMarginal.exactMarginal line 32
theorem OAI.ContingencyTables.RootedTreeMarginal.soft_slices line 36
def OAI.ContingencyTables.RootedTreeMarginal.scalarSoft line 50
def OAI.ContingencyTables.RootedTreeMarginal.scalarExact line 53
theorem OAI.ContingencyTables.RootedTreeMarginal.scalar_positive line 56
theorem OAI.ContingencyTables.RootedTreeMarginal.scalar_logConcave line 62
theorem OAI.ContingencyTables.RootedTreeMarginal.scalar_tendsto line 71
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) (R : RootedCompletion.Selection A.T) (alpha : ℝ) (t : I×J) (k : ℕ) :
    Tendsto (fun L : ℝ => scalarSoft A R alpha L t k) atTop (nhds (scalarExact A R alpha t k)) := by
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedTreeMarginal.scalarSoft, OAI.ContingencyTables.RootedTreeMarginal.scalarExact
theorem OAI.ContingencyTables.RootedTreeMarginal.exact_eq_fibre line 81
Source documentation
The selected-root retained-cell marginal is the actual physical fibre.
```
theorem exact_eq_fibre (A : Instance I J) (R : RootedCompletion.Selection A.T)
    (alpha : ℝ) (t : I×J) (k : Fin (cellWidth A t+1)) :
    scalarExact A R alpha t k.val=
      BalancedCellFibres.fibre (cellWidth A) (RootedPenalty.physicalWeight A R alpha) t k := by
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedTreeMarginal.scalarExact, OAI.ContingencyTables.BalancedCellFibres.fibre, OAI.ContingencyTables.RootedPenalty.physicalWeight