Radial functions

A function on a space equipped with a norm is radial if its value at a point depends only on the norm of that point, that is, if it factors through the norm. This file introduces the predicate Function.IsRadial and develops basic API.

Main definitions

• Function.IsRadial: the predicate stating that f : E → F factors through ‖·‖ : E → ℝ.
• Function.radialPart: a choice of function ℝ → F through which f : E → F factors; it satisfies f = f.radialPart ∘ (‖·‖) precisely when f is radial.

Tags

radial function, radially symmetric

def Function.IsRadial {E : Type u_2} {F : Type u_3} [Norm E] (f : E → F) : Prop

A function on a space with a norm is radial if it factors through the norm.

Equations

• Function.IsRadial f = Function.FactorsThrough f fun (x : E) => ‖x‖

theorem Function.isRadial_def {E : Type u_2} {F : Type u_3} [Norm E] (f : E → F) : IsRadial f ↔ ∀ {x y : E}, ‖x‖ = ‖y‖ → f x = f y

noncomputable def Function.radialPart {E : Type u_2} {F : Type u_3} [Norm E] [hF : Nonempty F] (f : E → F) : ℝ → F

The radial part of a function. If f is radial, then f = f.radialPart ∘ (‖·‖).

Equations

• Function.radialPart f = Function.extend (fun (x : E) => ‖x‖) f fun (x : ℝ) => Classical.choice hF

@[simp]

theorem Function.IsRadial.radialPart_norm {E : Type u_2} {F : Type u_3} [Norm E] [Nonempty F] {f : E → F} (hf : IsRadial f) {x : E} : radialPart f ‖x‖ = f x

theorem Function.IsRadial.even {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] {f : E → F} (hf : IsRadial f) : Function.Even f

theorem Function.IsRadial.comp_right {D : Type u_1} {E : Type u_2} {F : Type u_3} [Norm D] {f : D → E} {g : E → F} (hf : IsRadial f) : IsRadial (g ∘ f)

theorem Function.IsRadial.comp_isometry {E : Type u_2} {F : Type u_3} [SeminormedAddGroup E] {f : E → F} (hf : IsRadial f) {g : E → E} (hg : Isometry g) (hg₀ : g 0 = 0) : f ∘ g = f

theorem Function.isRadial_norm (E : Type u_2) [Norm E] : IsRadial fun (x : E) => ‖x‖

theorem Function.IsRadial.comp_norm {E : Type u_2} {F : Type u_3} [Norm E] (g : ℝ → F) : IsRadial (g ∘ fun (x : E) => ‖x‖)

theorem Function.isRadial_norm_sq (E : Type u_2) [Norm E] : IsRadial fun (x : E) => ‖x‖ ^ 2