cleaning up param deriv examples

SciLean/Core/FunctionTransformations/Preimage.lean

@@ -38,53 +38,53 @@ theorem preimage_comp' (f : β → γ) (g : α → β) :
 theorem Prod.mk.arg_fstsnd.preimage_rule_prod (f : α → β) (g : α → γ) (B : Set β) (C : Set γ) :
     preimage (fun x => (f x, g x)) (B.prod C)
     =
-    f ⁻¹' B ∩ g ⁻¹' C := sorry_proof
+    f ⁻¹' B ∩ g ⁻¹' C := by ext; simp[Set.prod]
 
 @[fun_trans]
 theorem Prod.mk.arg_fst.preimage_rule_prod (f : α → β) (c : γ) :
     preimage (fun x => (f x, c))
     =
-    fun s => f ⁻¹' (s.fst c) := sorry_proof
+    fun s => f ⁻¹' (s.fst c) := by ext; simp
 
 @[fun_trans]
 theorem Prod.mk.arg_snd.preimage_rule_prod (b : β) (g : α → γ) :
     preimage (fun x => (b, g x))
     =
-    fun s => g ⁻¹' (s.snd b) := sorry_proof
+    fun s => g ⁻¹' (s.snd b) := by ext; simp
 
 
 open SciLean
 variable {R} [RealScalar R] -- probably generalize following to LinearlyOrderedAddCommGroup
 
 @[fun_trans]
