ForestScaledIdentification.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Integer free assignments use the original scaled affine tree values

lemma OAI.ContingencyTables.ForestScaledPenalty.free_coefficient_sum line 16
def OAI.ContingencyTables.ForestScaledPenalty.integerCube line 31

theorem OAI.ContingencyTables.ForestScaledPenalty.scaledTree_integer line 36

Source documentation

The scaled affine value at each original integer free assignment is exactly the manuscript's solved tree value divided by its capacity.

theorem scaledTree_integer (A : Instance I J) (B : ℝ) (hB : 0 < B)
    (x q : I → J → ℤ) (f : FreeIndex A.small A.T A.b) (t : TreeCell A.T) :
    scaledTree A B x q (integerCube A B f) t=
      (solved A.small A.T A.r A.c x q
        (fun i j => (freeTable A.small A.T A.b f i j:ℤ)) t.val.1 t.val.2:ℝ)/(A.b t.val.1 t.val.2:ℝ) := by
…

Mentions: OAI.ContingencyTables.ForestScaledPenalty.scaledTree, OAI.ContingencyTables.ForestScaledPenalty.integerCube

lemma OAI.ContingencyTables.ForestScaledPenalty.intervalCost_div line 62
theorem OAI.ContingencyTables.ForestScaledPenalty.rootConstant_eq_assignment line 72
Source documentation
The root residual in the continuous display is the original root residual on every integer free assignment; it is independent of those free values by the proved component-cut cancellation.
```
theorem rootConstant_eq_assignment (A : Instance I J) (x q free : I → J → ℤ) :
    rootConstant A x q=
      ∑ a,if ForestPenaltyApplication.rootFlag A.T a then
        |(signedResidual A.small A.T A.r A.c x q free a:ℝ)| else 0 := by
…
```
Mentions: OAI.ContingencyTables.ForestScaledPenalty.rootConstant, OAI.ContingencyTables.ForestPenaltyApplication.rootFlag
lemma OAI.ContingencyTables.ForestScaledPenalty.tree_sum_eq line 85
theorem OAI.ContingencyTables.ForestScaledPenalty.penalty_at_integer line 97
Source documentation
Thus the continuous display agrees term for term with the actual root/tree penalty in the original finite definition of h_j.
```
theorem penalty_at_integer (A : Instance I J) (C B : ℝ) (hB : 0 < B)
    (z : View A → ℕ) (f : FreeIndex A.small A.T A.b) :
    penalty A C B (fun i j => (ForestCountIdentification.smallX A.small z i j:ℤ))
      (fun i j => ((A.b i j-ForestCountIdentification.smallY A.small z i j:ℕ):ℤ))
      (integerCube A B f)=C*ForestPenaltyBound.penalty A z f := by
…
```
Mentions: OAI.ContingencyTables.ForestScaledPenalty.penalty, OAI.ContingencyTables.ForestCountIdentification.smallX, OAI.ContingencyTables.ForestCountIdentification.smallY, OAI.ContingencyTables.ForestScaledPenalty.integerCube, OAI.ContingencyTables.ForestPenaltyBound.penalty