..

SciLean/Core/Distribution/ParametricDistribRevDeriv.lean

@@ -27,12 +27,14 @@ set_default_scalar R
 noncomputable
 def parDistribRevDeriv (f : X → 𝒟'(Y,Z)) (x : X) : 𝒟'(Y,Z×(Z→X)) :=
   ⟨fun φ =>
-      let dz := semiAdjoint R (fun dx => parDistribDeriv f x dx φ)
+      let dz := semiAdjoint R (fun dx => cderiv R (f · φ) x dx)
       let z  := f x φ
       (z, dz), sorry_proof⟩
 
+
 namespace parDistribRevDeriv
 
+
 theorem comp_rule
     (f : Y → 𝒟'(Z,U)) (g : X → Y)
     (hf : DistribDifferentiable f) (hg : HasAdjDiff R g) :
@@ -41,17 +43,19 @@ theorem comp_rule
     fun x =>
       let ydg := revDeriv R g x
       let udf := parDistribRevDeriv f ydg.1
-      udf.postComp (⟨fun (u,df') => (u, fun du => ydg.2 (df' du)), sorry_proof⟩) := by
+      udf.postComp (⟨fun (u,df') => (u, fun du => ydg.2 (df' du)), by sorry_proof⟩) := by
 
   unfold parDistribRevDeriv postComp
   funext x; ext φ
   simp
   fun_trans
   simp [action_push,revDeriv,fwdDeriv]
   have : ∀ x, HasSemiAdjoint R (∂ x':=x, f x' φ) := sorry_proof -- todo add: `DistribHasAdjDiff`
+  have : ∀ φ, CDifferentiable R fun x0 => (f x0) φ := sorry_proof
   fun_trans
 
 
+
 theorem bind_rule
     (f : X → Y → 𝒟'(Z,V)) (g : X → 𝒟'(Y,U)) (L : U ⊸ V ⊸ W) :
     parDistribRevDeriv (fun x => (g x).bind (f x) L)
@@ -84,7 +88,7 @@ def diracRevDeriv (x : X) : 𝒟'(X,R×(R→X)) :=
 @[fun_trans]
 theorem dirac.arg_xy.parDistribRevDeriv_rule
     (x : W → X) (hx : HasAdjDiff R x) :
-    parDistribRevDeriv (fun w => dirac (x w))
+    parDistribRevDeriv (fun w => dirac (x w) (R:=R))
     =
     fun w =>
       let xdx := revDeriv R x w

SciLean/Core/Distribution/SimpleExamples2D.lean

@@ -142,8 +142,7 @@ def foo3 (t' : R) :=
 
 variable [Module ℝ Z] [MeasureSpace X] [Module ℝ Y]
 
-
-
+#exit
 
 -- set_option profiler true in
 -- set_option trace.Meta.Tactic.fun_trans true in

SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean

@@ -19,6 +19,7 @@ variable
   {X : Type _} [SemiInnerProductSpace K X]
   {Y : Type _} [SemiInnerProductSpace K Y]
   {Z : Type _} [SemiInnerProductSpace K Z]
+  {W : Type _} [SemiInnerProductSpace K W]
   {ι : Type _} [IndexType ι] [LawfulIndexType ι] [DecidableEq ι]
   {E : ι → Type _} [∀ i, SemiInnerProductSpace K (E i)]
 
@@ -30,6 +31,7 @@ structure HasSemiAdjoint (f : X → Y) : Prop where
    -- maybe add: ∀ x, TestFunction x → TestFunction (f x) - I think this is important for proving linearity of f'
    -- maybe add: ∀ y, TestFunction y → TestFunction (f' y)
   -- Right now we have no use for functions that have semiAdjoint and are not differentiable
+  -- so we just assume that all are differentiable
   is_differentiable : CDifferentiable K f
 
 /-- Generalization of adjoint of linear map `f : X → Y`.
@@ -47,6 +49,7 @@ def semiAdjoint (f : X → Y) (y : Y) : X :=
   | isTrue h => Classical.choose h.semiAdjoint_exists y
   | isFalse _ => 0
 
+
 -- Basic identities ------------------------------------------------------------
 --------------------------------------------------------------------------------
 
@@ -59,9 +62,26 @@ theorem semiAdjoint.arg_y.IsLinearMap_rule (f : X → Y) :
 #generate_linear_map_simps SciLean.semiAdjoint.arg_y.IsLinearMap_rule
 
 @[fun_prop]
-theorem semiAdjoint.arg_y.CDifferentiable_rule (f : X → Y) (hf : CDifferentiable K f) :
+theorem semiAdjoint.arg_y.CDifferentiable_rule (f : X → Y) :
     CDifferentiable K (fun y => semiAdjoint K f y) := sorry_proof
 
+@[fun_prop]
+theorem semiAdjoint.arg_y.IsSmoothLinearMap_rule (f : X → Y) :
+    IsSmoothLinearMap K (fun y => semiAdjoint K f y) := by constructor; fun_prop; fun_prop
+
+
+-- Do we need joint smoothness in `w` and `x` for `f` ???
+@[fun_prop]
+theorem semiAdjoint.arg_f.IsSmoothLinearMap_rule (f : W → X → Y)
+    (hf₁ : ∀ x, IsSmoothLinearMap K (f · x)) (hf₂ : ∀ w, HasSemiAdjoint K (f w ·)) :
+    IsSmoothLinearMap K (fun w => semiAdjoint K (f w)) := sorry_proof
+
+@[fun_prop]
+theorem semiAdjoint.arg_f.CDifferentiable_rule (f : W → X → Y) (y : W → Y)
+    (hf₁ : CDifferentiable K (fun (w,x) => f w x)) (hf₂ : ∀ w, HasSemiAdjoint K (f w ·))
+    (hy : CDifferentiable K y) :
+    CDifferentiable K (fun w => semiAdjoint K (f w) (y w)) := sorry_proof
+
 @[fun_prop]
 theorem HasSemiAdjoint.CDifferentiable (f : X → Y) (hf : HasSemiAdjoint K f) :
     CDifferentiable K f := hf.is_differentiable