From bf02c94ebe9983586101cf895d794b5a786c45c8 Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Mon, 1 Apr 2024 11:46:14 -0400
Subject: [PATCH] ..

---
 .../ParametricDistribRevDeriv.lean            | 10 ++++++---
 .../Core/Distribution/SimpleExamples2D.lean   |  3 +--
 .../FunctionPropositions/HasSemiAdjoint.lean  | 22 ++++++++++++++++++-
 3 files changed, 29 insertions(+), 6 deletions(-)

diff --git a/SciLean/Core/Distribution/ParametricDistribRevDeriv.lean b/SciLean/Core/Distribution/ParametricDistribRevDeriv.lean
index 76d143af..e1ac796a 100644
--- a/SciLean/Core/Distribution/ParametricDistribRevDeriv.lean
+++ b/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,7 +43,7 @@ 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 φ
@@ -49,9 +51,11 @@ theorem comp_rule
   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
diff --git a/SciLean/Core/Distribution/SimpleExamples2D.lean b/SciLean/Core/Distribution/SimpleExamples2D.lean
index 25a7cdc8..a99ce258 100644
--- a/SciLean/Core/Distribution/SimpleExamples2D.lean
+++ b/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
diff --git a/SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean b/SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean
index 009fe3fc..beffdd8e 100644
--- a/SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean
+++ b/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