1. Physlib
  2. SpaceAndTime
  3. Space
  4. DistOfFunction
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.SpaceAndTime.Space.IsDistBounded public import Physlib.SpaceAndTime.Space.Derivatives.Basic public import Mathlib.MeasureTheory.SpecificCodomains.WithLp public import Physlib.Mathematics.Distribution.Basic

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. Derivatives

    E. Components

iv. References

@[expose] public section

A. Definition of a distribution from a function

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

All goals completed! 🐙
lemma distOfFunction_apply {d : ℕ} (f : Space d → F) (hf : IsDistBounded f) (η : 𝓢(Space d, ℝ)) : distOfFunction f hf η = ∫ x, η x • f x := rfl

B. Linarity properties of getting distributions from functions

@[simp] lemma distOfFunction_zero_eq_zero {d : ℕ} : distOfFunction (fun _ : Space d => (0 : F)) (𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕ⊢ IsDistBounded fun x => 0 All goals completed! 🐙) = 0 := F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕ⊢ distOfFunction (fun x => 0) ⋯ = 0 F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕη:𝓢(Space d, ℝ)⊢ (distOfFunction (fun x => 0) ⋯) η = 0 η All goals completed! 🐙All goals completed! 🐙All goals completed! 🐙lemma distOfFunction_mul_fun {d : ℕ} (f : Space d → ℝ) (hf : IsDistBounded f) (c : ℝ) : distOfFunction (fun x => c * f x) (𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕf:Space d → ℝhf:IsDistBounded fc:ℝ⊢ IsDistBounded fun x => c * f x All goals completed! 🐙) = c • distOfFunction f hf := d:ℕf:Space d → ℝhf:IsDistBounded fc:ℝ⊢ distOfFunction (fun x => c * f x) ⋯ = c • distOfFunction f hf All goals completed! 🐙lemma distOfFunction_neg {d : ℕ} (f : Space d → F) (hf : IsDistBounded (fun x => - f x)) : distOfFunction (fun x => - f x) hf = - distOfFunction f (𝕜:TypeE:TypeF:TypeF':Typeinst✝⁵:RCLike 𝕜inst✝⁴:NormedAddCommGroup Einst✝³:NormedAddCommGroup Finst✝²:NormedAddCommGroup F'inst✝¹:NormedSpace ℝ Einst✝:NormedSpace ℝ Fd:ℕf:Space d → Fhf:IsDistBounded fun x => -f x⊢ IsDistBounded f All goals completed! 🐙) := F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fhf:IsDistBounded fun x => -f x⊢ distOfFunction (fun x => -f x) hf = -distOfFunction f ⋯ convert distOfFunction_smul_fun f (F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fhf:IsDistBounded fun x => -f x⊢ IsDistBounded f All goals completed! 🐙) (-1) using 1 F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fhf:IsDistBounded fun x => -f x⊢ distOfFunction (fun x => -f x) hf = distOfFunction (fun x => -1 • f x) ⋯ All goals completed! 🐙 F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕf:Space d → Fhf:IsDistBounded fun x => -f x⊢ -distOfFunction f ⋯ = -1 • distOfFunction f ⋯ All goals completed! 🐙

C. Properties related to inner products

d:ℕn:ℕf:Space d → EuclideanSpace ℝ (Fin n)hf:IsDistBounded fη:𝓢(Space d, ℝ)y:EuclideanSpace ℝ (Fin n)⊢ Integrable (fun x => η x • f x) volume All goals completed! 🐙

D. Derivatives

The distributional spatial derivative of the distribution associated to a differentiable function is the distribution associated to the corresponding pointwise spatial derivative.

