OAI/Analysis/BernoulliCone/HarmonicWeakLaplacian.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.Test.directional line 13
2. lemma OAI.Bernoulli.H1.laplacian_ibp line 21

   Source documentation

   Distributional integration by parts against the Euclidean Laplacian; no second derivatives of the Sobolev function occur in this statement.

   lemma H1.laplacian_ibp {u : Space d → ℝ} {G : Space d → Space d}
       (hu : H1 D u G) {φ : Space d → ℝ} (hφ : Test D φ) :
       (∫ x in D, u x * Laplacian.laplacian φ x) =
         -(∫ x in D, inner ℝ (G x) (gradient φ x)) := by
   …

   Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.H1, OAI.Bernoulli.Test

3. lemma OAI.Bernoulli.HarmonicReplacement.weak_laplacian_zero line 55