ForestRootPenalty.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Actual root residuals of the integral forest completion

Summing a root-path flow gives the prescribed demand minus the total demand in the component. This formula also applies at roots and on singleton components, where the nonroot-only margin lemma is vacuous.

theorem OAI.ContingencyTables.ForestRootPenalty.completionFlow_divergence_all line 23
theorem OAI.ContingencyTables.ForestRootPenalty.sum_abs_componentTotal line 33
Source documentation
Absolute component totals sum to at most the total absolute demand. Each vertex is counted in one component, including isolated vertices.
```
theorem sum_abs_componentTotal (root : V → V) (r : V → ℝ) :
    (∑ a, |∑ v, if root v=a then r v else 0|)≤∑ v, |r v| := by
…
```

lemma OAI.ContingencyTables.ForestRootPenalty.root_eq_large line 51

Source documentation

Maximum capacity makes every original large edge stay within a tree component, which is the exact cancellation needed at component roots.

lemma root_eq_large (small : I → J → Bool) (b : I → J → ℕ)
    (T : SimpleGraph (I⊕J)) (hT : T≤ForestCapacity.cellGraph small) (hacyc : T.IsAcyclic)
    (hmax : ∀ F : SimpleGraph (I⊕J), F≤ForestCapacity.cellGraph small → F.IsAcyclic →
      MaximumForest.weight F (ForestCapacity.capacity b)≤MaximumForest.weight T (ForestCapacity.capacity b))
    (hb : ∀ i j, small i j=false → 1≤b i j) (i : I) (j : J) (hs : small i j=false) :
    componentRoot T (.inl i)=componentRoot T (.inr j) := by
…

Mentions: OAI.ContingencyTables.ForestCapacity.cellGraph, OAI.ContingencyTables.MaximumForest.weight, OAI.ContingencyTables.ForestCapacity.capacity

lemma OAI.ContingencyTables.ForestRootPenalty.tableCompletion_row_all line 77
lemma OAI.ContingencyTables.ForestRootPenalty.tableCompletion_column_all line 91
def OAI.ContingencyTables.ForestRootPenalty.residualDemand line 111
def OAI.ContingencyTables.ForestRootPenalty.componentTotal line 115
def OAI.ContingencyTables.ForestRootPenalty.smallDemand line 118

theorem OAI.ContingencyTables.ForestRootPenalty.componentTotal_residual line 125

Source documentation

Large-cell incidences cancel exactly within each component. The component residual therefore depends only on the small views, not on the chosen free values.

theorem componentTotal_residual (small : I → J → Bool) (T : SimpleGraph (I⊕J))
    (r : I → ℤ) (c : J → ℤ) (x q free X : I → J → ℤ)
    (hr : ∀ i, (∑ j, X i j)=r i) (hc : ∀ j, (∑ i, X i j)=c j)
    (hroot : ∀ i j, small i j=false → componentRoot T (.inl i)=componentRoot T (.inr j))
    (a : I⊕J) :
    componentTotal T (residualDemand small T r c x q free) a=
      componentTotal T (smallDemand small X x q) a := by
…

Mentions: OAI.ContingencyTables.ForestRootPenalty.componentTotal, OAI.ContingencyTables.ForestRootPenalty.residualDemand, OAI.ContingencyTables.ForestRootPenalty.smallDemand

def OAI.ContingencyTables.ForestRootPenalty.signedResidual line 164
theorem OAI.ContingencyTables.ForestRootPenalty.signedResidual_eq_component line 172
Source documentation
The actual completed table's signed root discrepancy is exactly the negative component total of its original residual demands.
```
theorem signedResidual_eq_component (small : I → J → Bool) (T : SimpleGraph (I⊕J))
    (hT : T≤ForestCapacity.cellGraph small) (r : I → ℤ) (c : J → ℤ)
    (x q free : I → J → ℤ) (a : I⊕J) :
    signedResidual small T r c x q free a=
      -(∑ v, if componentRoot T v=a then residualDemand small T r c x q free v else 0) := by
…
```
Mentions: OAI.ContingencyTables.ForestCapacity.cellGraph, OAI.ContingencyTables.ForestRootPenalty.signedResidual, OAI.ContingencyTables.ForestRootPenalty.residualDemand
theorem OAI.ContingencyTables.ForestRootPenalty.signedResidual_eq_small line 204

theorem OAI.ContingencyTables.ForestRootPenalty.signedResidual_independent line 220

Source documentation

The original root deviations do not depend on the free assignment; this follows from the actual integral completion, rather than an assumed affine representation of the source count.

theorem signedResidual_independent (small : I → J → Bool) (T : SimpleGraph (I⊕J))
    (hT : T≤ForestCapacity.cellGraph small) (r : I → ℤ) (c : J → ℤ)
    (x q free free' X : I → J → ℤ)
    (hr : ∀ i, (∑ j, X i j)=r i) (hc : ∀ j, (∑ i, X i j)=c j)
    (hroot : ∀ i j, small i j=false → componentRoot T (.inl i)=componentRoot T (.inr j)) :
    signedResidual small T r c x q free=signedResidual small T r c x q free' := by
…

Mentions: OAI.ContingencyTables.ForestCapacity.cellGraph, OAI.ContingencyTables.ForestRootPenalty.signedResidual

theorem OAI.ContingencyTables.ForestRootPenalty.sum_abs_signedResidual_le line 230
lemma OAI.ContingencyTables.ForestRootPenalty.abs_actualDeviation_solved line 289

theorem OAI.ContingencyTables.ForestRootPenalty.rootPenalty_le line 308

Source documentation

This is the root part of the source's actual penalty. Each small cell contributes at most its capacity at each of its two incidences.

theorem rootPenalty_le (small : I → J → Bool) (T : SimpleGraph (I⊕J))
    (hT : T≤ForestCapacity.cellGraph small) (b x y free : I → J → ℕ)
    (r : I → ℤ) (c : J → ℤ) (X : I → J → ℤ)
    (hr : ∀ i, (∑ j, X i j)=r i) (hc : ∀ j, (∑ i, X i j)=c j)
    (hroot : ∀ i j, small i j=false → componentRoot T (.inl i)=componentRoot T (.inr j))
    (hx : ∀ i j, small i j=true → x i j≤b i j)
    (hX : ∀ i j, 0≤X i j ∧ X i j≤b i j) :
    (∑ a, if ForestPenaltyApplication.rootFlag T a then
      |actualDeviation small T b x y free r c
        (solved small T r c (fun i j => (x i j:ℤ))
          (fun i j => ((b i j-y i j:ℕ):ℤ)) (fun i j => (free i j:ℤ))) a| else 0)≤
      2*∑ i, ∑ j, if small i j then (b i j:ℝ) else 0 := by
…

Mentions: OAI.ContingencyTables.ForestCapacity.cellGraph, OAI.ContingencyTables.ForestPenaltyApplication.rootFlag