F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕμ:Fin df:Space d → Fhf:IsDistBounded fhf_deriv:IsDistBounded (deriv μ f)hf_diff:Differentiable ℝ fη:𝓢(Space d, ℝ)⊢ Integrable (fun x => (fderiv ℝ (⇑η) x) (basis μ) • f x) volumeF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕμ:Fin df:Space d → Fhf:IsDistBounded fhf_deriv:IsDistBounded (deriv μ f)hf_diff:Differentiable ℝ fη:𝓢(Space d, ℝ)⊢ Integrable (fun x => η x • (fderiv ℝ f x) (basis μ)) volumeF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕμ:Fin df:Space d → Fhf:IsDistBounded fhf_deriv:IsDistBounded (deriv μ f)hf_diff:Differentiable ℝ fη:𝓢(Space d, ℝ)⊢ Integrable (fun x => η x • f x) volumeF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕμ:Fin df:Space d → Fhf:IsDistBounded fhf_deriv:IsDistBounded (deriv μ f)hf_diff:Differentiable ℝ fη:𝓢(Space d, ℝ)⊢ ∀ x ∈ tsupport f, DifferentiableAt ℝ (⇑η) xF:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕμ:Fin df:Space d → Fhf:IsDistBounded fhf_deriv:IsDistBounded (deriv μ f)hf_diff:Differentiable ℝ fη:𝓢(Space d, ℝ)⊢ ∀ x ∈ tsupport ⇑η, DifferentiableAt ℝ f x F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕμ:Fin df:Space d → Fhf:IsDistBounded fhf_deriv:IsDistBounded (deriv μ f)hf_diff:Differentiable ℝ fη:𝓢(Space d, ℝ)⊢ Integrable (fun x => (fderiv ℝ (⇑η) x) (basis μ) • f x) volume All goals completed! 🐙 F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕμ:Fin df:Space d → Fhf:IsDistBounded fhf_deriv:IsDistBounded (deriv μ f)hf_diff:Differentiable ℝ fη:𝓢(Space d, ℝ)⊢ Integrable (fun x => η x • (fderiv ℝ f x) (basis μ)) volume All goals completed! 🐙 F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕμ:Fin df:Space d → Fhf:IsDistBounded fhf_deriv:IsDistBounded (deriv μ f)hf_diff:Differentiable ℝ fη:𝓢(Space d, ℝ)⊢ Integrable (fun x => η x • f x) volume All goals completed! 🐙 F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕμ:Fin df:Space d → Fhf:IsDistBounded fhf_deriv:IsDistBounded (deriv μ f)hf_diff:Differentiable ℝ fη:𝓢(Space d, ℝ)⊢ ∀ x ∈ tsupport f, DifferentiableAt ℝ (⇑η) x All goals completed! 🐙 F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕμ:Fin df:Space d → Fhf:IsDistBounded fhf_deriv:IsDistBounded (deriv μ f)hf_diff:Differentiable ℝ fη:𝓢(Space d, ℝ)⊢ ∀ x ∈ tsupport ⇑η, DifferentiableAt ℝ f x F:Typeinst✝¹:NormedAddCommGroup Finst✝:NormedSpace ℝ Fd:ℕμ:Fin df:Space d → Fhf:IsDistBounded fhf_deriv:IsDistBounded (deriv μ f)hf_diff:Differentiable ℝ fη:𝓢(Space d, ℝ)x:Space da✝:x ∈ tsupport ⇑η⊢ DifferentiableAt ℝ f x All goals completed! 🐙

E. Components

d:ℕn:ℕf:Space d → EuclideanSpace ℝ (Fin n)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin n⊢ ∫ (x : Space d), (η x • f x).ofLp i = ∫ (x : Space d), η x * (f x).ofLp id:ℕn:ℕf:Space d → EuclideanSpace ℝ (Fin n)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin n⊢ ∀ (i : Fin n), Integrable (fun x => (η x • f x).ofLp i) volume d:ℕn:ℕf:Space d → EuclideanSpace ℝ (Fin n)hf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin n⊢ ∀ (i : Fin n), Integrable (fun x => (η x • f x).ofLp i) volume d:ℕn:ℕf:Space d → EuclideanSpace ℝ (Fin n)hf:IsDistBounded fη:𝓢(Space d, ℝ)i✝:Fin ni:Fin n⊢ Integrable (fun x => (η x • f x).ofLp i) volume d:ℕn:ℕf:Space d → EuclideanSpace ℝ (Fin n)hf:IsDistBounded fη:𝓢(Space d, ℝ)i✝:Fin ni:Fin n⊢ Integrable (fun x => η x * (f x).ofLp i) volume All goals completed! 🐙d:ℕn:ℕf:Space d → Lorentz.Vector nhf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin 1 ⊕ Fin n⊢ ∫ (x : Space d), ⟪Lorentz.Vector.basis i, η x • f x⟫_ℝ = ∫ (x : Space d), η x * f x id:ℕn:ℕf:Space d → Lorentz.Vector nhf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin 1 ⊕ Fin n⊢ Integrable (fun x => η x • f x) volume d:ℕn:ℕf:Space d → Lorentz.Vector nhf:IsDistBounded fη:𝓢(Space d, ℝ)i:Fin 1 ⊕ Fin n⊢ Integrable (fun x => η x • f x) volume All goals completed! 🐙