OAI/Analysis/BernoulliCone/HarmonicRadial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.HarmonicKernel.radial_hasFDerivAt line 15
2. lemma OAI.Bernoulli.HarmonicKernel.radial_directional line 21
3. lemma OAI.Bernoulli.HarmonicKernel.radial_second_directional line 28
4. lemma OAI.Bernoulli.HarmonicKernel.radial_laplacian line 50

   Source documentation

   The full Euclidean radial Laplacian; no polar-coordinate convention is hidden in this formula. It is used to build compact harmonic averaging kernels.

   lemma radial_laplacian {f : ℝ → ℝ} (hf : ContDiff ℝ ∞ f) (x : Space d) :
       Laplacian.laplacian (fun y : Space d => f (‖y‖^2)) x =
         4 * deriv (deriv f) (‖x‖^2) * ‖x‖^2 + 2 * d * deriv f (‖x‖^2) := by
   …

   Mentions: OAI.Bernoulli.Space