diff --git a/SciLean/Core/Integral/HasParamDerivWithJumps.lean b/SciLean/Core/Integral/HasParamDerivWithJumps.lean index c7ad88d6..66286457 100644 --- a/SciLean/Core/Integral/HasParamDerivWithJumps.lean +++ b/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] diff --git a/SciLean/Core/Integral/HasParamFwdDerivWithJumps.lean b/SciLean/Core/Integral/HasParamFwdDerivWithJumps.lean index db3bc9b6..fd6203d6 100644 --- a/SciLean/Core/Integral/HasParamFwdDerivWithJumps.lean +++ b/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 ------------------------------------------------------------------------------------ diff --git a/SciLean/Core/Integral/HasParamRevDerivWithJumps.lean b/SciLean/Core/Integral/HasParamRevDerivWithJumps.lean index a83cd966..ad5d0165 100644 --- a/SciLean/Core/Integral/HasParamRevDerivWithJumps.lean +++ b/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] ----------------------------------------------------------------------------------------------------