Variational adjoint

Definition of adjoint of linear function between function spaces. It is inspired by the definition of distributional adjoint of linear maps between test functions as described here: https://en.wikipedia.org/wiki/Distribution_(mathematics) under 'Preliminaries: Transpose of a linear operator' but we require that the adjoint is function between test functions too.

The key results are:

• variational adjoint is unique on test functions
• variational adjoint of identity is identity, HasVarAdjoint.id
• variational adjoint of composition is composition of adjoint in reverse order, HasVarAdjoint.comp
• variational adjoint of deriv is - deriv, HasVarAdjoint.deriv
• variational adjoint of algebraic operations is algebraic operation of adjoints, HasVarAdjoint.neg, HasVarAdjoint.add, HasVarAdjoint.sub, HasVarAdjoint.mul_left, HasVarAdjoint.mul_right, HasVarAdjoint.smul_left, HasVarAdjoint.smul_right

def IsLocalizedFunctionTransform {X : Type u_1} [NormedAddCommGroup X] {Y : Type u_2} [NormedAddCommGroup Y] {U : Type u_3} {V : Type 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

structure HasVarAdjoint {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [MeasureTheory.MeasureSpace Y] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] (F : (X → U) → Y → V) (F' : (Y → V) → X → U) : Prop

Map F from (X → U) to (X → V) has a variational adjoint F' if it preserves test functions and satisfies the adjoint relation ⟪F φ, ψ⟫ = ⟪φ, F' ψ⟫for all test functions φ and ψ for ⟪φ, ψ⟫ = ∫ x, ⟪φ x, ψ x⟫_ℝ ∂μ.

The canonical example is the function F = deriv that has adjoint F' = - deriv.

This notion of adjoint allows us to do formally variational calculus as often encountered in physics textbooks. In mathematical literature, the adjoint is often defined for unbounded operators, but such formal treatement is unnecessarily complicated for physics applications.

• test_fun_preserving (φ : X → U) : IsTestFunction φ → IsTestFunction (F φ)
• test_fun_preserving' (φ : Y → V) : IsTestFunction φ → IsTestFunction (F' φ)
• adjoint (φ : X → U) (ψ : Y → V) : IsTestFunction φ → IsTestFunction ψ → ∫ (y : Y), inner ℝ (F φ y) (ψ y) = ∫ (x : X), inner ℝ (φ x) (F' ψ x)
• ext : IsLocalizedFunctionTransform F'

theorem HasVarAdjoint.id {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] : HasVarAdjoint (fun (φ : X → U) => φ) fun (φ : X → U) => φ

theorem HasVarAdjoint.zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [MeasureTheory.MeasureSpace Y] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] : HasVarAdjoint (fun (x : X → U) (x : Y) => 0) fun (x : Y → V) (x : X) => 0

theorem HasVarAdjoint.comp {X : Type u_5} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {Y : Type u_1} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [MeasureTheory.MeasureSpace Y] {Z : Type u_2} [NormedAddCommGroup Z] [NormedSpace ℝ Z] [MeasureTheory.MeasureSpace Z] {U : Type u_6} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] {W : Type u_4} [NormedAddCommGroup W] [NormedSpace ℝ W] [InnerProductSpace' ℝ W] {F : (Y → V) → Z → W} {G : (X → U) → Y → V} {F' : (Z → W) → Y → V} {G' : (Y → V) → X → U} (hF : HasVarAdjoint F F') (hG : HasVarAdjoint G G') : HasVarAdjoint (fun (φ : X → U) => F (G φ)) fun (φ : Z → W) => G' (F' φ)

theorem HasVarAdjoint.deriv : HasVarAdjoint (fun (φ : ℝ → ℝ) => deriv φ) fun (φ : ℝ → ℝ) (x : ℝ) => -deriv φ x

theorem HasVarAdjoint.congr_fun {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [MeasureTheory.MeasureSpace Y] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] {F G : (X → U) → Y → V} {F' : (Y → V) → X → U} (h : HasVarAdjoint G F') (h' : ∀ (φ : X → U), IsTestFunction φ → F φ = G φ) : HasVarAdjoint F F'

theorem HasVarAdjoint.unique_on_test_functions {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {Y : Type u_2} [NormedAddCommGroup Y] [NormedSpace ℝ Y] [MeasureTheory.MeasureSpace Y] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] {F : (X → U) → Y → V} {F' G' : (Y → V) → X → U} [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] [MeasureTheory.volume.IsOpenPosMeasure] [OpensMeasurableSpace X] (hF' : HasVarAdjoint F F') (hG' : HasVarAdjoint F G') (φ : Y → V) : IsTestFunction φ → F' φ = G' φ

Variational adjoint is unique only when applied to test functions.

theorem HasVarAdjoint.unique {U : Type u_3} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] {X : Type u_1} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [MeasureTheory.MeasureSpace X] [OpensMeasurableSpace X] {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [FiniteDimensional ℝ Y] [MeasureTheory.MeasureSpace Y] {F : (X → U) → Y → V} {F' G' : (Y → V) → X → U} [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] [MeasureTheory.volume.IsOpenPosMeasure] (hF : HasVarAdjoint F F') (hG : HasVarAdjoint F G') (f : Y → V) : ContDiff ℝ (↑⊤) f → F' f = G' f

Variational adjoint is unique only when applied to smooth functions.

theorem HasVarAdjoint.neg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] {F : (X → U) → X → V} {F' : (X → V) → X → U} (hF : HasVarAdjoint F F') : HasVarAdjoint (fun (φ : X → U) (x : X) => -F φ x) fun (φ : X → V) (x : X) => -F' φ x

theorem HasVarAdjoint.add {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] [OpensMeasurableSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {F G : (X → U) → X → V} {F' G' : (X → V) → X → U} (hF : HasVarAdjoint F F') (hG : HasVarAdjoint G G') : HasVarAdjoint (fun (φ : X → U) (x : X) => F φ x + G φ x) fun (φ : X → V) (x : X) => F' φ x + G' φ x

theorem HasVarAdjoint.sub {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] [OpensMeasurableSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] {F G : (X → U) → X → V} {F' G' : (X → V) → X → U} (hF : HasVarAdjoint F F') (hG : HasVarAdjoint G G') : HasVarAdjoint (fun (φ : X → U) (x : X) => F φ x - G φ x) fun (φ : X → V) (x : X) => F' φ x - G' φ x

theorem HasVarAdjoint.mul_left {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {F : (X → ℝ) → X → ℝ} {ψ : X → ℝ} {F' : (X → ℝ) → X → ℝ} (hF : HasVarAdjoint F F') (hψ : ContDiff ℝ (↑⊤) ψ) : HasVarAdjoint (fun (φ : X → ℝ) (x : X) => ψ x * F φ x) fun (φ : X → ℝ) (x : X) => F' (fun (x : X) => ψ x * φ x) x

theorem HasVarAdjoint.mul_right {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {F : (X → ℝ) → X → ℝ} {ψ : X → ℝ} {F' : (X → ℝ) → X → ℝ} (hF : HasVarAdjoint F F') (hψ : ContDiff ℝ (↑⊤) ψ) : HasVarAdjoint (fun (φ : X → ℝ) (x : X) => F φ x * ψ x) fun (φ : X → ℝ) (x : X) => F' (fun (x : X) => φ x * ψ x) x

theorem HasVarAdjoint.smul_left {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] {F : (X → U) → X → V} {ψ : X → ℝ} {F' : (X → V) → X → U} (hF : HasVarAdjoint F F') (hψ : ContDiff ℝ (↑⊤) ψ) : HasVarAdjoint (fun (φ : X → U) (x : X) => ψ x • F φ x) fun (φ : X → V) (x : X) => F' (fun (x' : X) => ψ x' • φ x') x

theorem HasVarAdjoint.smul_right {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] {V : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] {F : (X → U) → X → V} {ψ : X → ℝ} {F' : (X → V) → X → U} (hF : HasVarAdjoint F F') (hψ : ContDiff ℝ (↑⊤) ψ) : HasVarAdjoint (fun (φ : X → U) (x : X) => ψ x • F φ x) fun (φ : X → V) (x : X) => F' (fun (x' : X) => ψ x' • φ x') x