Variational adjoint derivative

Variational adjoint derivative of F at u is a generalization of (fderiv ℝ F u).adjoint to function spaces. In particular, variational gradient is an analog of gradient F u := (fderiv ℝ F u).adjoint 1.

The definition of HasVarAdjDerivAt is constructed exactly such that we can prove composition theorem saying

  HasVarAdjDerivAt F F' (G u)) → HasVarAdjDerivAt G G' u →
    HasVarAdjDerivAt (F ∘ G) (G' ∘ F') u

This theorem is the main tool to mechanistically compute variational gradient.

structure HasVarAdjDerivAt {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) (u : X → U) : Prop

This is analogue of saying F' = (fderiv ℝ F u).adjoint.

This definition is useful as we can prove composition theorem for it and HasVarGradient F grad u can be computed by grad := F' (fun _ => 1).

• smooth_at : ContDiff ℝ (↑⊤) u
• diff (φ : ℝ → X → U) : ContDiff ℝ ↑⊤ ↿φ → ContDiff ℝ ↑⊤ fun (sx : ℝ × Y) => F (φ sx.1) sx.2
• linearize (φ : ℝ → X → U) : ContDiff ℝ ↑⊤ ↿φ → ∀ (x : Y), deriv (fun (s' : ℝ) => F (φ s') x) 0 = deriv (fun (s' : ℝ) => F (fun (x : X) => φ 0 x + s' • deriv (fun (x_1 : ℝ) => φ x_1 x) 0) x) 0
• adjoint : HasVarAdjoint (fun (δu : X → U) (x : Y) => deriv (fun (s : ℝ) => F (fun (x' : X) => u x' + s • δu x') x) 0) F'

theorem HasVarAdjDerivAt.apply_smooth_of_smooth {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} {u v : X → U} (h : HasVarAdjDerivAt F F' u) (hv : ContDiff ℝ (↑⊤) v) : ContDiff ℝ (↑⊤) (F v)

theorem HasVarAdjDerivAt.apply_smooth_self {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} {u : X → U} (h : HasVarAdjDerivAt F F' u) : ContDiff ℝ (↑⊤) (F u)

theorem HasVarAdjDerivAt.smooth_R {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} {u : X → U} (h : HasVarAdjDerivAt F F' u) {φ : ℝ → X → U} (hφ : ContDiff ℝ ↑⊤ ↿φ) (x : X) : ContDiff ℝ ↑⊤ fun (s : ℝ) => F (fun (x' : X) => φ s x') x

theorem HasVarAdjDerivAt.smooth_linear {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] {x : X} {F : (X → U) → X → V} {F' : (X → V) → X → U} {u : X → U} (h : HasVarAdjDerivAt F F' u) {φ : ℝ → X → U} (hφ : ContDiff ℝ ↑⊤ ↿φ) : ContDiff ℝ ↑⊤ fun (s' : ℝ) => F (fun (x : X) => φ 0 x + s' • deriv (fun (x_1 : ℝ) => φ x_1 x) 0) x

theorem HasVarAdjDerivAt.differentiable_linear {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} {u : X → U} (h : HasVarAdjDerivAt F F' u) {φ : ℝ → X → U} (hφ : ContDiff ℝ ↑⊤ ↿φ) (x : X) : Differentiable ℝ fun (s' : ℝ) => F (fun (x : X) => φ 0 x + s' • deriv (fun (x_1 : ℝ) => φ x_1 x) 0) x

theorem HasVarAdjDerivAt.id {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {U : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] (u : X → U) (hu : ContDiff ℝ (↑⊤) u) : HasVarAdjDerivAt (fun (φ : X → U) => φ) (fun (ψ : X → U) => ψ) u

theorem HasVarAdjDerivAt.const {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] (u : X → U) (v : X → V) (hu : ContDiff ℝ (↑⊤) u) (hv : ContDiff ℝ (↑⊤) v) : HasVarAdjDerivAt (fun (x : X → U) => v) (fun (x : X → V) => 0) u

theorem HasVarAdjDerivAt.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} {u : X → U} {F' : (Z → W) → Y → V} {G' : (Y → V) → X → U} (hF : HasVarAdjDerivAt F F' (G u)) (hG : HasVarAdjDerivAt G G' u) : HasVarAdjDerivAt (fun (u : X → U) => F (G u)) (fun (ψ : Z → W) => G' (F' ψ)) u

theorem HasVarAdjDerivAt.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] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] [MeasureTheory.volume.IsOpenPosMeasure] [OpensMeasurableSpace X] (F : (X → U) → Y → V) (u : X → U) (F' G' : (Y → V) → X → U) (hF : HasVarAdjDerivAt F F' u) (hG : HasVarAdjDerivAt F G' u) (φ : Y → V) (hφ : IsTestFunction φ) : F' φ = G' φ

theorem HasVarAdjDerivAt.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] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] [MeasureTheory.volume.IsOpenPosMeasure] {Y : Type u_2} [NormedAddCommGroup Y] [InnerProductSpace ℝ Y] [FiniteDimensional ℝ Y] [MeasureTheory.MeasureSpace Y] {F : (X → U) → Y → V} {u : X → U} {F' G' : (Y → V) → X → U} (hF : HasVarAdjDerivAt F F' u) (hG : HasVarAdjDerivAt F G' u) (φ : Y → V) (hφ : ContDiff ℝ (↑⊤) φ) : F' φ = G' φ

theorem HasVarAdjDerivAt.deriv' (u : ℝ → ℝ) (hu : ContDiff ℝ (↑⊤) u) : HasVarAdjDerivAt (fun (φ : ℝ → ℝ) => deriv φ) (fun (φ : ℝ → ℝ) (x : ℝ) => -deriv φ x) u

theorem HasVarAdjDerivAt.deriv {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] (F : (ℝ → U) → ℝ → ℝ) (F' : (ℝ → ℝ) → ℝ → U) (u : ℝ → U) (hF : HasVarAdjDerivAt F F' u) : HasVarAdjDerivAt (fun (φ : ℝ → U) => deriv (F φ)) (fun (ψ : ℝ → ℝ) (x : ℝ) => F' (fun (x' : ℝ) => -deriv ψ x') x) u

theorem HasVarAdjDerivAt.fmap {X : Type u_3} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] [InnerProductSpace' ℝ U] {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [InnerProductSpace' ℝ V] [CompleteSpace U] [CompleteSpace V] (f : X → U → V) {f' : X → U → V → U} (u : X → U) (hu : ContDiff ℝ (↑⊤) u) (hf' : ContDiff ℝ ↑⊤ ↿f) (hf : ∀ (x : X) (u : U), HasAdjFDerivAt ℝ (f x) (f' x u) u) : HasVarAdjDerivAt (fun (φ : X → U) (x : X) => f x (φ x)) (fun (ψ : X → V) (x : X) => f' x (u x) (ψ x)) u

theorem HasVarAdjDerivAt.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) (u : X → U) (hF : HasVarAdjDerivAt F F' u) : HasVarAdjDerivAt (fun (φ : X → U) (x : X) => -F φ x) (fun (ψ : X → V) (x : X) => -F' ψ x) u

theorem HasVarAdjDerivAt.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) (u : X → U) (hF : HasVarAdjDerivAt F F' u) (hG : HasVarAdjDerivAt G G' u) : HasVarAdjDerivAt (fun (φ : X → U) (x : X) => F φ x + G φ x) (fun (ψ : X → V) (x : X) => F' ψ x + G' ψ x) u

theorem HasVarAdjDerivAt.mul {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [MeasureTheory.MeasureSpace X] [OpensMeasurableSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts MeasureTheory.volume] (F G F' G' : (X → ℝ) → X → ℝ) (u : X → ℝ) (hF : HasVarAdjDerivAt F F' u) (hG : HasVarAdjDerivAt G G' u) : HasVarAdjDerivAt (fun (φ : X → ℝ) (x : X) => F φ x * G φ x) (fun (ψ : X → ℝ) (x : X) => F' (fun (x' : X) => ψ x' * G u x') x + G' (fun (x' : X) => F u x' * ψ x') x) u