BalancedSummation.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Balanced-pair summation of two-removal forms

This is the finite unweighted closure step in paper 200-01, Lemma lem:pair-summation (D'=B), and paper 200-02, Lemma lem:integer-signature. The hypotheses describe the actual old/fresh blocks and their adjacent cross entries. Cumulative coefficients are constructed from those cross entries; no transport or closure conclusion is assumed. In particular the zero-diagonal capacity-two case is included.

theorem OAI.ContingencyTables.sum_pred_second_differences line 24

Source documentation

The lower endpoint convention used by the balanced-pair matrices.

theorem sum_pred_second_differences (a : ℕ → ℝ) (n : ℕ) :
    (∑ j ∈ Finset.range (n + 1), (2 * a j - a (j - 1) - a (j + 1))) =
      a n - a (n + 1) := by
…

theorem OAI.ContingencyTables.sum_firstMoment_second_differences line 35

Source documentation

First moment of the discrete second difference, with exact boundaries.

theorem sum_firstMoment_second_differences (a : ℕ → ℝ) (n : ℕ) :
    (∑ j ∈ Finset.range (n + 1), (j : ℝ) * (2 * a j - a (j - 1) - a (j + 1))) =
      ((n : ℝ) + 1) * a n - a 0 - (n : ℝ) * a (n + 1) := by
…

theorem OAI.ContingencyTables.sum_secondMoment_second_differences line 46

Source documentation

Second moment of the same difference.

theorem sum_secondMoment_second_differences (a : ℕ → ℝ) (n : ℕ) :
    (∑ j ∈ Finset.range (n + 1), (j : ℝ) ^ 2 * (2 * a j - a (j - 1) - a (j + 1))) =
      ((n : ℝ) + 1) ^ 2 * a n - (n : ℝ) ^ 2 * a (n + 1) + a 0 -
        2 * ∑ j ∈ Finset.range (n + 1), a j := by
…

theorem OAI.ContingencyTables.sum_weighted_second_differences line 61

Source documentation

The exact weighted telescope in equation pair-weighted. The boundary terms are scalar values, so invalid endpoint matrices are never needed.

theorem sum_weighted_second_differences (a : ℕ → ℝ) (n : ℕ) :
    (∑ j ∈ Finset.range (n + 1), (j : ℝ) * ((n : ℝ) - j) *
      (2 * a j - a (j - 1) - a (j + 1))) =
      2 * (∑ j ∈ Finset.range (n + 1), a j) - ((n : ℝ) + 1) * (a 0 + a n) := by
…

theorem OAI.ContingencyTables.weighted_second_differences_bound line 80

Source documentation

Summation of the local inequalities with the actual nonnegative weights. Only interior inequalities are required.

theorem weighted_second_differences_bound (a v : ℕ → ℝ) (n : ℕ)
    (ha0 : a 0 = 0) (han : a n = 0)
    (hlocal : ∀ j, 0 < j → j < n →
      2 * a j - a (j - 1) - a (j + 1) ≤ -v j) :
    2 * (∑ j ∈ Finset.range (n + 1), a j) ≤
      -(∑ j ∈ Finset.range (n + 1), (j : ℝ) * ((n : ℝ) - j) * v j) := by
…

def OAI.ContingencyTables.pairCumulative line 110
Source documentation
The partial cross-entry sum in equation pair-cumulative.
```
def pairCumulative (S : ℕ → V →ₗ[ℝ] ℝ) (v : V) (j : ℕ) : ℝ :=
…
```
lemma OAI.ContingencyTables.pairCumulative_zero line 113
lemma OAI.ContingencyTables.pairCumulative_succ line 116
def OAI.ContingencyTables.pairCoefficient line 122
Source documentation
The cumulative coefficients, with division by zero harmless at the endpoints because the corresponding cumulative mass is proved zero.
```
noncomputable def pairCoefficient (S : ℕ → V →ₗ[ℝ] ℝ) (u : ℕ → ℝ) (v : V) (j : ℕ) : ℝ :=
…
```
lemma OAI.ContingencyTables.pairCoefficient_represents line 125
lemma OAI.ContingencyTables.pairCoefficient_represents_le line 146
Source documentation
Representation up to the balanced endpoint needs no value outside that endpoint. This version is used for the D'=B+1 interior displays.
```
lemma pairCoefficient_represents_le (S : ℕ → V →ₗ[ℝ] ℝ) (u : ℕ → ℝ)
    (n : ℕ) (v : V)
    (huint : ∀ j, 0 < j → j < n → 0 < u j)
    (hbalance : pairCumulative S v n = 0) {j : ℕ} (hj : j ≤ n) :
    u j * pairCoefficient S u v j = pairCumulative S v j := by
…
```
Mentions: OAI.ContingencyTables.pairCumulative, OAI.ContingencyTables.pairCoefficient
lemma OAI.ContingencyTables.pairCumulative_difference line 161

theorem OAI.ContingencyTables.balancedPair_sum_onePositive line 176

Source documentation

Summing the old blocks of the two-removal matrices preserves the one-positive-direction signature. The cumulative coefficients and common kernel are explicit.

theorem balancedPair_sum_onePositive
    (n : ℕ) (hn : 2 ≤ n)
    (B : ℕ → BilinForm ℝ W) (old : V →ₗ[ℝ] W) (ea eb : W)
    (S : ℕ → V →ₗ[ℝ] ℝ) (u : ℕ → ℝ)
    (hsymm : ∀ j ≤ n, ∀ x y, B j x y = B j y x)
    (hsig : ∀ j ≤ n, OnePositiveDirection (B j))
    (hu0 : u 0 = 0) (hun : u n = 0) (hun1 : u (n + 1) = 0)
    (huint : ∀ j, 0 < j → j < n → 0 < u j)
    (hS0 : S 0 = 0) (hSn1 : S (n + 1) = 0)
    (haa : ∀ j ≤ n, B j ea ea = u (j - 1))
    (hbb : ∀ j ≤ n, B j eb eb = u (j + 1))
    (hab : ∀ j ≤ n, B j ea eb = u j)
…

Mentions: OAI.ContingencyTables.OnePositiveDirection

theorem OAI.ContingencyTables.balancedPair_weighted_potential line 264

Source documentation

The actual weighted pair estimate (D'=B+1) used in integer signed transport. Only the box-valid interior matrices are evaluated. The coefficients are the explicitly constructed cumulative quotients.

theorem balancedPair_weighted_potential
    (n : ℕ) (B : ℕ → BilinForm ℝ W) (old : V →ₗ[ℝ] W) (ea eb : W)
    (S : ℕ → V →ₗ[ℝ] ℝ) (u : ℕ → ℝ) (v : V)
    (hsymm : ∀ j, 0 < j → j < n → ∀ x y, B j x y = B j y x)
    (hsig : ∀ j, 0 < j → j < n → OnePositiveDirection (B j))
    (hu0 : u 0 = 0) (hun : u n = 0)
    (huint : ∀ j, 0 < j → j < n → 0 < u j)
    (hbalance : pairCumulative S v n = 0)
    (haa : ∀ j, 0 < j → j < n → B j ea ea = u (j - 1))
    (hbb : ∀ j, 0 < j → j < n → B j eb eb = u (j + 1))
    (hab : ∀ j, 0 < j → j < n → B j ea eb = u j)
    (hha : ∀ j, 0 < j → j < n → B j (old v) ea = S j v)
…

Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.pairCumulative