Laplacian.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.NuclearUltrapower.laplacian line 15
Source documentation
sum of squared unitary displacements.
```
def laplacian (S : Finset Γ) (u : Γ → A) : A :=
…
```
theorem OAI.NuclearUltrapower.laplacian_nonneg line 18
theorem OAI.NuclearUltrapower.laplacian_selfAdjoint line 21
theorem OAI.NuclearUltrapower.laplacian_le line 24

theorem OAI.NuclearUltrapower.laplacian_complement_norm line 40

Source documentation

The norm form used for passing a positive lower bound through nuclearity.

theorem laplacian_complement_norm (S : Finset Γ) (u : Γ → unitary A)
    {b : ℝ} (hb : b ≤ 4 * (S.card : ℝ))
    (hgap : b • (1:A) ≤ laplacian S (fun s => (u s : A))) :
    ‖(4 * (S.card : ℝ)) • (1:A) - laplacian S (fun s => (u s : A))‖ ≤
      4 * (S.card : ℝ) - b := by
…

Mentions: OAI.NuclearUltrapower.laplacian

theorem OAI.NuclearUltrapower.laplacian_inner line 56
Source documentation
The quadratic form is exactly the energy, with no representation relations.
```
theorem laplacian_inner (S : Finset Γ) (u : Γ → (H →L[ℂ] H)) (x : H) :
    inner ℂ x (laplacian S u x) = (∑ s ∈ S, ‖u s x - x‖ ^ 2 : ℝ) := by
…
```
Mentions: OAI.NuclearUltrapower.laplacian

theorem OAI.NuclearUltrapower.laplacian_lower_iff line 63

Source documentation

Real quadratic forms detect the operator lower bound.

theorem laplacian_lower_iff (S : Finset Γ) (u : Γ → (H →L[ℂ] H)) (b : ℝ) :
    b • (1 : H →L[ℂ] H) ≤ laplacian S u ↔
      ∀ x, b * ‖x‖ ^ 2 ≤ ∑ s ∈ S, ‖u s x - x‖ ^ 2 := by
…

Mentions: OAI.NuclearUltrapower.laplacian