OAI/Analysis/BernoulliCone/HarmonicCaccioppoli.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.HarmonicReplacement.caccioppoli line 16

   Source documentation

   Caccioppoli's inequality for the genuine weak harmonic replacement. The only test inserted is a proved H¹₀ product; no smoothness of u is used.

   lemma caccioppoli {u : Space d → ℝ} {G : Space d → Space d}
       (hD : IsOpen D) (hu : H1 D u G)
       (ho : ∀ v V, H10 D v V → (∫ x in D, inner ℝ (G x) (V x)) = 0)
       {η : Space d → ℝ} (hη : Test D η) :
       (∫ x in D, ‖η x • G x‖^2) ≤ 4 * (∫ x in D, ‖u x • gradient η x‖^2) := by
   …

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