OAI/Analysis/LiebThirring/FlagApproximation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.SpectralProof.eventually_cut_prefix_negative line 11
2. lemma OAI.SharpLiebThirring.SpectralProof.exists_compact_negative_flag line 53

   Source documentation

   A compact orthonormal flag with the exact strict spectral margins.

   lemma exists_compact_negative_flag {N : ℕ} {W : ℝ → ℝ}
       (hW : LocallyIntegrable W volume) (u : Fin N → C1L2) (k κ : Fin N → ℝ)
       (ho : Orthonormal ℝ u) (he : ∀ i, (u i).IsEigen W (k i))
       (hk : ∀ i, 0 < k i) (hκ : ∀ i, 0 < κ i ∧ κ i < k i)
       (horder : Antitone k) :
       ∃ q : Fin N → C1L2, Orthonormal ℝ q ∧
         (∀ i, HasCompactSupport (q i).val) ∧
         ∀ i (v : C1L2), v ∈ Submodule.span ℝ (q '' Iic i) →
           energy W v v+κ i^2*inner ℝ v v ≤ 0 := by
   …