QuadraticForms.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SharpLiebThirring.SpectralProof.quadratic_error_bound line 13

lemma OAI.SharpLiebThirring.SpectralProof.eventually_negative_quadratic line 34

Source documentation

A strict negative diagonal is stable under entrywise perturbations.

lemma eventually_negative_quadratic {ι : Type u167} [Fintype ι] [DecidableEq ι] (M : ℕ → ι → ι → ℝ)
    (d : ι → ℝ) (hd : ∀ i, d i < 0)
    (hM : ∀ i j, Tendsto (fun n ↦ M n i j) atTop (𝓝 (if i=j then d i else 0))) :
    ∀ᶠ n in atTop, ∀ c : ι → ℝ, (∑ i, ∑ j, c i*c j*M n i j) ≤ 0 := by
…

lemma OAI.SharpLiebThirring.SpectralProof.doubled_orthonormal line 87

Source documentation

Complex orthonormal vectors give twice as many real orthonormal vectors.

lemma doubled_orthonormal {ι : Type u169} [DecidableEq ι] (a b : ι → E)
    (hr : ∀ i j, inner ℝ (a i) (a j)+inner ℝ (b i) (b j) = if i=j then 1 else 0)
    (hi : ∀ i j, inner ℝ (a i) (b j)-inner ℝ (b i) (a j) = 0) :
    Orthonormal ℝ (fun z : ι × Bool ↦
      WithLp.toLp 2 (if z.2 then (-b z.1,a z.1) else (a z.1,b z.1))) := by
…

lemma OAI.SharpLiebThirring.SpectralProof.complex_family_card_le_real_dimension line 103