Distributions from functions on space

i. Overview

In this module we define distributions on space constructed from functions f : Space d → F satisfying the condition IsDistBounded f.

This gives a convenient way to construct distributions from functions, without needing to reference the underlying Schwartz maps.

ii. Key results

• distOfFunction f hf : The distribution on space constructed from the function f : Space d → F satisfying the IsDistBounded f condition.

iii. Table of contents

• A. Definition of a distribution from a function
• B. Linarity properties of getting distributions from functions
• C. Properties related to inner products
• D. Components

iv. References

A. Definition of a distribution from a function

def Space.distOfFunction {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} (f : Space d → F) (hf : IsDistBounded f) : (Space d)→d[ℝ] F

A distribution Space d →d[ℝ] F from a function f : Space d → F which satisfies the IsDistBounded f condition.

Equations

• Space.distOfFunction f hf = SchwartzMap.mkCLMtoNormedSpace (fun (η : SchwartzMap (Space d) ℝ) => ∫ (x : Space d), η x • f x) ⋯ ⋯ ⋯

theorem Space.distOfFunction_apply {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} (f : Space d → F) (hf : IsDistBounded f) (η : SchwartzMap (Space d) ℝ) : (distOfFunction f hf) η = ∫ (x : Space d), η x • f x

B. Linarity properties of getting distributions from functions

@[simp]

theorem Space.distOfFunction_zero_eq_zero {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} : distOfFunction (fun (x : Space d) => 0) ⋯ = 0

theorem Space.distOfFunction_smul {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} (f : Space d → F) (hf : IsDistBounded f) (c : ℝ) : distOfFunction (c • f) ⋯ = c • distOfFunction f hf

theorem Space.distOfFunction_smul_fun {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} (f : Space d → F) (hf : IsDistBounded f) (c : ℝ) : distOfFunction (fun (x : Space d) => c • f x) ⋯ = c • distOfFunction f hf

theorem Space.distOfFunction_mul_fun {d : ℕ} (f : Space d → ℝ) (hf : IsDistBounded f) (c : ℝ) : distOfFunction (fun (x : Space d) => c * f x) ⋯ = c • distOfFunction f hf

theorem Space.distOfFunction_neg {F : Type} [NormedAddCommGroup F] [NormedSpace ℝ F] {d : ℕ} (f : Space d → F) (hf : IsDistBounded fun (x : Space d) => -f x) : distOfFunction (fun (x : Space d) => -f x) hf = -distOfFunction f ⋯

C. Properties related to inner products

theorem Space.distOfFunction_inner {d n : ℕ} (f : Space d → EuclideanSpace ℝ (Fin n)) (hf : IsDistBounded f) (η : SchwartzMap (Space d) ℝ) (y : EuclideanSpace ℝ (Fin n)) : inner ℝ ((distOfFunction f hf) η) y = ∫ (x : Space d), η x * inner ℝ (f x) y

D. Components

theorem Space.distOfFunction_eculid_eval {d n : ℕ} (f : Space d → EuclideanSpace ℝ (Fin n)) (hf : IsDistBounded f) (η : SchwartzMap (Space d) ℝ) (i : Fin n) : ((distOfFunction f hf) η).ofLp i = (distOfFunction (fun (x : Space d) => (f x).ofLp i) ⋯) η

theorem Space.distOfFunction_vector_eval {d n : ℕ} (f : Space d → Lorentz.Vector n) (hf : IsDistBounded f) (η : SchwartzMap (Space d) ℝ) (i : Fin 1 ⊕ Fin n) : (distOfFunction f hf) η i = (distOfFunction (fun (x : Space d) => f x i) ⋯) η