Localized function transforms

In this module we define a locality property for function transforms, F : (X → U) → (Y → V). The locality property IsLocalizedFunctionTransform, says that for every compact set K in Y there exists a compact set L of X, such that if φ and φ' are equal on L, then F φ and F φ' are equal on K.

def IsLocalizedFunctionTransform {X : Type u_1} [NormedAddCommGroup X] {Y : Type u_2} [NormedAddCommGroup Y] {U : Sort u_3} {V : Sort u_4} (F : (X → U) → Y → V) : Prop

Function transformation F is localizable if the values of the transformed function F φ on some compact set K can depend only on the values of φ on some another compact set L.

Equations

• IsLocalizedFunctionTransform F = ∀ (K : Set Y), IsCompact K → ∃ (L : Set X), IsCompact L ∧ ∀ (φ φ' : X → U), (∀ x ∈ L, φ x = φ' x) → ∀ x ∈ K, F φ x = F φ' x

theorem IsLocalizedFunctionTransform.comp {X : Type u_5} [NormedAddCommGroup X] {Y : Type u_1} [NormedAddCommGroup Y] {Z : Type u_2} [NormedAddCommGroup Z] {U : Sort u_6} {V : Sort u_3} {W : Sort u_4} {F : (Y → V) → Z → W} {G : (X → U) → Y → V} (hF : IsLocalizedFunctionTransform F) (hG : IsLocalizedFunctionTransform G) : IsLocalizedFunctionTransform (F ∘ G)

theorem IsLocalizedFunctionTransform.fun_comp {X : Type u_5} [NormedAddCommGroup X] {Y : Type u_1} [NormedAddCommGroup Y] {Z : Type u_2} [NormedAddCommGroup Z] {U : Sort u_6} {V : Sort u_3} {W : Sort u_4} {F : (Y → V) → Z → W} {G : (X → U) → Y → V} (hF : IsLocalizedFunctionTransform F) (hG : IsLocalizedFunctionTransform G) : IsLocalizedFunctionTransform fun (x : X → U) => F (G x)

@[simp]

theorem IsLocalizedFunctionTransform.id {Y : Type u_1} [NormedAddCommGroup Y] {V : Sort u_2} : IsLocalizedFunctionTransform _root_.id

theorem IsLocalizedFunctionTransform.neg {X : Type u_2} [NormedAddCommGroup X] {Y : Type u_3} [NormedAddCommGroup Y] {U : Sort u_4} {V : Type u_1} [NormedAddCommGroup V] {F : (X → U) → Y → V} (hF : IsLocalizedFunctionTransform F) : IsLocalizedFunctionTransform fun (φ : X → U) => -F φ

theorem IsLocalizedFunctionTransform.add {X : Type u_2} [NormedAddCommGroup X] {Y : Type u_3} [NormedAddCommGroup Y] {U : Sort u_4} {V : Type u_1} [NormedAddCommGroup V] {F G : (X → U) → Y → V} (hF : IsLocalizedFunctionTransform F) (hG : IsLocalizedFunctionTransform G) : IsLocalizedFunctionTransform fun (φ : X → U) => F φ + G φ

theorem IsLocalizedFunctionTransform.mul_left {X : Type u_1} [NormedAddCommGroup X] {F : (X → ℝ) → X → ℝ} {ψ : X → ℝ} (hF : IsLocalizedFunctionTransform F) : IsLocalizedFunctionTransform fun (φ : X → ℝ) (x : X) => ψ x * F φ x

theorem IsLocalizedFunctionTransform.mul_right {X : Type u_1} [NormedAddCommGroup X] {F : (X → ℝ) → X → ℝ} {ψ : X → ℝ} (hF : IsLocalizedFunctionTransform F) : IsLocalizedFunctionTransform fun (φ : X → ℝ) (x : X) => F φ x * ψ x

theorem IsLocalizedFunctionTransform.smul_left {X : Type u_2} [NormedAddCommGroup X] {U : Sort u_3} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {F : (X → U) → X → V} {ψ : X → ℝ} (hF : IsLocalizedFunctionTransform F) : IsLocalizedFunctionTransform fun (φ : X → U) (x : X) => ψ x • F φ x

theorem IsLocalizedFunctionTransform.div {d : ℕ} : IsLocalizedFunctionTransform fun (φ : Space d → Space d) (x : Space d) => Space.div φ x

theorem IsLocalizedFunctionTransform.grad {d : ℕ} : IsLocalizedFunctionTransform fun (ψ : Space d → ℝ) (x : Space d) => Space.grad ψ x

theorem IsLocalizedFunctionTransform.gradient {d : ℕ} : IsLocalizedFunctionTransform fun (ψ : Space d → ℝ) (x : Space d) => _root_.gradient ψ x

theorem IsLocalizedFunctionTransform.clm_apply {X : Type u_3} [NormedAddCommGroup X] {U : Type u_2} {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup U] [NormedSpace ℝ U] (f : X → U →L[ℝ] V) : IsLocalizedFunctionTransform fun (φ : X → U) (x : X) => (f x) (φ x)

theorem IsLocalizedFunctionTransform.deriv {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] : IsLocalizedFunctionTransform fun (φ : ℝ → U) => _root_.deriv φ

theorem IsLocalizedFunctionTransform.fderiv {X : Type u_2} [NormedAddCommGroup X] {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedSpace ℝ X] [ProperSpace X] {dx : X} : IsLocalizedFunctionTransform fun (φ : X → U) (x : X) => (_root_.fderiv ℝ φ x) dx

theorem IsLocalizedFunctionTransform.fst {X : Type u_3} [NormedAddCommGroup X] {U : Sort u_4} {V : Type u_2} {W : Type u_1} {F : (X → U) → X → W × V} (hF : IsLocalizedFunctionTransform F) : IsLocalizedFunctionTransform fun (φ : X → U) (x : X) => (F φ x).1

theorem IsLocalizedFunctionTransform.snd {X : Type u_3} [NormedAddCommGroup X] {U : Sort u_4} {V : Type u_2} {W : Type u_1} {F : (X → U) → X → W × V} (hF : IsLocalizedFunctionTransform F) : IsLocalizedFunctionTransform fun (φ : X → U) (x : X) => (F φ x).2

theorem IsLocalizedFunctionTransform.prod {X : Type u_2} [NormedAddCommGroup X] {U : Sort u_3} {V : Type u_4} {W : Type u_1} {F : (X → U) → X → W} {G : (X → U) → X → V} (hF : IsLocalizedFunctionTransform F) (hG : IsLocalizedFunctionTransform G) : IsLocalizedFunctionTransform fun (φ : X → U) (x : X) => (F φ x, G φ x)

theorem IsLocalizedFunctionTransform.adjFDeriv {X : Type u_1} [NormedAddCommGroup X] {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] {dy : Y} [NormedSpace ℝ X] [ProperSpace X] [InnerProductSpace' ℝ X] [InnerProductSpace' ℝ Y] : IsLocalizedFunctionTransform fun (φ : X → Y) (x : X) => _root_.adjFDeriv ℝ φ x dy