OAI/Geometry/RCD/Sobolev/EuclideanLaplacianDilation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.laplacian_affine_dilation line 15

   Source documentation

   The Laplacian gains exactly two powers of a scalar input dilation.

   theorem laplacian_affine_dilation {n : ℕ} {f : Euclidean n → ℝ}
       (hf : ContDiff ℝ 2 f) (p : Euclidean n) (t : ℝ) (x : Euclidean n) :
       (Δ (fun y => f (p+t • y))) x = t^2*(Δ f) (p+t • x) := by
   …

   Mentions: OAI.RegularPointCoordinates.Euclidean

2. theorem OAI.RegularPointCoordinates.harmonicOnNhd_affine_dilation line 33

   Source documentation

   Classical local harmonicity is preserved by an affine dilation.

   theorem harmonicOnNhd_affine_dilation {n : ℕ} {f : Euclidean n → ℝ}
       (hf : ContDiff ℝ 2 f) {Ω : Set (Euclidean n)}
       (hh : HarmonicOnNhd f Ω) (p : Euclidean n) (t : ℝ) :
       HarmonicOnNhd (fun y => f (p+t • y)) {x | p+t • x ∈ Ω} := by
   …

   Mentions: OAI.RegularPointCoordinates.Euclidean