QuadraticTransport.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Quadratic ingredients for contingency-table transport

The quadratic-form version of the one-positive-direction property and the scalar telescoping step give the balanced-pair transport argument in both contingency-table sampling and counting papers.

def OAI.ContingencyTables.OnePositiveDirection line 32
Source documentation
A symmetric form is nonpositive on the form-orthogonal complement of every vector of positive square. This is the quadratic formulation of positive inertia at most one.
```
def OnePositiveDirection (B : BilinForm ℝ V) : Prop :=
…
```
theorem OAI.ContingencyTables.onePositiveDirection_of_kernel line 37
Source documentation
Nonpositivity on the kernel of one linear functional suffices for the quadratic signature needed in the manuscripts.
```
theorem onePositiveDirection_of_kernel (B : BilinForm ℝ V)
    (hsymm : ∀ x y, B x y = B y x) (ℓ : V →ₗ[ℝ] ℝ)
    (hker : ∀ v, ℓ v = 0 → B v v ≤ 0) : OnePositiveDirection B := by
…
```
Mentions: OAI.ContingencyTables.OnePositiveDirection
theorem OAI.ContingencyTables.positive_projection line 59
Source documentation
The projection inequality (200-01, equation positive-projection; 200-02, equation signature-projection).
```
theorem positive_projection (B : BilinForm ℝ V)
    (hsymm : ∀ x y, B x y = B y x) (hsig : OnePositiveDirection B)
    (u v : V) (hu : 0 < B u u) :
    B v v ≤ (B u v) ^ 2 / B u u := by
…
```
Mentions: OAI.ContingencyTables.OnePositiveDirection

theorem OAI.ContingencyTables.onePositiveDirection_of_rankOne_sub_squares line 80

Source documentation

The rank-one-minus-squares decomposition used for laminar factors implies the required signature. This theorem only requires the concrete decomposition on quadratic evaluations.

theorem onePositiveDirection_of_rankOne_sub_squares {G : Type*} [Fintype G]
    (B : BilinForm ℝ V) (hsymm : ∀ x y, B x y = B y x)
    (ℓ : V →ₗ[ℝ] ℝ) (L : G → V →ₗ[ℝ] ℝ) (a : G → ℝ)
    (ha : ∀ g, 0 ≤ a g)
    (hdecomp : ∀ v, B v v = (ℓ v) ^ 2 - ∑ g, a g * (L g v) ^ 2) :
    OnePositiveDirection B := by
…

Mentions: OAI.ContingencyTables.OnePositiveDirection

theorem OAI.ContingencyTables.pair_expansion line 96

Source documentation

Exact scalar expansion behind the balanced-pair telescoping inequality. The two mixed entries are expressed as discrete differences of the cumulative coefficients.

theorem pair_expansion (v um u up gm g gp : ℝ) :
    v + 2 * g * ((u * g - um * gm) - (up * gp - u * g)) +
        (um - 2 * u + up) * g ^ 2 -
        (um * (g - gm) ^ 2 + up * (g - gp) ^ 2) =
      v + 2 * u * g ^ 2 - um * gm ^ 2 - up * gp ^ 2 := by
…

theorem OAI.ContingencyTables.pair_telescoping_step line 107
Source documentation
Once the local projection estimate is available, the exact expansion gives equation pair-one in 200-01 and integer-telescoping in 200-02. The hypothesis is a local quadratic estimate, not a claim that the whole manuscript has been proved.
```
theorem pair_telescoping_step (v um u up gm g gp : ℝ)
    (hprojection :
      v + 2 * g * ((u * g - um * gm) - (up * gp - u * g)) +
          (um - 2 * u + up) * g ^ 2 ≤
        um * (g - gm) ^ 2 + up * (g - gp) ^ 2) :
    2 * u * g ^ 2 - um * gm ^ 2 - up * gp ^ 2 ≤ -v := by
…
```

theorem OAI.ContingencyTables.pair_step_of_signature line 124

Source documentation

The local inequality follows from the signature even when either or both of the fresh diagonal entries vanish. This includes the capacity-two boundary case in both manuscripts.

theorem pair_step_of_signature (B : BilinForm ℝ V)
    (hsymm : ∀ x y, B x y = B y x) (hsig : OnePositiveDirection B)
    (h ea eb : V) (um u up gm g gp : ℝ)
    (haa : B ea ea = um) (hbb : B eb eb = up) (hab : B ea eb = u)
    (hha : B h ea = u * g - um * gm)
    (hhb : B h eb = up * gp - u * g)
    (hum : 0 ≤ um) (hup : 0 ≤ up)
    (hpositive : 0 < um ∨ 0 < up ∨ (um = 0 ∧ up = 0 ∧ 0 < u)) :
    2 * u * g ^ 2 - um * gm ^ 2 - up * gp ^ 2 ≤ -B h h := by
…

Mentions: OAI.ContingencyTables.OnePositiveDirection

theorem OAI.ContingencyTables.sum_second_differences line 187
Source documentation
The scalar second differences telescope with their actual boundary terms. No absent endpoint matrix is needed.
```
theorem sum_second_differences (a : ℕ → ℝ) (n : ℕ) :
    (∑ j ∈ range n, (2 * a (j + 1) - a j - a (j + 2))) =
      a 1 - a 0 + a n - a (n + 1) := by
…
```

theorem OAI.ContingencyTables.sum_second_differences_zero line 198

Source documentation

The endpoint convention in the unweighted balanced-pair summation makes the scalar second differences have zero total.

theorem sum_second_differences_zero (a : ℕ → ℝ) (n : ℕ)
    (h0 : a 0 = 0) (h1 : a 1 = 0) (hn : a n = 0) (hn1 : a (n + 1) = 0) :
    (∑ j ∈ range n, (2 * a (j + 1) - a j - a (j + 2))) = 0 := by
…