CorrelationVariance.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Exact finite correlation and variance estimates

The diagonal and off-diagonal coefficients are exact finite counts. The mixed sum has one exceptional parent column, hence D nested terms and D(D-1) separated terms. Every count identity permits arbitrary signed coefficients. The final cancellation imposes no positivity assumption on the common correlation alpha.

theorem OAI.ThompsonNonamenability.sum_one_exception line 31
Source documentation
One distinguished position and all the other positions, with signed values.
```
theorem sum_one_exception (i : Fin D) (b c : ℝ) :
    (∑ j : Fin D, if j = i then b else c) = b + ((D : ℝ) - 1) * c := by
…
```

theorem OAI.ThompsonNonamenability.sum_matrix_le line 43

Source documentation

D diagonal terms and D(D-1) off-diagonal terms, with no sign premise.

theorem sum_matrix_le (K : Fin D → Fin D → ℝ) (b c : ℝ)
    (hdiag : ∀ j, K j j ≤ b)
    (hoff : ∀ j k, j ≠ k → K j k ≤ c) :
    (∑ j, ∑ k, K j k) ≤
      (D : ℝ) * ((D : ℝ) - 1) * c + (D : ℝ) * b := by
…

theorem OAI.ThompsonNonamenability.sum_fixed_column_ge line 65

Source documentation

The exceptional column contributes D terms, irrespective of the row index.

theorem sum_fixed_column_ge (i : Fin D) (K : Fin D → Fin D → ℝ) (b c : ℝ)
    (hnested : ∀ j, b ≤ K j i)
    (hsep : ∀ j k, k ≠ i → c ≤ K j k) :
    (D : ℝ) * ((D : ℝ) - 1) * c + (D : ℝ) * b ≤ ∑ j, ∑ k, K j k := by
…

theorem OAI.ThompsonNonamenability.normalize_pair_total line 86
def OAI.ThompsonNonamenability.corr line 95
Source documentation
The literal finite average of the real inner product.
```
def corr (A : Finset G) (x y : G → E) : ℝ :=
…
```
theorem OAI.ThompsonNonamenability.corr_comm line 98
theorem OAI.ThompsonNonamenability.unit_inner_abs_le line 104
theorem OAI.ThompsonNonamenability.corr_abs_le_one line 111
theorem OAI.ThompsonNonamenability.realAvg_norm_finMean_sq line 124
theorem OAI.ThompsonNonamenability.corr_finMean line 129
theorem OAI.ThompsonNonamenability.realAvg_norm_sub_sq line 134

theorem OAI.ThompsonNonamenability.realAvg_norm_finMean_sq_le line 141

Source documentation

Parent or sibling averages: the same exact diagonal count applies to both.

theorem realAvg_norm_finMean_sq_le (A : Finset G) (hA : A.Nonempty)
    (hD : 0 < D) (x : G → Fin D → E) (c : ℝ)
    (hx : ∀ g ∈ A, ∀ j, ‖x g j‖ ≤ 1)
    (hsep : ∀ j k, j ≠ k → corr A (fun g => x g j) (fun g => x g k) ≤ c) :
    realAvg A (fun g => ‖finMean (x g)‖^2) ≤
      (1 - (D : ℝ)⁻¹) * c + (D : ℝ)⁻¹ := by
…

Mentions: OAI.ThompsonNonamenability.corr, OAI.ThompsonNonamenability.realAvg, OAI.ThompsonNonamenability.finMean

theorem OAI.ThompsonNonamenability.corr_finMean_ge line 159

Source documentation

Only the designated parent column is uncontrolled in a mixed sum.

theorem corr_finMean_ge (A : Finset G) (hA : A.Nonempty) (hD : 0 < D)
    (i : Fin D) (z x : G → Fin D → E) (c : ℝ)
    (hz : ∀ g ∈ A, ∀ j, ‖z g j‖ ≤ 1)
    (hx : ∀ g ∈ A, ∀ k, ‖x g k‖ ≤ 1)
    (hsep : ∀ j k, k ≠ i → c ≤ corr A (fun g => z g j) (fun g => x g k)) :
    (1 - (D : ℝ)⁻¹) * c - (D : ℝ)⁻¹ ≤
      corr A (fun g => finMean (z g)) (fun g => finMean (x g)) := by
…

Mentions: OAI.ThompsonNonamenability.corr, OAI.ThompsonNonamenability.finMean

theorem OAI.ThompsonNonamenability.finite_variance_bound line 181

Source documentation

The finite Hilbert variance bound with exact cancellation of signed alpha.

theorem finite_variance_bound (A : Finset G) (hA : A.Nonempty) (hD : 0 < D)
    (x : G → Fin D → E) (y : G → Fin D → Fin D → E) (α η : ℝ)
    (hx : ∀ g ∈ A, ∀ k, ‖x g k‖ ≤ 1)
    (hy : ∀ g ∈ A, ∀ i j, ‖y g i j‖ ≤ 1)
    (hparent : ∀ j k, j ≠ k →
      |corr A (fun g => x g j) (fun g => x g k) - α| ≤ η)
    (hchild : ∀ i j k, j ≠ k →
      |corr A (fun g => y g i j) (fun g => y g i k) - α| ≤ η)
    (hmixed : ∀ i j k, k ≠ i →
      |corr A (fun g => y g i j) (fun g => x g k) - α| ≤ η) :
    ∀ i, realAvg A (fun g => ‖finMean (y g i) - finMean (x g)‖^2) ≤
      4 / (D : ℝ) + 4 * (1 - 1 / (D : ℝ)) * η := by
…

Mentions: OAI.ThompsonNonamenability.corr, OAI.ThompsonNonamenability.realAvg, OAI.ThompsonNonamenability.finMean