Ball normalizations for harmonic functions

The PDE roadmap's Lane C uses translations and dilations to reduce local arguments on a ball Metric.ball x r to arguments on the unit ball. The files TauCeti.Analysis.InnerProductSpace.Harmonic.Isometry and TauCeti.Analysis.InnerProductSpace.Harmonic.Dilation prove the underlying invariance of harmonicity under translations and nonzero dilations. This file packages the corresponding consumer forms for metric balls, using the generic set normalizations from TauCeti.Analysis.Normed.Module.Ball.

The main statement is harmonicOnNhd_comp_const_add_smul_ball_iff: for 0 < r, the normalized function y ↦ f (x + r • y) is harmonic near the unit ball if and only if f is harmonic near Metric.ball x r.

Main declarations

• TauCeti.harmonicOnNhd_comp_add_right_ball_zero_iff, TauCeti.harmonicOnNhd_comp_add_right_closedBall_zero_iff: translation-normalized harmonicity on a ball and on a closed ball.
• TauCeti.harmonicOnNhd_comp_const_add_smul_ball_radius_iff: ball-level affine normalization by y ↦ x + c • y for nonzero scale c.
• TauCeti.harmonicOnNhd_comp_const_add_smul_ball_iff: the unit-ball specialization.

theorem TauCeti.harmonicOnNhd_comp_const_add_smul_ball_radius_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (x : E) {c : ℝ} (hc : c ≠ 0) (r : ℝ) {f : E → F} : InnerProductSpace.HarmonicOnNhd (fun (y : E) => f (x + c • y)) (Metric.ball 0 r) ↔ InnerProductSpace.HarmonicOnNhd f (Metric.ball x (‖c‖ * r))

Harmonicity on a neighbourhood of Metric.ball x (‖c‖ * r) is equivalent to harmonicity of y ↦ f (x + c • y) on a neighbourhood of Metric.ball 0 r, for nonzero scale c.

theorem TauCeti.harmonicOnNhd_comp_add_right_ball_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (x : E) (r : ℝ) {f : E → F} : InnerProductSpace.HarmonicOnNhd (fun (y : E) => f (y + x)) (Metric.ball 0 r) ↔ InnerProductSpace.HarmonicOnNhd f (Metric.ball x r)

Translation-normalized harmonicity on a ball. The function y ↦ f (y + x) is harmonic near the radius-r ball centered at 0 exactly when f is harmonic near the corresponding ball centered at x.

theorem TauCeti.harmonicOnNhd_comp_add_right_closedBall_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (x : E) (r : ℝ) {f : E → F} : InnerProductSpace.HarmonicOnNhd (fun (y : E) => f (y + x)) (Metric.closedBall 0 r) ↔ InnerProductSpace.HarmonicOnNhd f (Metric.closedBall x r)

Translation-normalized harmonicity on a closed ball. The function y ↦ f (y + x) is harmonic near the radius-r closed ball centered at 0 exactly when f is harmonic near the corresponding closed ball centered at x.

theorem TauCeti.harmonicOnNhd_comp_const_add_smul_ball_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (x : E) {r : ℝ} (hr : 0 < r) {f : E → F} : InnerProductSpace.HarmonicOnNhd (fun (y : E) => f (x + r • y)) (Metric.ball 0 1) ↔ InnerProductSpace.HarmonicOnNhd f (Metric.ball x r)

Harmonicity on a neighbourhood of Metric.ball x r is equivalent to harmonicity of the normalized function y ↦ f (x + r • y) on a neighbourhood of the unit ball.