ForestAffineCompletion.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The original integral forest solution is the cut-defined affine completion

lemma OAI.ContingencyTables.ForestAffineCoefficients.selected_nonroot line 15
lemma OAI.ContingencyTables.ForestAffineCoefficients.other_tree_sign_zero line 29
def OAI.ContingencyTables.ForestAffineCoefficients.smallContribution line 35
def OAI.ContingencyTables.ForestAffineCoefficients.offset line 41
def OAI.ContingencyTables.ForestAffineCoefficients.affineTree line 45

theorem OAI.ContingencyTables.ForestAffineCoefficients.affine_of_nonroot_equations line 51

Source documentation

Isolating the actual selected tree edge in the root-away cut gives its affine value for every real solution of the nonroot equations.

theorem affine_of_nonroot_equations (A : Instance I J) (t : TreeCell A.T)
    (x q z : I → J → ℝ)
    (hr : ∀ i,Sum.inl i≠componentRoot A.T (.inl i) →
      rowDifference A.small x z (fun i j => (A.X i j:ℝ)) i=0)
    (hc : ∀ j,Sum.inr j≠componentRoot A.T (.inr j) →
      columnDifference A.small q z (fun i j => (A.X i j:ℝ)) j=0) :
    z t.val.1 t.val.2=affineTree A t x q (fun a => z a.1 a.2) := by
…

Mentions: OAI.ContingencyTables.ForestAffineCoefficients.affineTree

theorem OAI.ContingencyTables.ForestAffineCoefficients.solved_eq_affine line 113
Source documentation
In particular this affine display is the original integral solution used inside h_j, rather than an unrelated continuous extension.
```
theorem solved_eq_affine (A : Instance I J) (t : TreeCell A.T)
    (x q free : I → J → ℤ) :
    (solved A.small A.T A.r A.c x q free t.val.1 t.val.2:ℝ)=
      affineTree A t (fun i j => (x i j:ℝ)) (fun i j => (q i j:ℝ))
        (fun a => (free a.1 a.2:ℝ)) := by
…
```
Mentions: OAI.ContingencyTables.ForestAffineCoefficients.affineTree