alternative way to index discontinuities in HasParamDerivWithJumps

SciLean/Core/Integral/HasParamDerivWithJumps.lean

@@ -101,6 +101,19 @@ def HasParamFDerivWithJumpsAt (f : W → X → Y) (w : W)
     /- Jump discontinuities of `f`. -/
     (jump : outParam <| I → Set X) : Prop := ∃ J Ω ι, HasParamFDerivWithJumpsAtImpl R f w f' I J ι Ω jumpVals jumpSpeed jump
 
+variable (W X Y)
+structure DiscontinuityData where
+  vals : X → Y×Y
+  speed : W → X → R
+  discontinuity : Set X
+variable {W X Y}
+
+@[gtrans]
+def HasParamFDerivWithJumpsAt' (f : W → X → Y) (w : W)
+    (f' : outParam <| W → X → Y)
+    (disc : outParam <| List (DiscontinuityData R W X Y))
+    : Prop := ∃ J Ω ι, HasParamFDerivWithJumpsAtImpl R f w f' sorry J ι Ω sorry sorry sorry
+
 
 def HasParamFDerivWithJumps (f : W → X → Y)
     (f' : W → W → X → Y)
@@ -126,6 +139,45 @@ theorem fderiv_under_integral
   interior + shocks := sorry_proof
 
 
+open FiniteDimensional
+-- @[fun_trans]
+theorem fderiv_under_integral_over_set
+  {X} [NormedAddCommGroup X] [AdjointSpace R X] [CompleteSpace X] [MeasureSpace X] [BorelSpace X]
+  (f : W → X → Y) (w dw : W) (μ : Measure X) (A : Set X)
+  {I} [hI:IndexType I] {f' df s S}
+  (hf : HasParamFDerivWithJumpsAt R f w f' I df s S)
+  /- todo: add some integrability conditions -/ :
+  (fderiv R (fun w' => ∫ x in A, f w' x ∂μ) w dw)
+  =
+  let interior := ∫ x in A, f' dw x ∂μ
+  let density := fun x => Scalar.ofENNReal (R:=R) (μ.rnDeriv volume x)
+  let shocks := ∑ i, ∫ x in S i ∩ A, (s i dw x * density x) • ((df i x).1 - (df i x).2) ∂μH[finrank R X - (1:ℕ)]
+  interior + shocks := sorry_proof
+
+
+variable (l : List ℕ)
+
+#check l.foldl (init:=0) (fun s n => s + n)
+
+open FiniteDimensional
+-- @[fun_trans]
+theorem fderiv_under_integral'
+  {X} [NormedAddCommGroup X] [AdjointSpace R X] [CompleteSpace X] [MeasureSpace X] [BorelSpace X]
+  (f : W → X → Y) (w dw : W) (μ : Measure X)
+  {f' disc}
+  (hf : HasParamFDerivWithJumpsAt' R f w f' disc)
+  /- todo: add some integrability conditions -/ :
+  (fderiv R (fun w' => ∫ x, f w' x ∂μ) w dw)
+  =
+  let interior := ∫ x, f' dw x ∂μ
+  let density := fun x => Scalar.ofENNReal (R:=R) (μ.rnDeriv volume x)
+  let shocks := disc.foldl (init:=0)
+    fun sum ⟨df,s,S⟩ => sum + ∫ x in S,
+      let vals := df x
+      (s dw x * density x) • (vals.1 - vals.2) ∂μH[finrank R X - (1:ℕ)]
+  interior + shocks := sorry_proof
+
+
 ----------------------------------------------------------------------------------------------------
 -- Lambda rules ------------------------------------------------------------------------------------
 ----------------------------------------------------------------------------------------------------
@@ -142,6 +194,17 @@ theorem smooth_rule
   sorry_proof
 
 
+@[gtrans high]
+theorem smooth_rule'
+    (w : W)
+    (f : W → X → Y) (hf : ∀ x, DifferentiableAt R (f · x) w) :
+    HasParamFDerivWithJumpsAt' R f w
+      (fun dw x => fderiv R (f · x) w dw)
+      [{ vals := 0, speed := 0, discontinuity := ∅ }] :=
+
+  sorry_proof
+
+
 theorem comp_smooth_jumps_rule
     (f : W → Y → Z) (g : W → X → Y) (w : W)
     {I g' bg sg Sg}
@@ -161,6 +224,30 @@ theorem comp_smooth_jumps_rule
       (jump := Sg) := sorry_proof
 
 
+attribute [ftrans_simp] List.cons_append  List.nil_append List.singleton_append
+attribute [ftrans_simp ↓] List.cons_append  List.nil_append List.singleton_append
+
+
+theorem comp_smooth_jumps_rule'
+    (f : W → Y → Z) (g : W → X → Y) (w : W)
+    {g' disc}
+    (hf : Differentiable R (fun (w,y) => f w y))
+    (hg : HasParamFDerivWithJumpsAt' R g w g' disc) :
+    HasParamFDerivWithJumpsAt' (R:=R) (fun w x => f w (g w x)) w
+      (f' := fun dw x =>
+         let y := g w x
+         let dy := g' dw x
+         let dz := fderiv R (fun (w,y) => f w y) (w,y) (dw,dy)
+         dz)
+      (disc := disc.map fun ⟨vals,speed,d⟩ =>
+        { vals := fun x =>
+            let y := vals x
+            (f w y.1, f w y.2)
+          speed := speed
+          discontinuity := d })
+       := sorry_proof
+
+
 theorem comp_smooth_jumps_rule_at
     (f : W → Y → Z) (g : W → X → Y) (w : W)
     {I g' bg sg Sg}
@@ -209,6 +296,28 @@ theorem comp1_smooth_jumps_rule
     comp_smooth_jumps_rule R f g w hf hg
 
 
+theorem comp1_smooth_jumps_rule'
+    (f : W → Y → Z) (hf : Differentiable R (fun (w,y) => f w y))
+    (g : W → X → Y) (w : W)
+    {g' disc}
+    (hg : HasParamFDerivWithJumpsAt' R g w g' disc) :
+    HasParamFDerivWithJumpsAt' (R:=R) (fun w x => f w (g w x)) w
+      /- f' -/
+      (fun dw x =>
+         let y := g w x
+         let dy := g' dw x
+         let dz := fderiv R (fun (w,y) => f w y) (w,y) (dw,dy)
+         dz)
+      (disc := disc.map fun ⟨vals,speed,d⟩ =>
+        { vals := fun x =>
+            let y := vals x
+            (f w y.1, f w y.2)
+          speed := speed
+          discontinuity := d }) :=
+
+    comp_smooth_jumps_rule' R f g w hf hg
+
+
 @[gtrans]
 theorem _root_.Prod.mk.arg_fstsnd.HasParamFDerivWithJumpsAt_rule
     (f : W → X → Y) (g : W → X → Z) (w : W)
@@ -232,6 +341,29 @@ theorem _root_.Prod.mk.arg_fstsnd.HasParamFDerivWithJumpsAt_rule
       (jump := Sum.elim Sf Sg) := sorry_proof
 
 
+@[gtrans]
+theorem _root_.Prod.mk.arg_fstsnd.HasParamFDerivWithJumpsAt_rule'
+    (f : W → X → Y) (g : W → X → Z) (w : W)
+    {f' fdisc} {g' gdisc}
+    (hf : HasParamFDerivWithJumpsAt' R f w f' fdisc)
+    (hg : HasParamFDerivWithJumpsAt' R g w g' gdisc)
+    /- (hIJ : DisjointJumps R Sf Sg) -/ :
+    HasParamFDerivWithJumpsAt' (R:=R) (fun w x => (f w x, g w x)) w
+      (f' := fun dw x => (f' dw x, g' dw x))
+      (disc :=
+        fdisc.map (fun d =>
+          { d with vals := fun x =>
+              let y := d.vals x
+              let z := g w x
+              ((y.1, z), (y.2, z)) })
+        ++
+        gdisc.map (fun d =>
+          { d with vals := fun x =>
+              let y := f w x
+              let z := d.vals x
+              ((y, z.1), (y, z.2)) })) := sorry_proof
+
+
 theorem comp2_smooth_jumps_rule
     (f : W → Y₁ → Y₂ → Z) (hf : Differentiable R (fun (w,y₁,y₂) => f w y₁ y₂))
     (g₁ : W → X → Y₁) (g₂ : W → X → Y₂) (w : W)
@@ -266,6 +398,38 @@ theorem comp2_smooth_jumps_rule
   . rename_i i x; induction i <;> simp
 
 
+theorem comp2_smooth_jumps_rule'
+    (f : W → Y₁ → Y₂ → Z) (hf : Differentiable R (fun (w,y₁,y₂) => f w y₁ y₂))
+    (g₁ : W → X → Y₁) (g₂ : W → X → Y₂) (w : W)
+    {g₁' dg₁} {g₂' dg₂}
+    (hg₁ : HasParamFDerivWithJumpsAt' R g₁ w g₁' dg₁)
+    (hg₂ : HasParamFDerivWithJumpsAt' R g₂ w g₂' dg₂) :
+    HasParamFDerivWithJumpsAt' (R:=R) (fun w x => f w (g₁ w x) (g₂ w x)) w
+      (f' := fun dw x =>
+         let y₁ := g₁ w x
+         let dy₁ := g₁' dw x
+         let y₂ := g₂ w x
+         let dy₂ := g₂' dw x
+         let dz := fderiv R (fun (w,y₁,y₂) => f w y₁ y₂) (w,y₁,y₂) (dw,dy₁,dy₂)
+         dz)
+      (disc :=
+        (dg₁.map fun d => { d with
+          vals := fun x =>
+           let y₁ := d.vals x
+           let y₂ := g₂ w x
+           (f w y₁.1 y₂, f w y₁.2 y₂) })
+        ++
+        (dg₂.map fun d => { d with
+          vals := fun x =>
+           let y₁ := g₁ w x
+           let y₂ := d.vals x
+           (f w y₁ y₂.1, f w y₁ y₂.2) })) := by
+
+  convert comp_smooth_jumps_rule' R (fun (w:W) (y:Y₁×Y₂) => f w y.1 y.2) (fun w x => (g₁ w x, g₂ w x)) w
+    (hf) (Prod.mk.arg_fstsnd.HasParamFDerivWithJumpsAt_rule' R g₁ g₂ w hg₁ hg₂)
+
+  . simp[Function.comp]
+
 
 end HasParamFDerivWithJumpsAt
 open HasParamFDerivWithJumpsAt
@@ -416,3 +580,85 @@ def Scalar.cos.arg_a0.HasParamFDerivWithJumpsAt_rule :=
 def gaussian.arg_a0.HasParamFDerivWithJumpsAt_rule (σ : R) :=
   (comp2_smooth_jumps_rule (R:=R) (W:=W) (X:=X) (Y₁:=X) (Y₂:=X) (Z:=R) (fun _ μ x => gaussian μ σ x) (by simp; fun_prop))
   -- rewrite_type_by (repeat ext); autodiff
+
+
+
+----------------------------------------------------------------------------------------------------
+
+
+@[gtrans]
+def Prod.fst.arg_self.HasParamFDerivWithJumpsAt_rule' :=
+  (comp1_smooth_jumps_rule' (R:=R) (W:=W) (X:=X) (Y:=Y×Z) (Z:=Y) (fun _ yz => yz.1) (by fun_prop))
+  -- rewrite_type_by (repeat ext); autodiff
+
+
+@[gtrans]
+def Prod.snd.arg_self.HasParamFDerivWithJumpsAt_rule' :=
+  (comp1_smooth_jumps_rule' (R:=R) (W:=W) (X:=X) (Y:=Y×Z) (Z:=Z) (fun _ yz => yz.2) (by fun_prop))
+  -- rewrite_type_by (repeat ext); autodiff
+
+
+@[gtrans]
+def HAdd.hAdd.arg_a0a1.HasParamFDerivWithJumpsAt_rule' :=
+  (comp2_smooth_jumps_rule' (R:=R) (W:=W) (X:=X) (Y₁:=Y) (Y₂:=Y) (Z:=Y) (fun _ y₁ y₂ => y₁ + y₂) (by fun_prop))
+  -- rewrite_type_by (repeat ext); autodiff
+
+
+@[gtrans]
+def HSub.hSub.arg_a0a1.HasParamFDerivWithJumpsAt_rule' :=
+  (comp2_smooth_jumps_rule' (R:=R) (W:=W) (X:=X) (Y₁:=Y) (Y₂:=Y) (Z:=Y) (fun _ y₁ y₂ => y₁ - y₂) (by fun_prop))
+  -- rewrite_type_by (repeat ext); autodiff
+
+
+@[gtrans]
+def Neg.neg.arg_a0.HasParamFDerivWithJumpsAt_rule' :=
+  (comp1_smooth_jumps_rule' (R:=R) (X:=X) (Y:=Y) (Z:=Y) (fun (w : W) y => - y) (by fun_prop))
+  -- rewrite_type_by (repeat ext); autodiff
+
+
+@[gtrans]
+def HMul.hMul.arg_a0a1.HasParamFDerivWithJumpsAt_rule' :=
+  (comp2_smooth_jumps_rule' (R:=R) (W:=W) (X:=X) (Y₁:=R) (Y₂:=R) (Z:=R) (fun _ y₁ y₂ => y₁ * y₂) (by fun_prop))
+  -- rewrite_type_by (repeat ext); autodiff
+
+
+@[gtrans]
+def HPow.hPow.arg_a0.HasParamFDerivWithJumpsAt_rule' (n:ℕ) :=
+  (comp1_smooth_jumps_rule' (R:=R) (X:=X) (Y:=R) (Z:=R) (fun (w : W) y => y^n) (by fun_prop))
+  -- rewrite_type_by (repeat ext); autodiff
+
+
+@[gtrans]
+def HSMul.hSMul.arg_a0a1.HasParamFDerivWithJumpsAt_rule' :=
+  (comp2_smooth_jumps_rule' (R:=R) (W:=W) (X:=X) (Y₁:=R) (Y₂:=Y) (Z:=Y) (fun _ y₁ y₂ => y₁ • y₂) (by fun_prop))
+  -- rewrite_type_by (repeat ext); autodiff
+
+
+@[gtrans]
+theorem ite.arg_te.HasParamFDerivWithJumpsAt_rule'
+    (f g : W → X → Y) (w : W)
+    {c : W → X → Prop} [∀ w x, Decidable (c w x)]
+    {f' df} {g' dg}
+    (hf : HasParamFDerivWithJumpsAt' R f w f' df)
+    (hg : HasParamFDerivWithJumpsAt' R g w g' dg) :
+    HasParamFDerivWithJumpsAt' (R:=R) (fun w x => if c w x then f w x else g w x) w
+      (f' := fun dw x => if c w x then f' dw x else g' dw x)
+      (disc :=
+        {vals := fun x => (f w x, g w x)
+         speed := frontierSpeed' R (fun w => {x | ¬c w x}) w
+         discontinuity := frontier {x | c w x}}
+        ::
+        df.map (fun d => {d with discontinuity := d.discontinuity ∩ {x | c w x}})
+        ++
+        dg.map (fun d => {d with discontinuity := d.discontinuity ∩ {x | ¬c w x}})) := by
+
+  sorry_proof
+
+
+attribute [ftrans_simp] List.append_assoc List.map_cons List.map_nil
+attribute [ftrans_simp ↓] List.append_assoc List.map_cons List.map_nil
+
+set_option trace.Meta.Tactic.simp.rewrite true in
+#check (([1] ++ [2,3] ++ [5,6]) ++ ([1] ++ [2,3] ++ [5,6])  ) rewrite_by
+  simp (config:={singlePass:=true}) only [ftrans_simp]
+  simp (config:={singlePass:=true}) only [ftrans_simp]

SciLean/Core/Integral/HasParamFwdDerivWithJumps.lean

@@ -75,6 +75,28 @@ theorem fwdFDeriv_under_integral
   . simp only [fderiv_under_integral R f w dw μ hf.1, add_left_inj, snd_integral (hf:=sorry_proof)]
 
 
+open FiniteDimensional
+@[fun_trans]
+theorem fwdFDeriv_under_integral_over_set
+  {X} [NormedAddCommGroup X] [AdjointSpace R X] [CompleteSpace X] [MeasureSpace X] [BorelSpace X]
+  (f : W → X → Y) (w : W) (μ : Measure X) (A : Set X)
+  {I} [hI : IndexType I] {f' df s S}
+  (hf : HasParamFwdFDerivWithJumpsAt R f w f' I df s S)
+  /- (hμ : μ ≪ volume) -/ :
+  (fwdFDeriv R (fun w' => ∫ x in A, f w' x ∂μ) w)
+  =
+  fun dw =>
+    let interior := ∫ x in A, f' dw x ∂μ
+    let density := fun x => Scalar.ofENNReal (R:=R) (μ.rnDeriv volume x)
+    let shocks := ∑ i, ∫ x in S i ∩ A, (s i dw x * density x) • ((df i x).1 - (df i x).2) ∂μH[finrank R X - (1:ℕ)]
+    (interior.1, interior.2 + shocks) := by
+
+  unfold fwdFDeriv
+  funext dw; ext
+  . simp only [fst_integral (hf := sorry_proof), hf.2]
+  . simp only [fderiv_under_integral_over_set R f w dw μ A hf.1, add_left_inj, snd_integral (hf:=sorry_proof)]
+
+
 
 ----------------------------------------------------------------------------------------------------
 -- Lambda rules ------------------------------------------------------------------------------------

SciLean/Core/Integral/HasParamRevDerivWithJumps.lean

@@ -111,7 +111,24 @@ theorem revFDeriv_under_integral
   have hf' : ∀ x, IsContinuousLinearMap R (f' x).2 := sorry_proof -- this should be part of hf
   fun_trans (disch:=apply hf') [adjoint_sum,adjoint_integral,adjoint_adjoint,smul_smul]
 
+@[fun_trans]
+theorem revFDeriv_under_integral_over_set
+    (f : W → X → Y) (w : W) (μ : Measure X) (A : Set X)
+    {I} [hI : IndexType I] {f' df s S}
+    (hf : HasParamRevFDerivWithJumpsAt R f w f' I df s S) :
+    (revFDeriv R (fun w' => ∫ x in A, f w' x ∂μ) w)
+    =
+    let val := ∫ x in A, f w x ∂μ
+    (val, fun dy =>
+      let interior := ∫ x in A, (f' x).2 dy ∂μ
+      let density := fun x => Scalar.ofENNReal (R:=R) (μ.rnDeriv volume x)
+      let shocks := ∑ i, ∫ x in S i ∩ A, (⟪(df i x).1 - (df i x).2, dy⟫ * density x) • s i x ∂μH[finrank R X - (1:ℕ)]
+      interior + shocks) := by
 
+  unfold revFDeriv
+  simp only [fderiv_under_integral_over_set R f w _ μ A hf.1]
+  have hf' : ∀ x, IsContinuousLinearMap R (f' x).2 := sorry_proof -- this should be part of hf
+  fun_trans (disch:=apply hf') [adjoint_sum,adjoint_integral,adjoint_adjoint,smul_smul]
 
 
 ----------------------------------------------------------------------------------------------------