OAI/Analysis/LiebThirring/ComplexFamilies.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.SpectralProof.real_family_bound_sorted line 13
2. lemma OAI.SharpLiebThirring.SpectralProof.real_family_action_bound line 39
3. lemma OAI.SharpLiebThirring.SpectralProof.action_constant_eq_sharp line 57
4. lemma OAI.SharpLiebThirring.SpectralProof.real_family_bound line 67
5. lemma OAI.SharpLiebThirring.SpectralProof.realify_finite_family line 100

   Source documentation

   Finite realification, retaining all complex multiplicities at each energy.

   lemma realify_finite_family {ι : Type} [Fintype ι] [DecidableEq ι]
       {W : ℝ → ℝ} (hW : LocallyIntegrable W volume) (k : ι → ℝ)
       (hk : ∀ i, 0 < k i) (a b : ι → C1L2)
       (ha : ∀ i, (a i).IsEigen W (k i)) (hb : ∀ i, (b i).IsEigen W (k i))
       (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)
       (p : ℝ) :
       ∃ (J : Type) (_ : Fintype J) (v : J → C1L2) (l : J → ℝ),
         Orthonormal ℝ v ∧ (∀ j, (v j).IsEigen W (l j)) ∧ (∀ j, 0 < l j) ∧
         (∑ i, k i^p) ≤ ∑ j, l j^p := by
   …