OAI/Analysis/LiebThirring/PotentialSplit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.OperatorProof.potential_decomposition line 13

   Source documentation

   The only potential-approximation fact needed for the associated operator: an Lᵖ potential, p>1, is bounded plus an arbitrarily small L¹ remainder.

   lemma potential_decomposition {γ : ℝ} {W : ℝ → ℝ} (hγ : 1/2 < γ)
       (hW : Admissible γ W) {ε : ℝ} (hε : 0 < ε) :
       ∃ b : ℝ, 0 ≤ b ∧ ∃ V : ℝ → ℝ, (∀ x, 0 ≤ V x) ∧ Integrable V ∧
         (∫ x, V x) ≤ ε ∧ ∀ x, ‖W x‖ ≤ b+V x := by
   …

   Mentions: OAI.SharpLiebThirring.Admissible