HilbertAverage.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite averages in the unit ball

The norm bounds hold in any real seminormed space. Inner-product expansions are kept in a separate section and require a real inner-product space.

def OAI.ThompsonNonamenability.finMean line 28
Source documentation
The equally weighted mean of a finite family.
```
def finMean (x : Fin D → E) : E :=
…
```
theorem OAI.ThompsonNonamenability.finMean_sub line 31
theorem OAI.ThompsonNonamenability.finMean_const line 35
theorem OAI.ThompsonNonamenability.norm_finMean_sq_le line 42
Source documentation
The squared norm of a mean is bounded by the mean of the squared norms.
```
theorem norm_finMean_sq_le (hD : 0 < D) (x : Fin D → E) :
    ‖finMean x‖ ^ 2 ≤ (D : ℝ)⁻¹ * ∑ i, ‖x i‖ ^ 2 := by
…
```
Mentions: OAI.ThompsonNonamenability.finMean
theorem OAI.ThompsonNonamenability.finMean_mem_unitBall line 62
Source documentation
Averaging a finite family in the closed unit ball preserves its norm bound.
```
theorem finMean_mem_unitBall (hD : 0 < D) (x : Fin D → UnitBall E) :
    ‖finMean (fun i => (x i : E))‖ ≤ 1 := by
…
```
Mentions: OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.finMean
def OAI.ThompsonNonamenability.ballMean line 79
Source documentation
The equally weighted mean, bundled with its unit-ball bound.
```
def ballMean (hD : 0 < D) (x : Fin D → UnitBall E) : UnitBall E :=
…
```
Mentions: OAI.ThompsonNonamenability.UnitBall
theorem OAI.ThompsonNonamenability.coe_ballMean line 82
theorem OAI.ThompsonNonamenability.inner_finMean line 93
Source documentation
The inner product of two finite averages is the average of all pairings.
```
theorem inner_finMean (x : Fin D → E) (y : Fin K → E) :
    ⟪finMean x, finMean y⟫_ℝ =
      ((D : ℝ)⁻¹ * (K : ℝ)⁻¹) * ∑ i, ∑ j, ⟪x i, y j⟫_ℝ := by
…
```
Mentions: OAI.ThompsonNonamenability.finMean
theorem OAI.ThompsonNonamenability.norm_finMean_sq line 100
Source documentation
Expand the squared norm of an average into all pairwise inner products.
```
theorem norm_finMean_sq (x : Fin D → E) :
    ‖finMean x‖ ^ 2 = ((D : ℝ)⁻¹) ^ 2 * ∑ i, ∑ j, ⟪x i, x j⟫_ℝ := by
…
```
Mentions: OAI.ThompsonNonamenability.finMean