-theorem HAdd.hAdd.arg_a0.preimage_rule_Ioo (x' a b : R)  :
+theorem HAdd.hAdd.arg_a0.preimage_rule_Ioo (x' a b : R) :
     preimage (fun x : R => x + x') (Ioo a b)
     =
-    Ioo (a - x') (b - x') := by ext; simp; sorry_proof
+    Ioo (a - x') (b - x') := by ext; simp; sorry_proof -- over ℝ `simp` finishes the proof
 
 @[fun_trans]
 theorem HAdd.hAdd.arg_a1.preimage_rule_Ioo (x' a b : R)  :
     preimage (fun x : R => x' + x) (Ioo a b)
     =
-    Ioo (a - x') (b - x') := by ext; simp; sorry_proof
+    Ioo (a - x') (b - x') := by ext; simp; sorry_proof -- over ℝ `simp` finishes the proof
 
 @[fun_trans]
 theorem HSub.hSub.arg_a0.preimage_rule_Ioo (x' a b : R)  :
     preimage (fun x : R => x - x') (Ioo a b)
     =
-    Ioo (a + x') (b + x') := by ext; simp; sorry_proof
+    Ioo (a + x') (b + x') := by ext; simp; sorry_proof -- over ℝ `simp` finishes the proof
 
 @[fun_trans]
 theorem HSub.hSub.arg_a1.preimage_rule_Ioo (x' a b : R)  :
     preimage (fun x : R => x' - x) (Ioo a b)
     =
-    Ioo (x' - b) (x' - a) := by ext; simp; sorry_proof
+    Ioo (x' - b) (x' - a) := by ext; simp; sorry_proof -- over ℝ `simp` finishes the proof
 
 @[fun_trans]
 theorem Neg.neg.arg_a1.preimage_rule_Ioo (a b : R)  :
     preimage (fun x : R => - x) (Ioo a b)
     =
-    Ioo (-b) (-a) := by ext; simp; sorry_proof
+    Ioo (-b) (-a) := by ext; simp; sorry_proof -- over ℝ `simp` finishes the proof
 
 
 

SciLean/Core/Functions/Gaussian.lean

@@ -1,5 +1,6 @@
 import SciLean.Core.FunctionTransformations
 import SciLean.Core.Functions.Exp
+import SciLean.Core.Functions.Inner
 import SciLean.Tactic.Autodiff
 -- import SciLean.Core.Meta.GenerateRevDeriv
 
@@ -69,6 +70,67 @@ theorem gaussian.arg_μx.Differentiable_rule
     Differentiable R (fun w => gaussian (μ w) σ (x w)) := by intro w; fun_prop
 
 
+set_option linter.unusedVariables false in
+@[fun_trans]
+theorem gaussian.arg_μx.fderiv_rule
+    {W} [NormedAddCommGroup W] [NormedSpace R W]
+    {U} [NormedAddCommGroup U] [AdjointSpace R U]
+    (μ : W → U) (σ : R) (x : W → U)
+    (hμ : Differentiable R μ) (hx : Differentiable R x) :
+    fderiv R (fun w => gaussian (μ w) σ (x w))
+    =
+    fun w => fun dw =>L[R]
+      let μ' := μ w
+      let dμ := fderiv R μ w dw
+      let x' := x w
+      let dx := fderiv R x w dw
+      let dx' := - σ^(-2:ℤ) * ⟪dx-dμ, x'-μ'⟫
+      dx' * gaussian μ' σ x' := sorry_proof
+
+
+set_option linter.unusedVariables false in
+@[fun_trans]
+theorem gaussian.arg_μx.fwdFDeriv_rule
+    {W} [NormedAddCommGroup W] [NormedSpace R W]
+    {U} [NormedAddCommGroup U] [AdjointSpace R U]
+    (μ : W → U) (σ : R) (x : W → U)
+    (hμ : Differentiable R μ) (hx : Differentiable R x) :
+    fwdFDeriv R (fun w => gaussian (μ w) σ (x w))
+    =
+    fun w dw =>
+      let μdμ := fwdFDeriv R μ w dw
+      let xdx := fwdFDeriv R x w dw
+      let dx' := - σ^(-2:ℤ) * ⟪xdx.2-μdμ.2, xdx.1-μdμ.1⟫
+      let s := gaussian μdμ.1 σ xdx.1
+      (s, dx' * s) := by unfold fwdFDeriv; autodiff
+
+
+set_option linter.unusedVariables false in
+@[fun_trans]
+theorem gaussian.arg_μx.revFDeriv_rule
+    {W} [NormedAddCommGroup W] [AdjointSpace R W] [CompleteSpace W]
+    {U} [NormedAddCommGroup U] [AdjointSpace R U] [CompleteSpace U]
+    (μ : W → U) (σ : R) (x : W → U)
+    (hμ : Differentiable R μ) (hx : Differentiable R x) :
+    revFDeriv R (fun w => gaussian (μ w) σ (x w))
+    =
+    fun w =>
+      let μdμ := revFDeriv R μ w
+      let xdx := revFDeriv R x w
+      let s := gaussian μdμ.1 σ xdx.1
+      (s,
+       fun dr =>
+         let dx' := (dr * s * σ^(-2:ℤ)) • (xdx.1-μdμ.1)
+         let dw₁ := xdx.2 dx'
+         let dw₂ := μdμ.2 dx'
+         dw₂ - dw₁) := by
+  unfold revFDeriv
+  funext w; simp
+  autodiff; autodiff
+  funext dw; simp[← smul_assoc,mul_comm]
+  sorry_proof
+
+
 @[fun_prop]
 theorem gaussian.arg_μx.CDifferentiableAt_rule (w : W)
     (μ : W → U) (σ : R) (x : W → U)

SciLean/Core/Transformations/HasParamDerivWithJumps/Common.lean

@@ -130,7 +130,7 @@ set_default_scalar R
 --       frontierSpeed is not well defined
 @[simp,ftrans_simp]
 theorem frontierSpeed_setOf_le (φ ψ : W → X → R) :
-    frontierSpeed' R  (fun w => {x | φ w x ≤ ψ w x})
+    frontierSpeed R  (fun w => {x | φ w x ≤ ψ w x})
     =
     fun w dw x =>
       let ζ := (fun w x => φ w x - ψ w x)
@@ -139,14 +139,51 @@ theorem frontierSpeed_setOf_le (φ ψ : W → X → R) :
 
 @[simp,ftrans_simp]
 theorem frontierSpeed_setOf_lt (φ ψ : W → X → R) :
-    frontierSpeed' R  (fun w => {x | φ w x < ψ w x})
+    frontierSpeed R  (fun w => {x | φ w x < ψ w x})
     =
     fun w dw x =>
       let ζ := (fun w x => φ w x - ψ w x)
       (-(fderiv R (ζ · x) w dw)/‖fgradient (ζ w ·) x‖₂) := by
   sorry_proof
 
 
+-- not sure what to do when `(a w) > (b w)`. In that case is not really well defined `frontierSpeed`
+set_option linter.unusedVariables false in
+open Set in
+@[simp,ftrans_simp]
+theorem frontierSpeed_Icc (a b : W → R) (ha : Differentiable R a) (hb : Differentiable R b) :
+    frontierSpeed R  (fun w => Icc (a w) (b w))
+    =
+    fun w dw x =>
+      let ada := fwdFDeriv R a w dw
+      let bdb := fwdFDeriv R b w dw
+      let m := (ada.1 + bdb.1)/2
+      if x < m then
+        - ada.2
+      else
+        bdb.2 := by
+  sorry_proof
+
+
+set_option linter.unusedVariables false in
+open Set in
+@[simp,ftrans_simp]
+theorem frontierGrad_Icc
+    {W} [NormedAddCommGroup W] [AdjointSpace R W] [CompleteSpace W]
+    (a b : W → R) (ha : Differentiable R a) (hb : Differentiable R b) :
+    frontierGrad R (fun w => Icc (a w) (b w))
+    =
+    fun w x =>
+      let ada := revFDeriv R a w
+      let bdb := revFDeriv R b w
+      let m := (ada.1 + bdb.1)/2
+      if x < m then
+        - ada.2 1
+      else
+        bdb.2 1 := by
+  sorry_proof
+
+
 end
 
 ----------------------------------------------------------------------------------------------------

SciLean/Core/Transformations/HasParamDerivWithJumps/Functions.lean

@@ -23,22 +23,22 @@ variable
 open Scalar in
 @[gtrans]
 def Norm2.norm2.HasParamFDerivWithJumpsAt_rule :=
-  (HasParamFDerivWithJumpsAt.comp1_smooth_jumps_rule (R:=R) (W:=W) (X:=X) (Y:=U) (Z:=R)
+  (HasParamFDerivWithJumpsAt.comp1_differentiable_jumps_rule (R:=R) (W:=W) (X:=X) (Y:=U) (Z:=R)
     (fun _ y => ‖y‖₂²[R]) (by simp; fun_prop))
   rewrite_type_by (repeat ext); autodiff
 
 
 open Scalar in
 @[gtrans]
 def Norm2.norm2.HasParamFwdFDerivWithJumpsAt_rule :=
-  (HasParamFwdDerivWithJumps.comp1_smooth_jumps_rule (R:=R) (W:=W) (X:=X) (Y:=U) (Z:=R)
+  (HasParamFwdDerivWithJumps.comp1_differentiable_jumps_rule (R:=R) (W:=W) (X:=X) (Y:=U) (Z:=R)
     (fun _ y => ‖y‖₂²[R]) (by simp; fun_prop))
   rewrite_type_by (repeat ext); autodiff
 
 open Scalar in
 @[gtrans]
 def Norm2.norm2.HasParamRevFDerivWithJumpsAt_rule :=
-  (HasParamRevFDerivWithJumpsAt.comp1_smooth_jumps_rule (R:=R) (W:=U) (X:=X) (Y:=V) (Z:=R)
+  (HasParamRevFDerivWithJumpsAt.comp1_differentiable_jumps_rule (R:=R) (W:=U) (X:=X) (Y:=V) (Z:=R)
     (fun _ y => ‖y‖₂²[R]) (by simp; fun_prop))
   rewrite_type_by (repeat ext); autodiff