OAI/Analysis/LiebThirring/SobolevProjection.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLiebThirring.SobolevProof.ae_const_of_weak_derivative_zero line 13

    Source documentation

    A locally integrable function whose distributional derivative vanishes is constant. This uses only smooth compact tests, hence applies to the H¹ definition.

    lemma ae_const_of_weak_derivative_zero {f : ℝ → ℝ} (hf : LocallyIntegrable f volume)
    (hw : ∀ φ : ℝ → ℝ, ContDiff ℝ ∞ φ → HasCompactSupport φ →
      (∫ x, f x * deriv φ x) = 0) : ∃ c : ℝ, f =ᵐ[volume] fun _ ↦ c := by
…
  2. lemma OAI.SharpLiebThirring.SobolevProof.primitive_weak_derivative line 50
  3. lemma OAI.SharpLiebThirring.SobolevProof.weak_derivative_representation line 91

    Source documentation

    The precise one-dimensional Sobolev representative, obtained from the weak derivative without assuming any pointwise regularity or adding a representative to the domain.

    lemma weak_derivative_representation {f g : ℝ → ℝ}
    (hf : LocallyIntegrable f volume) (hg : LocallyIntegrable g volume)
    (hw : ∀ φ : ℝ → ℝ, ContDiff ℝ ∞ φ → HasCompactSupport φ →
      (∫ x, f x * deriv φ x) = -(∫ x, g x * φ x)) :
    ∃ c : ℝ, f =ᵐ[volume] fun x ↦ c + ∫ t in (0 : ℝ)..x, g t := by
…
  4. lemma OAI.SharpLiebThirring.SobolevProof.h1_project_weak line 116
  5. lemma OAI.SharpLiebThirring.SobolevProof.h1_continuous_representative line 136
  6. structure OAI.SharpLiebThirring.SobolevProof.RealEigenfunction line 162

    Source documentation

    Classical representative of a real weak second-order eigenfunction.

    structure RealEigenfunction (W : ℝ → ℝ) (k : ℝ) where
…
  7. lemma OAI.SharpLiebThirring.SobolevProof.real_eigen_of_weak line 172
  8. lemma OAI.SharpLiebThirring.SobolevProof.clm_mul_real line 224
  9. lemma OAI.SharpLiebThirring.SobolevProof.integrable_h1_test line 227
  10. lemma OAI.SharpLiebThirring.SobolevProof.integrable_potential_h1_test line 232
  11. lemma OAI.SharpLiebThirring.SobolevProof.eigen_weak_second line 243
  12. lemma OAI.SharpLiebThirring.SobolevProof.eigen_project_weak_second line 271
  13. lemma OAI.SharpLiebThirring.SobolevProof.eigen_project_representative line 289
  14. def OAI.SharpLiebThirring.SobolevProof.RealEigenfunction.toC1L2 line 302
  15. lemma OAI.SharpLiebThirring.SobolevProof.RealEigenfunction.toC1L2_eigen line 305
  16. lemma OAI.SharpLiebThirring.SobolevProof.eigen_C1_representative line 314
  17. lemma OAI.SharpLiebThirring.SobolevProof.re_l2Pairing line 321
  18. lemma OAI.SharpLiebThirring.SobolevProof.im_l2Pairing line 338