HarmonicSphereNorm

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The Euclidean norm on the sup-normed carrier, and its coordinate calculus

Vec d = Fin d -> R carries the sup norm, so Mathlib's ‖·‖ on the carrier is not the Euclidean gauge in which spheres, radial functions and the Laplacian are written. CoarseGraining supplies the squared Euclidean gauge vecNormSq and the explicit balls euclideanBall/euclideanClosedBall built from it, but no norm and no differential calculus for it.

This module adds the norm euclideanNorm x = sqrt (vecNormSq x), its elementary comparison with the explicit balls, and -- the substantive part -- the coordinate derivative of a function of the Euclidean distance to a fixed centre. The derivative is expressed through coordFDeriv, the continuous linear functional v ↦ sum_i c i * v i, which is the only shape of Frechet derivative that occurs for the functions considered here and which evaluates on CoarseGraining's basisVec i to c i.

Everything is carrier-native: no EuclideanSpace transfer appears anywhere, and CoarseGraining's euclideanCoordDeriv i u x = fderiv R u x (basisVec i) is used as the definition of the coordinate derivative throughout.

Contents

• euclideanNorm, sq_euclideanNorm, euclideanNorm_pos, continuous_euclideanNorm -- the norm and its basic properties.
• mem_euclideanBall_iff_euclideanNorm_lt, mem_euclideanClosedBall_iff_euclideanNorm_le -- the explicit balls in terms of the norm.
• coord, coord -- the coordinate functionals.
• has, has, `has -- the derivative of the Euclidean gauge away from its centre.
• has, euclideanCoordDeriv_comp_euclideanNorm_sub-- the chain ruled_i (Phi (|x - z|)) = Phi' (|x - z|) * (x i - z i) / |x - z|`.

References

• ABK26, e.nablaw.oscillations (the eventual consumer).

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanNorm {d : ℕ} (x : HCPolySupport.Vec d) : ℝ

The Euclidean norm expressed through the squared vector norm.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanNorm x = √(HCPolySupport.vecNormSq x)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanNorm_nonneg {d : ℕ} (x : HCPolySupport.Vec d) : 0 ≤ euclideanNorm x

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.sq_euclideanNorm {d : ℕ} (x : HCPolySupport.Vec d) : euclideanNorm x ^ 2 = HCPolySupport.vecNormSq x

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanNorm_eq_zero_iff {d : ℕ} {x : HCPolySupport.Vec d} : euclideanNorm x = 0 ↔ x = 0

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanNorm_pos {d : ℕ} {x : HCPolySupport.Vec d} (hx : x ≠ 0) : 0 < euclideanNorm x

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.continuous_vecNormSq {d : ℕ} : Continuous HCPolySupport.vecNormSq

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.continuous_euclideanNorm {d : ℕ} : Continuous euclideanNorm

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanSqDist_eq_sq_euclideanNorm {d : ℕ} (x y : HCPolySupport.Vec d) : HCPolySupport.euclideanSqDist x y = euclideanNorm (x - y) ^ 2

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.mem_euclideanBall_iff_euclideanNorm_lt {d : ℕ} {z x : HCPolySupport.Vec d} {r : ℝ} (hr : 0 ≤ r) : x ∈ HCPolySupport.euclideanBall z r ↔ euclideanNorm (x - z) < r

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.mem_euclideanClosedBall_iff_euclideanNorm_le {d : ℕ} {z x : HCPolySupport.Vec d} {r : ℝ} (hr : 0 ≤ r) : x ∈ HCPolySupport.euclideanClosedBall z r ↔ euclideanNorm (x - z) ≤ r

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.Corrector.coordFDeriv {d : ℕ} (c : HCPolySupport.Vec d) : HCPolySupport.Vec d →L[ℝ] ℝ

The continuous linear functional with coordinate coefficient vector c.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.Corrector.coordFDeriv c = ∑ i : Fin d, c i • ContinuousLinearMap.proj i

@[simp]

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.coordFDeriv_apply {d : ℕ} (c v : HCPolySupport.Vec d) : (coordFDeriv c) v = ∑ i : Fin d, c i * v i

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.hasFDerivAt_vecNormSq {d : ℕ} (x : HCPolySupport.Vec d) : HasFDerivAt HCPolySupport.vecNormSq (coordFDeriv fun (i : Fin d) => 2 * x i) x

The derivative of the squared Euclidean norm.

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanCoordDeriv_of_hasFDerivAt {d : ℕ} {f : HCPolySupport.Vec d → ℝ} {L : HCPolySupport.Vec d →L[ℝ] ℝ} {x : HCPolySupport.Vec d} (h : HasFDerivAt f L x) (i : Fin d) : HCPolySupport.euclideanCoordDeriv i f x = L (HCPolySupport.basisVec i)

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.hasFDerivAt_vecNormSq_sub {d : ℕ} (z x : HCPolySupport.Vec d) : HasFDerivAt (fun (y : HCPolySupport.Vec d) => HCPolySupport.vecNormSq (y - z)) (coordFDeriv fun (i : Fin d) => 2 * (x i - z i)) x

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.hasFDerivAt_euclideanNorm_sub {d : ℕ} {z x : HCPolySupport.Vec d} (hx : x ≠ z) : HasFDerivAt (fun (y : HCPolySupport.Vec d) => euclideanNorm (y - z)) (coordFDeriv fun (i : Fin d) => (x i - z i) / euclideanNorm (x - z)) x

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.hasFDerivAt_comp_euclideanNorm_sub {d : ℕ} {Φ : ℝ → ℝ} {c : ℝ} {z x : HCPolySupport.Vec d} (hx : x ≠ z) (hΦ : HasDerivAt Φ c (euclideanNorm (x - z))) : HasFDerivAt (fun (y : HCPolySupport.Vec d) => Φ (euclideanNorm (y - z))) (coordFDeriv fun (i : Fin d) => c * ((x i - z i) / euclideanNorm (x - z))) x

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.euclideanCoordDeriv_comp_euclideanNorm_sub {d : ℕ} {Φ : ℝ → ℝ} {c : ℝ} {z x : HCPolySupport.Vec d} (hx : x ≠ z) (hΦ : HasDerivAt Φ c (euclideanNorm (x - z))) (i : Fin d) : HCPolySupport.euclideanCoordDeriv i (fun (y : HCPolySupport.Vec d) => Φ (euclideanNorm (y - z))) x = c * ((x i - z i) / euclideanNorm (x - z))

theorem Algsuperdiff.Section3.Provider.Diffusivity.Corrector.hasFDerivAt_coord_sub {d : ℕ} {z x : HCPolySupport.Vec d} (i : Fin d) : HasFDerivAt (fun (y : HCPolySupport.Vec d) => y i - z i) (coordFDeriv (HCPolySupport.basisVec i)) x