ForestAffineCoefficients.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The actual maximum-forest cut coefficients of tree completions

def OAI.ContingencyTables.ForestAffineCoefficients.edge line 16
def OAI.ContingencyTables.ForestAffineCoefficients.cutVertex line 18
def OAI.ContingencyTables.ForestAffineCoefficients.cutSide line 22
lemma OAI.ContingencyTables.ForestAffineCoefficients.cut_properties line 25
def OAI.ContingencyTables.ForestAffineCoefficients.sign line 32
lemma OAI.ContingencyTables.ForestAffineCoefficients.sign_abs_le_one line 35
lemma OAI.ContingencyTables.ForestAffineCoefficients.sign_abs_self line 40
lemma OAI.ContingencyTables.ForestAffineCoefficients.sign_self_ne_zero line 43
def OAI.ContingencyTables.ForestAffineCoefficients.coefficient line 49
lemma OAI.ContingencyTables.ForestAffineCoefficients.coefficient_abs_le_one line 53
lemma OAI.ContingencyTables.ForestAffineCoefficients.capacity_le_of_coefficient_ne_zero line 63
Source documentation
A nonzero tree coefficient crosses the actual edge-deletion cut, so maximum total capacity bounds the contributing free capacity.
```
lemma capacity_le_of_coefficient_ne_zero (A : Instance I J) (t : TreeCell A.T) (a : I×J)
    (ha : coefficient A t a≠0) : A.b a.1 a.2 ≤ A.b t.val.1 t.val.2 := by
…
```
Mentions: OAI.ContingencyTables.ForestAffineCoefficients.coefficient
theorem OAI.ContingencyTables.ForestAffineCoefficients.normalized_coefficient_bound line 82
Source documentation
Scaling a free coordinate by (b_free+1)/B and normalizing a tree value by b_tree gives coefficients at most 2/B, including structural zero coefficients. This is the precise forest input to the evaluator's Lipschitz estimate.
```
theorem normalized_coefficient_bound (A : Instance I J) (t : TreeCell A.T) (a : I×J)
    (B : ℝ) (hB : 0 < B) :
    |coefficient A t a*((A.b a.1 a.2:ℝ)+1)/B/(A.b t.val.1 t.val.2:ℝ)| ≤ 2/B := by
…
```
Mentions: OAI.ContingencyTables.ForestAffineCoefficients.coefficient