From b87d1bf9075d2f95a7136e1d663411e6e52da3a1 Mon Sep 17 00:00:00 2001 From: lecopivo Date: Mon, 1 Apr 2024 15:57:33 +0200 Subject: [PATCH] refactoring of distributions - probably too aggresive and should be reverted --- SciLean/Core/Distribution/Basic.lean | 397 ++++++++---------- SciLean/Core/Distribution/Eval.lean | 45 +- .../Distribution/ParametricDistribDeriv.lean | 99 +++-- .../ParametricDistribFwdDeriv.lean | 74 ++-- .../ParametricDistribRevDeriv.lean | 47 +-- SciLean/Core/Distribution/SimpleExamples.lean | 5 + .../Core/Distribution/SimpleExamples2D.lean | 21 +- SciLean/Core/Distribution/SurfaceDirac.lean | 30 +- .../Core/FunctionSpaces/SmoothLinearMap.lean | 40 ++ 9 files changed, 378 insertions(+), 380 deletions(-) diff --git a/SciLean/Core/Distribution/Basic.lean b/SciLean/Core/Distribution/Basic.lean index 8649d0df..37d9d219 100644 --- a/SciLean/Core/Distribution/Basic.lean +++ b/SciLean/Core/Distribution/Basic.lean @@ -16,7 +16,7 @@ namespace SciLean variable {R} [RealScalar R] {W} [Vec R W] [Module ℝ W] - {X} [TopologicalSpace X] [space : TCOr (Vec R X) (DiscreteTopology X)] + {X} [Vec R X] -- [TopologicalSpace X] [space : TCOr (Vec R X) (DiscreteTopology X)] {Y} [Vec R Y] [Module ℝ Y] {Z} [Vec R Z] {U} [Vec R U] @@ -25,15 +25,9 @@ variable set_default_scalar R variable (R X Y) -structure Distribution where - action : (π’Ÿ X) ⊸ Y +abbrev Distribution := (π’Ÿ X) ⊸ Y variable {R X Y} -namespace Distribution -scoped notation "βŸͺ" f' ", " Ο† "⟫" => Distribution.action f' Ο† -end Distribution - -open Distribution notation "π’Ÿ'" X => Distribution defaultScalar% X defaultScalar% notation "π’Ÿ'" "(" X ", " Y ")" => Distribution defaultScalar% X Y @@ -42,33 +36,29 @@ notation "π’Ÿ'" "(" X ", " Y ")" => Distribution defaultScalar% X Y | `($(_) $_ $X $Y) => `(π’Ÿ'($X,$Y)) | _ => throw () -@[simp, ftrans_simp] -theorem action_mk_apply (f : (π’Ÿ X) ⊸ Y) (Ο† : π’Ÿ X) : - βŸͺDistribution.mk (R:=R) f, Ο†βŸ« = f Ο† := by rfl @[ext] -theorem Distribution.ext (x y : Distribution R X Y) : - (βˆ€ (Ο† : π’Ÿ X), βŸͺx,Ο†βŸ« = βŸͺy,Ο†βŸ«) +theorem Distribution.ext (x y : π’Ÿ'(X,Y)) : + (βˆ€ (Ο† : π’Ÿ X), x Ο† = y Ο†) β†’ x = y := by - induction x; induction y; simp only [action_mk_apply, mk.injEq]; aesop + apply SmoothLinearMap.ext ---------------------------------------------------------------------------------------------------- -- Algebra ----------------------------------------------------------------------------------------- ---------------------------------------------------------------------------------------------------- -instance : Zero (π’Ÿ'(X,Y)) := ⟨⟨fun _Ο† ⊸ 0⟩⟩ -instance : Add (π’Ÿ'(X,Y)) := ⟨fun f g => ⟨fun Ο† ⊸ βŸͺf, Ο†βŸ« + βŸͺg, Ο†βŸ«βŸ©βŸ© -instance : Sub (π’Ÿ'(X,Y)) := ⟨fun f g => ⟨fun Ο† ⊸ βŸͺf, Ο†βŸ« - βŸͺg, Ο†βŸ«βŸ©βŸ© -instance : Neg (π’Ÿ'(X,Y)) := ⟨fun f => ⟨fun Ο† ⊸ -βŸͺf, Ο†βŸ«βŸ©βŸ© -instance : SMul R (π’Ÿ'(X,Y)) := ⟨fun r f => ⟨fun Ο† ⊸ r β€’ βŸͺf, Ο†βŸ«βŸ©βŸ© -instance [Module ℝ Y] : SMul ℝ (π’Ÿ'(X,Y)) := ⟨fun r f => ⟨⟨fun Ο† => r β€’ βŸͺf, Ο†βŸ«, sorry_proof⟩⟩⟩ +-- instance : Zero (π’Ÿ'(X,Y)) := by unfold Distribution; infer_instance +-- instance : Add (π’Ÿ'(X,Y)) := by unfold Distribution; infer_instance +-- instance : Sub (π’Ÿ'(X,Y)) := by unfold Distribution; infer_instance +-- instance : Neg (π’Ÿ'(X,Y)) := by unfold Distribution; infer_instance +-- instance : SMul R (π’Ÿ'(X,Y)) := by unfold Distribution; infer_instance +instance [Module ℝ Y] : SMul ℝ (π’Ÿ'(X,Y)) := ⟨fun r f => ⟨fun Ο† => r β€’ (f Ο†), sorry_proof⟩⟩ --- not sure what exact the topology is supposed to be here -instance : UniformSpace (π’Ÿ'(X,Y)) := sorry -instance : Vec R (π’Ÿ'(X,Y)) := Vec.mkSorryProofs +-- instance : UniformSpace (π’Ÿ'(X,Y)) := by unfold Distribution; infer_instance +-- instance : Vec R (π’Ÿ'(X,Y)) := by unfold Distribution; infer_instance instance [Module ℝ Y] : Module ℝ (π’Ÿ'(X,Y)) := Module.mkSorryProofs @@ -76,57 +66,77 @@ instance [Module ℝ Y] : Module ℝ (π’Ÿ'(X,Y)) := Module.mkSorryProofs -- Extended action --------------------------------------------------------------------------------- ---------------------------------------------------------------------------------------------------- -open Notation in +open BigOperators in @[pp_dot] noncomputable -def Distribution.extAction (T : π’Ÿ'(X,Y)) (Ο† : X β†’ R) : Y := limit n β†’ ∞, βŸͺT, testFunApprox n Ο†βŸ« +def Distribution.extAction (T : π’Ÿ'(X,Y)) (Ο† : X β†’ Z) (L : Y ⊸ Z ⊸ W) : W := + if h : βˆƒ (zβ‚™ : β„• β†’ Z) (Ο†β‚™ : β„• β†’ π’Ÿ X), βˆ€ x, βˆ‘' i, Ο†β‚™ i x β€’ zβ‚™ i = Ο† x then + let zβ‚™ := Classical.choose h + let Ο†β‚™ := (Classical.choose_spec h).choose + βˆ‘' i, L (T (Ο†β‚™ i)) (zβ‚™ i) + else + 0 + +namespace Distribution +scoped notation "βŸͺ" T ", " Ο† "⟫[" L "]" => Distribution.extAction T Ο† L +end Distribution + + +noncomputable +abbrev Distribution.extAction' (T : π’Ÿ'(X,Y)) (Ο† : X β†’ R) : Y := T.extAction Ο† (fun y ⊸ fun r ⊸ r β€’ y) -@[pp_dot] noncomputable -def Distribution.extAction' (T : π’Ÿ'(X,Y)) (Ο† : X β†’ Z) (L : Y β†’ Z β†’ W) : W := sorry - -- write Ο† as βˆ‘ i, Ο†α΅’ β€’ zα΅’ - -- and βŸͺT, Ο†βŸ«[L] = βˆ‘ i, L βŸͺT, Ο†α΅’βŸ« zα΅’ +abbrev Distribution.integrate (T : π’Ÿ'(X,Y)) : Y := T.extAction' (fun _ => 1) + +@[fun_prop] +theorem TestFunction.apply_IsSmoothLinearMap : IsSmoothLinearMap R fun (Ο† : π’Ÿ X) => (Ο† : X β†’ R) := sorry_proof --- Lean usually fails to unify this theorem, thus we have a custom simproc to apply it theorem Distribution.mk_extAction (T : (X β†’ R) β†’ Y) (hT : IsSmoothLinearMap R (fun Ο† : π’Ÿ X => T Ο†)) (Ο† : X β†’ R) : - (Distribution.mk (⟨fun Ο† => T Ο†,hT⟩)).extAction Ο† = T Ο† := sorry_proof + Distribution.extAction (SmoothLinearMap.mk' R (fun (Ο† : π’Ÿ X) => T Ο†) hT : Distribution _ _ _) Ο† (fun y ⊸ fun r ⊸ r β€’ y) = T Ο† := sorry_proof + +-- This is definitely not true as stated, what kind of condistions do we need on `Ο†` and `T`? +@[fun_prop] +theorem Distribution.extAction.arg_Ο†.IsSmoothLinearMap (T : π’Ÿ'(X,U)) (Ο† : W β†’ X β†’ V) (L : U ⊸ V ⊸ Z) + (hΟ† : IsSmoothLinearMap R Ο†) : + IsSmoothLinearMap R (fun w => T.extAction (Ο† w) L) := sorry_proof --- #check Function. --- theorem Distribution.mk_restrict (T : (X β†’ R) β†’ R) (hT : IsSmoothLinearMap R (fun Ο† : π’Ÿ X => T Ο†)) (Ο† : X β†’ R) (A : Set X) : --- ((Distribution.mk (⟨fun Ο† => T Ο†,hT⟩)).restrict A).extAction Ο† = T Ο† := sorry_proof +@[fun_prop] +theorem Distribution.extAction.arg_T.IsSmoothLinearMap (T : W β†’ π’Ÿ'(X,U)) (Ο† : X β†’ V) (L : U ⊸ V ⊸ Z) + (hT : IsSmoothLinearMap R T) : + IsSmoothLinearMap R (fun w => (T w).extAction Ο† L) := sorry_proof -open Lean Meta in -/-- Simproc to apply `Distribution.mk_extAction` theorem -/ -simproc_decl Distribution.mk_extAction_simproc (Distribution.extAction (Distribution.mk (SmoothLinearMap.mk _ _)) _) := fun e => do +-- open Lean Meta in +-- /-- Simproc to apply `Distribution.mk_extAction` theorem -/ +-- simproc_decl Distribution.mk_extAction_simproc (Distribution.extAction (Distribution.mk (SmoothLinearMap.mk _ _)) _) := fun e => do - let Ο† := e.appArg! - let T := e.appFn!.appArg! +-- let Ο† := e.appArg! +-- let T := e.appFn!.appArg! - let .lam xName xType xBody xBi := T.appArg!.appFn!.appArg! - | return .continue - let hT := T.appArg!.appArg! +-- let .lam xName xType xBody xBi := T.appArg!.appFn!.appArg! +-- | return .continue +-- let hT := T.appArg!.appArg! - withLocalDecl xName xBi xType fun x => do - let R := xType.getArg! 0 - let X := xType.getArg! 2 - withLocalDecl `Ο†' xBi (← mkArrow X R) fun Ο†' => do - let b := xBody.instantiate1 x - let b := b.replace (fun e' => - if e'.isAppOf ``DFunLike.coe && - 5 ≀ e'.getAppNumArgs && - e'.getArg! 4 == x then - .some (mkAppN Ο†' e'.getAppArgs[5:]) - else - .none) +-- withLocalDecl xName xBi xType fun x => do +-- let R := xType.getArg! 0 +-- let X := xType.getArg! 2 +-- withLocalDecl `Ο†' xBi (← mkArrow X R) fun Ο†' => do +-- let b := xBody.instantiate1 x +-- let b := b.replace (fun e' => +-- if e'.isAppOf ``DFunLike.coe && +-- 5 ≀ e'.getAppNumArgs && +-- e'.getArg! 4 == x then +-- .some (mkAppN Ο†' e'.getAppArgs[5:]) +-- else +-- .none) - if b.containsFVar x.fvarId! then - return .continue +-- if b.containsFVar x.fvarId! then +-- return .continue - let T ← mkLambdaFVars #[Ο†'] b - let prf ← mkAppM ``Distribution.mk_extAction #[T, hT, Ο†] - return .visit {expr := T.beta #[Ο†], proof? := prf} +-- let T ← mkLambdaFVars #[Ο†'] b +-- let prf ← mkAppM ``Distribution.mk_extAction #[T, hT, Ο†] +-- return .visit {expr := T.beta #[Ο†], proof? := prf} @@ -151,17 +161,13 @@ simproc_decl Distribution.mk_extAction_simproc (Distribution.extAction (Distribu -- seqRight_eq := by intros; rfl -- pure_seq := by intros; rfl -def dirac (x : X) : π’Ÿ' X := ⟨fun Ο† ⊸ Ο† x⟩ +def dirac (x : X) : π’Ÿ' X := fun Ο† ⊸ Ο† x -open Notation -noncomputable -def Distribution.bind (x' : π’Ÿ'(X,Z)) (f : X β†’ π’Ÿ' Y) : π’Ÿ'(Y,Z) := - ⟨⟨fun Ο† => x'.extAction fun x => βŸͺf x, Ο†βŸ«, sorry_proof⟩⟩ open Notation noncomputable -def Distribution.bind' (x' : π’Ÿ'(X,U)) (f : X β†’ π’Ÿ'(Y,V)) (L : U β†’ V β†’ W) : π’Ÿ'(Y,W) := - ⟨⟨fun Ο† => x'.extAction' (fun x => βŸͺf x, Ο†βŸ«) L, sorry_proof⟩⟩ +def Distribution.bind (x' : π’Ÿ'(X,U)) (f : X β†’ π’Ÿ'(Y,V)) (L : U ⊸ V ⊸ W) : π’Ÿ'(Y,W) := + fun Ο† ⊸ x'.extAction (fun x => f x Ο†) L ---------------------------------------------------------------------------------------------------- @@ -169,106 +175,57 @@ def Distribution.bind' (x' : π’Ÿ'(X,U)) (f : X β†’ π’Ÿ'(Y,V)) (L : U β†’ V β†’ ---------------------------------------------------------------------------------------------------- @[simp, ftrans_simp] -theorem action_dirac (x : X) (Ο† : π’Ÿ X) : βŸͺdirac x, Ο†βŸ« = Ο† x := by simp[dirac] +theorem action_dirac (x : X) (Ο† : π’Ÿ X) : dirac x Ο† = Ο† x := by simp[dirac] @[simp, ftrans_simp] -theorem action_bind (x : π’Ÿ'(X,Z)) (f : X β†’ π’Ÿ' Y) (Ο† : π’Ÿ Y) : - βŸͺx.bind f, Ο†βŸ« = x.extAction (fun x' => βŸͺf x', Ο†βŸ«) := by +theorem action_bind (x : π’Ÿ'(X,U)) (f : X β†’ π’Ÿ'(Y,V)) (L : U ⊸ V ⊸ W) (Ο† : π’Ÿ Y) : + x.bind f L Ο† = x.extAction (fun x' => f x' Ο†) L := by simp[Distribution.bind] -@[simp, ftrans_simp] -theorem extAction_bind (x : π’Ÿ'(X,Z)) (f : X β†’ π’Ÿ' Y) (Ο† : Y β†’ R) : - (x.bind f).extAction Ο† = x.extAction (fun x' => (f x').extAction Ο†) := by - simp[Distribution.bind] - sorry_proof + +-- @[simp, ftrans_simp] +-- theorem extAction_bind (x : π’Ÿ'(X,U)) (f : X β†’ π’Ÿ'(Y,V)) (L : U ⊸ V ⊸ W) (Ο† : Y β†’ Z) (K : W ⊸ Z ⊸ W') : +-- (x.bind f L).extAction Ο† K = x.extAction (fun x' => (f x').extAction Ο† (sorry : V ⊸ Z ⊸ VβŠ—Z)) (sorry : U ⊸ (VβŠ—Z) ⊸ W') := by +-- simp [Distribution.bind] ---------------------------------------------------------------------------------------------------- -- Arithmetics ------------------------------------------------------------------------------------- ---------------------------------------------------------------------------------------------------- -@[simp, ftrans_simp, action_push] -theorem Distribution.zero_action (Ο† : π’Ÿ X) : βŸͺ(0 : π’Ÿ'(X,Y)), Ο†βŸ« = 0 := by rfl - -@[action_push] -theorem Distribution.add_action (T T' : π’Ÿ'(X,Y)) (Ο† : π’Ÿ X) : βŸͺT + T', Ο†βŸ« = βŸͺT,Ο†βŸ« + βŸͺT',Ο†βŸ« := by rfl - -@[action_push] -theorem Distribution.sub_action (T T' : π’Ÿ'(X,Y)) (Ο† : π’Ÿ X) : βŸͺT - T', Ο†βŸ« = βŸͺT,Ο†βŸ« - βŸͺT',Ο†βŸ« := by rfl - -@[action_push] -theorem Distribution.smul_action (r : R) (T : π’Ÿ'(X,Y)) (Ο† : π’Ÿ X) : βŸͺr β€’ T, Ο†βŸ« = r β€’ βŸͺT,Ο†βŸ« := by rfl - -@[action_push] -theorem Distribution.neg_action (T : π’Ÿ'(X,Y)) (Ο† : π’Ÿ X) : βŸͺ- T, Ο†βŸ« = - βŸͺT,Ο†βŸ« := by rfl - -open BigOperators in -@[action_push] -theorem Distribution.fintype_sum_action {I} [Fintype I] (T : I β†’ π’Ÿ'(X,Y)) (Ο† : π’Ÿ X) : - βŸͺβˆ‘ i, T i, Ο†βŸ« = βˆ‘ i, βŸͺT i, Ο†βŸ« := by sorry_proof - -@[action_push] -theorem Distribution.indextype_sum_action {I} [IndexType I] (T : I β†’ π’Ÿ'(X,Y)) (Ο† : π’Ÿ X) : - βŸͺβˆ‘ i, T i, Ο†βŸ« = βˆ‘ i, βŸͺT i, Ο†βŸ« := by sorry_proof +section Arithmetics @[simp, ftrans_simp, action_push] -theorem Distribution.zero_extAction (Ο† : X β†’ R) : (0 : π’Ÿ'(X,Y)).extAction Ο† = 0 := by sorry_proof - --- todo: this needs some integrability condition -@[action_push] -theorem Distribution.add_extAction (T T' : π’Ÿ'(X,Y)) (Ο† : X β†’ R) : - (T + T').extAction Ο† = T.extAction Ο† + T'.extAction Ο† := by sorry_proof - -@[action_push] -theorem Distribution.sub_extAction (T T' : π’Ÿ'(X,Y)) (Ο† : X β†’ R) : - (T - T').extAction Ο† = T.extAction Ο† - T'.extAction Ο† := by sorry_proof - -@[action_push] -theorem Distribution.smul_extAction (r : R) (T : π’Ÿ'(X,Y)) (Ο† : X β†’ R) : - (r β€’ T).extAction Ο† = r β€’ T.extAction Ο† := by sorry_proof +theorem Distribution.zero_extAction (Ο† : X β†’ V) (L : U ⊸ V ⊸ W) : (0 : π’Ÿ'(X,U)).extAction Ο† L = 0 := by sorry_proof -@[action_push] -theorem Distribution.neg_extAction (T : π’Ÿ'(X,Y)) (Ο† : X β†’ R) : - (- T).extAction Ο† = - T.extAction Ο† := by sorry_proof - -open BigOperators in -@[action_push] -theorem Distribution.fintype_sum_extAction {I} [Fintype I] (T : I β†’ π’Ÿ'(X,Y)) (Ο† : X β†’ R) : - (βˆ‘ i, T i).extAction Ο† = βˆ‘ i, (T i).extAction Ο† := by sorry_proof - -@[action_push] -theorem Distribution.indextype_sum_extAction {I} [IndexType I] (T : I β†’ π’Ÿ'(X,Y)) (Ο† : X β†’ R) : - (βˆ‘ i, T i).extAction Ο† = βˆ‘ i, (T i).extAction Ο† := by sorry_proof - - -@[simp, ftrans_simp, action_push] -theorem Distribution.zero_extAction' (Ο† : X β†’ Z) (L : Y β†’ Z β†’ W) : (0 : π’Ÿ'(X,Y)).extAction' Ο† L = 0 := by sorry_proof -- todo: this needs some integrability condition @[action_push] -theorem Distribution.add_extAction' (T T' : π’Ÿ'(X,Y)) (Ο† : X β†’ Z) (L : Y β†’ Z β†’ W) : - (T + T').extAction' Ο† L = T.extAction' Ο† L + T'.extAction' Ο† L := by sorry_proof +theorem Distribution.add_extAction (T T' : π’Ÿ'(X,U)) (Ο† : X β†’ V) (L : U ⊸ V ⊸ W) : + ((T + T') : π’Ÿ'(X,U)).extAction Ο† L = T.extAction Ο† L + T'.extAction Ο† L := by sorry_proof @[action_push] -theorem Distribution.sub_extAction' (T T' : π’Ÿ'(X,Y)) (Ο† : X β†’ Z) (L : Y β†’ Z β†’ W) : - (T - T').extAction' Ο† L = T.extAction' Ο† L - T'.extAction' Ο† L := by sorry_proof +theorem Distribution.sub_extAction (T T' : π’Ÿ'(X,U)) (Ο† : X β†’ V) (L : U ⊸ V ⊸ W) : + (T - T').extAction Ο† L = T.extAction Ο† L - T'.extAction Ο† L := by sorry_proof @[action_push] -theorem Distribution.smul_extAction' (r : R) (T : π’Ÿ'(X,Y)) (Ο† : X β†’ Z) (L : Y β†’ Z β†’ W) : - (r β€’ T).extAction' Ο† L = r β€’ T.extAction' Ο† L := by sorry_proof +theorem Distribution.smul_extAction (r : R) (T : π’Ÿ'(X,U)) (Ο† : X β†’ V) (L : U ⊸ V ⊸ W) : + (r β€’ T).extAction Ο† L = r β€’ T.extAction Ο† L := by sorry_proof @[action_push] -theorem Distribution.neg_extAction' (T : π’Ÿ'(X,Y)) (Ο† : X β†’ Z) (L : Y β†’ Z β†’ W) : - (- T).extAction' Ο† L = - T.extAction' Ο† L := by sorry_proof +theorem Distribution.neg_extAction (T : π’Ÿ'(X,U)) (Ο† : X β†’ V) (L : U ⊸ V ⊸ W) : + (- T).extAction Ο† L = - T.extAction Ο† L := by sorry_proof open BigOperators in @[action_push] -theorem Distribution.fintype_sum_extAction' {I} [Fintype I] (T : I β†’ π’Ÿ'(X,Y)) (Ο† : X β†’ Z) (L : Y β†’ Z β†’ W) : - (βˆ‘ i, T i).extAction' Ο† L = βˆ‘ i, (T i).extAction' Ο† L := by sorry_proof +theorem Distribution.fintype_sum_extAction {I} [Fintype I] (T : I β†’ π’Ÿ'(X,U)) (Ο† : X β†’ V) (L : U ⊸ V ⊸ W) : + (βˆ‘ i, T i).extAction Ο† L = βˆ‘ i, (T i).extAction Ο† L := by sorry_proof @[action_push] -theorem Distribution.indextype_sum_extAction' {I} [IndexType I] (T : I β†’ π’Ÿ'(X,Y)) (Ο† : X β†’ Z) (L : Y β†’ Z β†’ W) : - (βˆ‘ i, T i).extAction' Ο† L = βˆ‘ i, (T i).extAction' Ο† L := by sorry_proof +theorem Distribution.indextype_sum_extAction {I} [IndexType I] (T : I β†’ π’Ÿ'(X,U)) (Ο† : X β†’ V) (L : U ⊸ V ⊸ W) : + (βˆ‘ i, T i).extAction Ο† L = βˆ‘ i, (T i).extAction Ο† L := by sorry_proof + +end Arithmetics ---------------------------------------------------------------------------------------------------- @@ -280,9 +237,9 @@ variable [MeasureSpace X] open Classical Notation in noncomputable def iteD (A : Set X) (t e : π’Ÿ'(X,Y)) : π’Ÿ'(X,Y) := - ⟨⟨fun Ο† => - t.extAction (fun x => if x ∈ A then Ο† x else 0) + - e.extAction (fun x => if x ∈ A then 0 else Ο† x), sorry_proof⟩⟩ + fun Ο† ⊸ + t.extAction (fun x => if x ∈ A then Ο† x else 0) (fun y ⊸ fun r ⊸ r β€’ y) + + e.extAction (fun x => if x ∈ A then 0 else Ο† x) (fun y ⊸ fun r ⊸ r β€’ y) open Lean.Parser Term in syntax withPosition("ifD " term " then " @@ -301,15 +258,20 @@ def unexpandIteD : Lean.PrettyPrinter.Unexpander @[action_push] theorem Distribution.action_iteD (A : Set X) (t e : π’Ÿ'(X,Y)) (Ο† : π’Ÿ X) : - βŸͺiteD A t e, Ο†βŸ« = - t.extAction (fun x => if x ∈ A then Ο† x else 0) + - e.extAction (fun x => if x βˆ‰ A then Ο† x else 0) := by sorry_proof + iteD A t e Ο† = + t.extAction (fun x => if x ∈ A then Ο† x else 0) (fun y ⊸ fun r ⊸ r β€’ y) + + e.extAction (fun x => if x βˆ‰ A then Ο† x else 0) (fun y ⊸ fun r ⊸ r β€’ y) := by sorry_proof @[action_push] -theorem Distribution.extAction_iteD (A : Set X) (t e : π’Ÿ'(X,Y)) (Ο† : X β†’ R) : - (iteD A t e).extAction Ο† = - t.extAction (fun x => if x ∈ A then Ο† x else 0) + - e.extAction (fun x => if x βˆ‰ A then Ο† x else 0) := by sorry_proof +theorem Distribution.extAction_iteD (A : Set X) (t e : π’Ÿ'(X,U)) (Ο† : X β†’ V) (L : U ⊸ V ⊸ W) : + (iteD A t e).extAction Ο† L = + t.extAction (fun x => if x ∈ A then Ο† x else 0) L + + e.extAction (fun x => if x βˆ‰ A then Ο† x else 0) L := by sorry_proof + +@[fun_prop] +theorem iteD.arg_te.IsSmoothLinearMap_rule (A : Set X) (t e : W β†’ π’Ÿ'(X,Y)) + (ht : IsSmoothLinearMap R t) (he : IsSmoothLinearMap R e) : + IsSmoothLinearMap R (fun w => iteD A (t w) (e w)) := sorry_proof ---------------------------------------------------------------------------------------------------- @@ -367,23 +329,28 @@ theorem iteD_restrict' (T : π’Ÿ'(X,Y)) (A : Set X) : -- Distributiona product -------------------------------------------------------------------------- ---------------------------------------------------------------------------------------------------- -variable {X₁} [Vec R X₁] {Xβ‚‚} [Vec R Xβ‚‚] +variable {X₁} [Vec R X₁] {Xβ‚‚} [Vec R Xβ‚‚] {Y₁} [Vec R Y₁] {Yβ‚‚} [Vec R Yβ‚‚] -- can we extended to vector valued distributions? noncomputable -def Distribution.prod' (p : X₁ β†’ Xβ‚‚ β†’ X) (T : π’Ÿ' (X₁,Y)) (S : X₁ β†’ π’Ÿ' Xβ‚‚) : π’Ÿ'(X,Y) := - ⟨⟨fun Ο† => T.extAction (fun x₁ => (S x₁).extAction fun xβ‚‚ => Ο† (p x₁ xβ‚‚)), sorry_proof⟩⟩ - -noncomputable -abbrev Distribution.prod (T : π’Ÿ'(X₁,Y)) (S : π’Ÿ' Xβ‚‚) : π’Ÿ'(X₁×Xβ‚‚,Y) := prod' Prod.mk T (fun _ => S) +def Distribution.prod (p : X₁ β†’ Xβ‚‚ β†’ X) (T : π’Ÿ' (X₁,Y₁)) (S : X₁ β†’ π’Ÿ'(Xβ‚‚,Yβ‚‚)) (L : Y₁ ⊸ Yβ‚‚ ⊸ Z) : π’Ÿ'(X,Z) := + ⟨fun Ο† => T.extAction (fun x₁ => S x₁ ⟨fun xβ‚‚ => Ο† (p x₁ xβ‚‚), sorry_proof⟩) L, sorry_proof⟩ @[simp, ftrans_simp] -theorem Distribution.prod'_restrict (p : X₁ β†’ Xβ‚‚ β†’ X) (T : π’Ÿ'(X₁,Y)) (S : X₁ β†’ π’Ÿ' Xβ‚‚) (A : Set X) : - (prod' p T S).restrict A = prod' p (T.restrict (A.preimage1 p)) (fun x₁ => (S x₁).restrict (p x₁ ⁻¹' A)) := sorry_proof +theorem Distribution.prod_restrict (p : X₁ β†’ Xβ‚‚ β†’ X) (T : π’Ÿ'(X₁,Y₁)) (S : X₁ β†’ π’Ÿ'(Xβ‚‚,Yβ‚‚)) (L : Y₁ ⊸ Yβ‚‚ ⊸ Z) (A : Set X) : + (prod p T S L).restrict A = prod p (T.restrict (A.preimage1 p)) (fun x₁ => (S x₁).restrict (p x₁ ⁻¹' A)) L := sorry_proof @[action_push] -theorem Distribution.prod'_extAction (p : X₁ β†’ Xβ‚‚ β†’ X) (T : π’Ÿ'(X₁,Y)) (S : X₁ β†’ π’Ÿ' Xβ‚‚) (Ο† : X β†’ R) : - (prod' p T S).extAction Ο† = T.extAction (fun x₁ => (S x₁).extAction fun xβ‚‚ => Ο† (p x₁ xβ‚‚)) := sorry_proof +theorem Distribution.prod'_extAction (p : X₁ β†’ Xβ‚‚ β†’ X) (T : π’Ÿ'(X₁,Y₁)) (S : X₁ β†’ π’Ÿ'(Xβ‚‚,Yβ‚‚)) (L : Y₁ ⊸ Yβ‚‚ ⊸ Z) (K : Z ⊸ R ⊸ Z) (Ο† : X β†’ R) : + (prod p T S L).extAction Ο† K + = + T.extAction (fun x₁ => (S x₁).extAction (fun xβ‚‚ => Ο† (p x₁ xβ‚‚)) (fun yβ‚‚ ⊸ fun r ⊸ r β€’ yβ‚‚)) (fun y₁ ⊸ fun yβ‚‚ ⊸ K (L y₁ yβ‚‚) 1) := sorry_proof + +-- @[action_push] +-- theorem Distribution.prod'_extAction' (p : X₁ β†’ Xβ‚‚ β†’ X) (T : π’Ÿ'(X₁,Y₁)) (S : X₁ β†’ π’Ÿ'(Xβ‚‚,Yβ‚‚)) (L : Y₁ ⊸ Yβ‚‚ ⊸ U) (Ο† : X β†’ V) (K : U ⊸ V ⊸ W) : +-- (prod p T S L).extAction Ο† K +-- = +-- T.extAction (fun x₁ => (S x₁).extAction (fun xβ‚‚ => Ο† (p x₁ xβ‚‚)) (sorry : Yβ‚‚ ⊸ V ⊸ Yβ‚‚βŠ—V)) (fun y₁ ⊸ fun yv ⊸ ) := sorry_proof ---------------------------------------------------------------------------------------------------- @@ -391,89 +358,81 @@ theorem Distribution.prod'_extAction (p : X₁ β†’ Xβ‚‚ β†’ X) (T : π’Ÿ'(X₁,Y ---------------------------------------------------------------------------------------------------- noncomputable -def Distribution.postComp (T : π’Ÿ'(X,Y)) (f : Y β†’ Z) : π’Ÿ'(X,Z) := - if h : IsSmoothLinearMap R f then - ⟨fun Ο† ⊸ f βŸͺT,Ο†βŸ«βŸ© - else - 0 - -@[pp_dot] -noncomputable -abbrev Distribution.postExtAction (T : π’Ÿ'(X,π’Ÿ'(Y,Z))) (Ο† : Y β†’ R) : π’Ÿ'(X,Z) := - T.postComp (fun u => u.extAction Ο†) +def Distribution.postComp (T : π’Ÿ'(X,Y)) (f : Y ⊸ Z) : π’Ÿ'(X,Z) := fun Ο† ⊸ f (T Ο†) -noncomputable -abbrev Distribution.postRestrict (T : π’Ÿ'(X,π’Ÿ'(Y,Z))) (A : X β†’ Set Y) : π’Ÿ'(X,π’Ÿ'(Y,Z)) := - ⟨⟨fun Ο† => - ⟨fun ψ => sorry, - sorry_proof⟩, - sorry_proof⟩⟩ +-- @[pp_dot] +-- noncomputable +-- abbrev Distribution.postExtAction (T : π’Ÿ'(X,π’Ÿ'(Y,U))) (Ο† : Y β†’ V) (L : U ⊸ V ⊸ W) : π’Ÿ'(X,W) := +-- T.postComp (fun u ⊸ u.extAction Ο† L) +@[fun_prop] +theorem Distribution.postComp.arg_T.IsSmoothLinarMap_rule (T : W β†’ π’Ÿ'(X,Y)) (f : Y ⊸ Z) + (hT : IsSmoothLinearMap R T) : + IsSmoothLinearMap R (fun w => (T w).postComp f) := by unfold postComp; sorry_proof @[simp, ftrans_simp] theorem postComp_id (u : π’Ÿ'(X,Y)) : - (u.postComp (fun y => y)) = u := sorry_proof + (u.postComp (fun y ⊸ y)) = u := sorry_proof @[simp, ftrans_simp] -theorem postComp_comp (x : π’Ÿ'(X,U)) (g : U β†’ V) (f : V β†’ W) : +theorem postComp_comp (x : π’Ÿ'(X,U)) (g : U ⊸ V) (f : V ⊸ W) : (x.postComp g).postComp f = - x.postComp (fun u => f (g u)) := sorry_proof + x.postComp (fun u ⊸ f (g u)) := sorry_proof @[simp, ftrans_simp] -theorem postComp_assoc (x : π’Ÿ'(X,U)) (y : U β†’ π’Ÿ'(Y,V)) (f : V β†’ W) (Ο† : Y β†’ R) : - (x.postComp y).postComp (fun T => T.postComp f) +theorem postComp_assoc (x : π’Ÿ'(X,U)) (y : U ⊸ π’Ÿ'(Y,V)) (f : V ⊸ W) (Ο† : Y β†’ R) : + (x.postComp y).postComp (fun T ⊸ T.postComp f) = - (x.postComp (fun u => (y u).postComp f)) := sorry_proof + (x.postComp (fun u ⊸ (y u).postComp f)) := sorry_proof @[action_push] -theorem postComp_extAction (x : π’Ÿ'(X,U)) (y : U β†’ V) (Ο† : X β†’ R) : - (x.postComp y).extAction Ο† +theorem postComp_extAction (x : π’Ÿ'(X,U)) (f : U ⊸ V) (Ο† : X β†’ W) (L : V ⊸ W ⊸ Z) : + (x.postComp y).extAction Ο† L = - y (x.extAction Ο†) := sorry_proof + (x.extAction Ο† (fun u ⊸ fun w ⊸ L (f u) w)) := sorry_proof @[action_push] -theorem postComp_restrict_extAction (x : π’Ÿ'(X,U)) (y : U β†’ V) (A : Set X) (Ο† : X β†’ R) : - ((x.postComp y).restrict A).extAction Ο† +theorem postComp_restrict_extAction (x : π’Ÿ'(X,U)) (f : U ⊸ V) (A : Set X) (Ο† : X β†’ W) (L : V ⊸ W ⊸ Z) : + ((x.postComp f).restrict A).extAction Ο† L = - y ((x.restrict A).extAction Ο†) := sorry_proof - + ((x.restrict A).extAction Ο† (fun u ⊸ fun w ⊸ (L (f u) w))) := sorry_proof -@[simp, ftrans_simp, action_push] -theorem Distribution.zero_postExtAction (Ο† : Y β†’ R) : (0 : π’Ÿ'(X,π’Ÿ'(Y,Z))).postExtAction Ο† = 0 := by sorry_proof --- todo: this needs some integrability condition -@[action_push] -theorem Distribution.add_postExtAction (T T' : π’Ÿ'(X,π’Ÿ'(Y,Z))) (Ο† : Y β†’ R) : - (T + T').postExtAction Ο† = T.postExtAction Ο† + T'.postExtAction Ο† := by sorry_proof +-- @[simp, ftrans_simp, action_push] +-- theorem Distribution.zero_postExtAction (Ο† : Y β†’ R) : (0 : π’Ÿ'(X,π’Ÿ'(Y,Z))).postExtAction Ο† = 0 := by sorry_proof -@[action_push] -theorem Distribution.sub_postExtAction (T T' : π’Ÿ'(X,π’Ÿ'(Y,Z))) (Ο† : Y β†’ R) : - (T - T').postExtAction Ο† = T.postExtAction Ο† - T'.postExtAction Ο† := by sorry_proof - -@[action_push] -theorem Distribution.smul_postExtAction (r : R) (T : π’Ÿ'(X,π’Ÿ'(Y,Z))) (Ο† : Y β†’ R) : - (r β€’ T).postExtAction Ο† = r β€’ T.postExtAction Ο† := by sorry_proof +-- -- todo: this needs some integrability condition +-- @[action_push] +-- theorem Distribution.add_postExtAction (T T' : π’Ÿ'(X,π’Ÿ'(Y,Z))) (Ο† : Y β†’ R) : +-- (T + T').postExtAction Ο† = T.postExtAction Ο† + T'.postExtAction Ο† := by sorry_proof -@[action_push] -theorem Distribution.neg_postExtAction (T : π’Ÿ'(X,π’Ÿ'(Y,Z))) (Ο† : Y β†’ R) : - (- T).postExtAction Ο† = - T.postExtAction Ο† := by sorry_proof +-- @[action_push] +-- theorem Distribution.sub_postExtAction (T T' : π’Ÿ'(X,π’Ÿ'(Y,Z))) (Ο† : Y β†’ R) : +-- (T - T').postExtAction Ο† = T.postExtAction Ο† - T'.postExtAction Ο† := by sorry_proof -open BigOperators in -@[action_push] -theorem Distribution.fintype_sum_postExtAction {I} [Fintype I] (T : I β†’ π’Ÿ'(X,π’Ÿ'(Y,Z))) (Ο† : Y β†’ R) : - (βˆ‘ i, T i).postExtAction Ο† = βˆ‘ i, (T i).postExtAction Ο† := by sorry_proof +-- @[action_push] +-- theorem Distribution.smul_postExtAction (r : R) (T : π’Ÿ'(X,π’Ÿ'(Y,Z))) (Ο† : Y β†’ R) : +-- (r β€’ T).postExtAction Ο† = r β€’ T.postExtAction Ο† := by sorry_proof +-- @[action_push] +-- theorem Distribution.neg_postExtAction (T : π’Ÿ'(X,π’Ÿ'(Y,Z))) (Ο† : Y β†’ R) : +-- (- T).postExtAction Ο† = - T.postExtAction Ο† := by sorry_proof -@[action_push] -theorem Distribution.ifD_postExtAction (T T' : π’Ÿ'(X,π’Ÿ'(Y,Z))) (A : Set X) (Ο† : Y β†’ R) : - (ifD A then T else T').postExtAction Ο† = ifD A then T.postExtAction Ο† else T'.postExtAction Ο† := by sorry_proof +-- open BigOperators in +-- @[action_push] +-- theorem Distribution.fintype_sum_postExtAction {I} [Fintype I] (T : I β†’ π’Ÿ'(X,π’Ÿ'(Y,Z))) (Ο† : Y β†’ R) : +-- (βˆ‘ i, T i).postExtAction Ο† = βˆ‘ i, (T i).postExtAction Ο† := by sorry_proof -- @[action_push] --- theorem Distribution.indextype_sum_postExtAction {I} [IndexType I] (T : I β†’ π’Ÿ'(X,π’Ÿ'(Y,Z))) (Ο† : Y β†’ R) : --- (βˆ‘ i, T i).postExtAction Ο† = βˆ‘ i, (T i).postExtAction Ο† := by sorry_proof +-- theorem Distribution.ifD_postExtAction (T T' : π’Ÿ'(X,π’Ÿ'(Y,Z))) (A : Set X) (Ο† : Y β†’ R) : +-- (ifD A then T else T').postExtAction Ο† = ifD A then T.postExtAction Ο† else T'.postExtAction Ο† := by sorry_proof + +-- -- @[action_push] +-- -- theorem Distribution.indextype_sum_postExtAction {I} [IndexType I] (T : I β†’ π’Ÿ'(X,π’Ÿ'(Y,Z))) (Ο† : Y β†’ R) : +-- -- (βˆ‘ i, T i).postExtAction Ο† = βˆ‘ i, (T i).postExtAction Ο† := by sorry_proof ---------------------------------------------------------------------------------------------------- @@ -483,11 +442,11 @@ theorem Distribution.ifD_postExtAction (T T' : π’Ÿ'(X,π’Ÿ'(Y,Z))) (A : Set X) @[coe] noncomputable def _root_.Function.toDistribution (f : X β†’ Y) : π’Ÿ'(X,Y) := - ⟨fun Ο† ⊸ ∫' x, Ο† x β€’ f x⟩ + fun Ο† ⊸ ∫' x, Ο† x β€’ f x def Distribution.IsFunction (T : π’Ÿ'(X,Y)) : Prop := βˆƒ (f : X β†’ Y), βˆ€ (Ο† : π’Ÿ X), - βŸͺT, Ο†βŸ« = ∫' x, Ο† x β€’ f x + T Ο† = ∫' x, Ο† x β€’ f x noncomputable def Distribution.toFunction (T : π’Ÿ'(X,Y)) : X β†’ Y := @@ -498,11 +457,11 @@ def Distribution.toFunction (T : π’Ÿ'(X,Y)) : X β†’ Y := @[action_push] theorem Function.toDistribution_action (f : X β†’ Y) (Ο† : π’Ÿ X) : - βŸͺf.toDistribution, Ο†βŸ« = ∫' x, Ο† x β€’ f x := by rfl + f.toDistribution Ο† = ∫' x, Ο† x β€’ f x := by rfl @[action_push] theorem Function.toDistribution_extAction (f : X β†’ Y) (Ο† : X β†’ R) : - f.toDistribution.extAction Ο† + f.toDistribution.extAction Ο† (fun y ⊸ fun r ⊸ r β€’ y) = ∫' x, Ο† x β€’ f x := sorry_proof @@ -521,14 +480,14 @@ variable [MeasurableSpace X] noncomputable def _root_.MeasureTheory.Measure.toDistribution (ΞΌ : Measure X) : π’Ÿ' X := - ⟨fun Ο† ⊸ ∫' x, Ο† x βˆ‚ΞΌβŸ© + fun Ο† ⊸ ∫' x, Ο† x βˆ‚ΞΌ noncomputable instance : Coe (Measure X) (π’Ÿ' X) := ⟨fun ΞΌ => ΞΌ.toDistribution⟩ def Distribution.IsMeasure (f : π’Ÿ' X) : Prop := βˆƒ (ΞΌ : Measure X), βˆ€ (Ο† : π’Ÿ X), - βŸͺf, Ο†βŸ« = ∫' x, Ο† x βˆ‚ΞΌ + f Ο† = ∫' x, Ο† x βˆ‚ΞΌ open Classical noncomputable diff --git a/SciLean/Core/Distribution/Eval.lean b/SciLean/Core/Distribution/Eval.lean index 6f8d6c48..55fcad5e 100644 --- a/SciLean/Core/Distribution/Eval.lean +++ b/SciLean/Core/Distribution/Eval.lean @@ -8,11 +8,11 @@ namespace SciLean variable {R} [RealScalar R] - {X} [TopologicalSpace X] [space : TCOr (Vec R X) (DiscreteTopology X)] - {Y} [Vec R Y] + {X} [Vec R X] -- [TopologicalSpace X] [space : TCOr (Vec R X) (DiscreteTopology X)] + {Y} [Vec R Y] [Module ℝ Y] {Z} [Vec R Z] {U} [Vec R U] - {V} [Vec R V] + {V} [Vec R V] [Module ℝ V] {W} [Vec R W] set_default_scalar R @@ -21,48 +21,55 @@ open Classical @[action_push] theorem action_extAction (T : π’Ÿ' X) (Ο† : π’Ÿ X) : - T.action Ο† = T.extAction Ο† := sorry_proof + T Ο† = T.extAction' Ο† := sorry_proof @[action_push] -theorem extAction_vecDirac (x : X) (Ο† : X β†’ R) : - (dirac x).extAction Ο† +theorem extAction_vecDirac (x : X) (Ο† : X β†’ Y) (L : R ⊸ Y ⊸ Z) : + (dirac x).extAction Ο† L = - Ο† x := sorry_proof + L 1 (Ο† x) := sorry_proof @[action_push] -theorem extAction_restrict_vecDirac (x : X) (A : Set X) (Ο† : X β†’ R) : - ((dirac x).restrict A).extAction Ο† +theorem extAction_restrict_vecDirac (x : X) (A : Set X) (Ο† : X β†’ Y) (L : R ⊸ Y ⊸ Z) : + ((dirac x).restrict A).extAction Ο† L = - if x ∈ A then Ο† x else 0 := sorry_proof + if x ∈ A then L 1 (Ο† x) else 0 := sorry_proof -- x.postComp (fun u => (y u).extAction Ο†) := by sorry_proof @[action_push] -theorem postExtAction_postComp (x : π’Ÿ'(X,U)) (y : U β†’ π’Ÿ'(Y,Z)) (Ο† : Y β†’ R) : - (x.postComp y).postExtAction Ο† +theorem postExtAction_postComp (x : π’Ÿ'(X,U)) (y : U ⊸ π’Ÿ'(Y,Z)) (Ο† : Y β†’ R) : + (x.postComp y).postComp (⟨fun T => T.extAction' Ο†, by unfold Distribution.extAction'; fun_prop⟩) = - x.postComp (fun u => (y u).extAction Ο†) := by sorry_proof + x.postComp (⟨fun u => (y u).extAction' Ο†, by unfold Distribution.extAction'; fun_prop⟩) := by sorry_proof variable [MeasureSpace X] open Rand in @[action_push] -theorem function_toDistribution_eval (f : X β†’ R) (A : Set X) (Ο† : X β†’ R) [UniformRand A] : - (f.toDistribution.restrict A).extAction Ο† +theorem function_toDistribution_eval (f : X β†’ Y) (A : Set X) (Ο† : X β†’ U) (L : Y ⊸ U ⊸ V) [UniformRand A] : + (f.toDistribution.restrict A).extAction Ο† L = (uniform A).E fun x => let V : R := Scalar.ofENNReal (volume A) - V β€’ f x * Ο† x := sorry_proof + V β€’ L (f x) (Ο† x) := sorry_proof open Rand in @[action_push] -theorem function_toDistribution_eval_restrict (f : X β†’ R) (B A : Set X) (Ο† : X β†’ R) [UniformRand A] : - ((f.toDistribution.restrict B).restrict A).extAction Ο† +theorem function_toDistribution_eval_restrict (f : X β†’ Y) (B A : Set X) (Ο† : X β†’ U) (L : Y ⊸ U ⊸ V) [UniformRand A] : + ((f.toDistribution.restrict B).restrict A).extAction Ο† L = (uniform A).E fun x => let V : R := Scalar.ofENNReal (volume A) if x.1 ∈ B then - V β€’ f x * Ο† x + V β€’ L (f x) (Ο† x) else 0 := sorry_proof + + +@[simp, ftrans_simp, action_push] +theorem function_toDistribution_extAction_unit {X} [Vec R X] [Module ℝ X] (f : Unit β†’ X) (Ο† : Unit β†’ Y) (L : X ⊸ Y ⊸ Z) : + f.toDistribution.extAction Ο† L + = + L (f ()) (Ο† ()) := sorry_proof diff --git a/SciLean/Core/Distribution/ParametricDistribDeriv.lean b/SciLean/Core/Distribution/ParametricDistribDeriv.lean index 11b7f062..a5633426 100644 --- a/SciLean/Core/Distribution/ParametricDistribDeriv.lean +++ b/SciLean/Core/Distribution/ParametricDistribDeriv.lean @@ -17,24 +17,25 @@ variable {Y} [Vec R Y] [Module ℝ Y] {Z} [Vec R Z] [Module ℝ Z] {U} [Vec R U] -- [Module ℝ U] + {V} [Vec R V] -- [Module ℝ U] set_default_scalar R noncomputable -def diracDeriv (x dx : X) : π’Ÿ' X := ⟨fun Ο† ⊸ cderiv R Ο† x dx⟩ +def diracDeriv (x dx : X) : π’Ÿ' X := fun Ο† ⊸ cderiv R Ο† x dx @[fun_prop] def DistribDifferentiableAt (f : X β†’ π’Ÿ'(Y,Z)) (x : X) := - βˆ€ (Ο† : X β†’ π’Ÿ Y), CDifferentiableAt R Ο† x β†’ CDifferentiableAt R (fun x => βŸͺf x, Ο† x⟫) x + βˆ€ (Ο† : X β†’ π’Ÿ Y), CDifferentiableAt R Ο† x β†’ CDifferentiableAt R (fun x => f x (Ο† x)) x theorem distribDifferentiableAt_const_test_fun {f : X β†’ π’Ÿ'(Y,Z)} {x : X} (hf : DistribDifferentiableAt f x) {Ο† : π’Ÿ Y} : - CDifferentiableAt R (fun x => βŸͺf x, Ο†βŸ«) x := by + CDifferentiableAt R (fun x => f x Ο†) x := by apply hf fun_prop @@ -57,12 +58,12 @@ open Classical in @[fun_trans] noncomputable def parDistribDeriv (f : X β†’ π’Ÿ'(Y,Z)) (x dx : X) : π’Ÿ'(Y,Z) := - ⟨⟨fun Ο† => βˆ‚ (x':=x;dx), βŸͺf x', Ο†βŸ«, sorry_proof⟩⟩ + ⟨fun Ο† => βˆ‚ (x':=x;dx), f x' Ο†, sorry_proof⟩ @[simp, ftrans_simp] theorem action_parDistribDeriv (f : X β†’ π’Ÿ'(Y,Z)) (x dx : X) (Ο† : π’Ÿ Y) : - βŸͺparDistribDeriv f x dx, Ο†βŸ« = βˆ‚ (x':=x;dx), βŸͺf x', Ο†βŸ« := rfl + parDistribDeriv f x dx Ο† = βˆ‚ (x':=x;dx), f x' Ο† := rfl ---------------------------------------------------------------------------------------------------- @@ -126,7 +127,7 @@ theorem DistribDiffrentiable.comp_rule intro x unfold DistribDifferentiableAt intro Ο† hΟ† - apply CDifferentiable.comp_rule (K:=R) (f:=fun xy : XΓ—Y => βŸͺf xy.2,Ο† xy.1⟫) (g:=fun x => (x, g x)) + apply CDifferentiable.comp_rule (K:=R) (f:=fun xy : XΓ—Y => f xy.2 (Ο† xy.1)) (g:=fun x => (x, g x)) (hg:=by fun_prop) intro x sorry_proof -- is this even true ? @@ -157,10 +158,10 @@ theorem parDistribDeriv.comp_rule -- I think `f` has to be `deg` @[fun_prop] theorem Bind.bind.arg_fx.DistribDifferentiable_rule - (f : X β†’ Y β†’ π’Ÿ' Z) (g : X β†’ π’Ÿ' Y) + (f : X β†’ Y β†’ π’Ÿ'(Z,V)) (g : X β†’ π’Ÿ'(Y,U)) (L : U ⊸ V ⊸ W) (hf : DistribDifferentiable (fun (x,y) => f x y)) -- `f` has to be nice enough to accomodate action of `g` (hg : DistribDifferentiable g) : - DistribDifferentiable (fun x => (g x).bind (f x)) := by + DistribDifferentiable (fun x => (g x).bind (f x) L) := by intro x unfold DistribDifferentiableAt @@ -171,15 +172,15 @@ theorem Bind.bind.arg_fx.DistribDifferentiable_rule @[fun_trans] theorem Bind.bind.arg_fx.parDistribDiff_rule - (f : X β†’ Y β†’ π’Ÿ' Z) (g : X β†’ π’Ÿ' Y) + (f : X β†’ Y β†’ π’Ÿ'(Z,V)) (g : X β†’ π’Ÿ'(Y,U)) (L : U ⊸ V ⊸ W) (hf : DistribDifferentiable (fun (x,y) => f x y)) -- `f` has to be nice enough to accomodate action of `g` (hg : DistribDifferentiable g) : - parDistribDeriv (fun x => (g x).bind (f x)) + parDistribDeriv (fun x => (g x).bind (f x) L) = fun x dx => - ((parDistribDeriv g x dx).bind (f x Β· )) + ((parDistribDeriv g x dx).bind (f x Β· ) L) + - ((g x).bind (fun y => parDistribDeriv (f Β· y) x dx)) := sorry_proof + ((g x).bind (fun y => parDistribDeriv (f Β· y) x dx) L) := sorry_proof @@ -217,11 +218,11 @@ theorem toDistribution.linear_parDistribDeriv_rule (f : W β†’ X β†’ Y) (L : Y parDistribDeriv (fun w => (fun x => L (f w x)).toDistribution) = fun w dw => - parDistribDeriv Tf w dw |>.postComp L := by + parDistribDeriv (fun w => (fun x => f w x).toDistribution) w dw |>.postComp (fun y ⊸ L y) := by funext w dw unfold parDistribDeriv Distribution.postComp Function.toDistribution ext Ο† - simp [ftrans_simp, Distribution.mk_extAction_simproc] + simp [ftrans_simp] -- , Distribution.mk_extAction_simproc] sorry_proof @@ -235,11 +236,11 @@ variable [MeasureSpace X] [MeasureSpace Y] [MeasureSpace (XΓ—Y)] open Notation @[fun_trans] -theorem cintegral.arg_f.cderiv_distrib_rule (f : W β†’ X β†’ R) : +theorem cintegral.arg_f.cderiv_distrib_rule (f : W β†’ X β†’ Y) : cderiv R (fun w => ∫' x, f w x) = fun w dw => - (parDistribDeriv (fun w => (f w Β·).toDistribution) w dw).extAction (fun _ => 1) := sorry_proof + (parDistribDeriv (fun w => (f w Β·).toDistribution) w dw).extAction (fun _ => (1:R)) (fun y ⊸ fun r ⊸ r β€’ y) := sorry_proof @[fun_trans] @@ -247,33 +248,30 @@ theorem cintegral.arg_f.cderiv_distrib_rule' (f : W β†’ X β†’ R) (A : Set X): cderiv R (fun w => ∫' x in A, f w x) = fun w dw => - (parDistribDeriv (fun w => (f w Β·).toDistribution) w dw).restrict A |>.extAction fun _ => 1 := sorry_proof - --- (parDistribDeriv (fun w => (f w Β·).toDistribution) w dw).extAction (fun x => if x ∈ A then 1 else 0) := sorry_proof - + (parDistribDeriv (fun w => (f w Β·).toDistribution) w dw).restrict A |>.extAction (fun _ => (1:R)) (fun y ⊸ fun r ⊸ r β€’ y) := sorry_proof @[fun_trans] -theorem cintegral.arg_f.parDistribDeriv_rule (f : W β†’ X β†’ Y β†’ R) : - parDistribDeriv (fun w => (fun x => ∫' y, f w x y).toDistribution) +theorem cintegral.arg_f.parDistribDeriv_rule (f : W β†’ X β†’ Y β†’ Z) : + parDistribDeriv (fun w => (fun x => ∫' y, f w x y).toDistribution (R:=R)) = fun w dw => let Tf := (fun w => (fun x => (fun y => f w x y).toDistribution (R:=R)).toDistribution (R:=R)) - parDistribDeriv Tf w dw |>.postExtAction (fun _ => 1) := by + parDistribDeriv Tf w dw |>.postComp (fun T ⊸ T.extAction (fun _ => (1:R)) (fun z ⊸ fun r ⊸ r β€’ z)) := by funext w dw - unfold postExtAction parDistribDeriv postComp Function.toDistribution + unfold parDistribDeriv postComp Function.toDistribution ext Ο† - simp [ftrans_simp, Distribution.mk_extAction_simproc] + simp [ftrans_simp] -- , Distribution.mk_extAction_simproc] sorry_proof @[fun_trans] -theorem cintegral.arg_f.parDistribDeriv_rule' (f : W β†’ X β†’ Y β†’ R) (B : X β†’ Set Y) : +theorem cintegral.arg_f.parDistribDeriv_rule' (f : W β†’ X β†’ Y β†’ Z) (B : X β†’ Set Y) : parDistribDeriv (fun w => (fun x => ∫' y in B x, f w x y).toDistribution) = fun w dw => let Tf := (fun w => (fun x => ((fun y => f w x y).toDistribution (R:=R)).restrict (B x)).toDistribution (R:=R)) - parDistribDeriv Tf w dw |>.postExtAction (fun _ => 1) := sorry_proof + parDistribDeriv Tf w dw |>.postComp (fun T ⊸ T.extAction (fun _ => (1:R)) (fun z ⊸ fun r ⊸ r β€’ z)) := sorry_proof @@ -284,21 +282,21 @@ theorem cintegral.arg_f.parDistribDeriv_rule' (f : W β†’ X β†’ Y β†’ R) (B : X ---------------------------------------------------------------------------------------------------- @[fun_prop] -theorem HAdd.hAdd.arg_a0a1.DistribDifferentiable_rule (f g : W β†’ X β†’ R) +theorem HAdd.hAdd.arg_a0a1.DistribDifferentiable_rule (f g : W β†’ X β†’ Y) /- (hf : βˆ€ x, CDifferentiable R (f Β· x)) (hg : βˆ€ x, CDifferentiable R (g Β· x)) -/ : - DistribDifferentiable (fun w => (fun x => f w x + g w x).toDistribution) := by + DistribDifferentiable (fun w => (fun x => f w x + g w x).toDistribution (R:=R)) := by intro _ Ο† hΟ†; simp; sorry_proof -- fun_prop (disch:=assumption) -- we probably only require local integrability in `x` of f and g for this to be true @[fun_trans] -theorem HAdd.hAdd.arg_a0a1.parDistribDeriv_rule (f g : W β†’ X β†’ R) +theorem HAdd.hAdd.arg_a0a1.parDistribDeriv_rule (f g : W β†’ X β†’ Y) /- (hf : βˆ€ x, CDifferentiable R (f Β· x)) (hg : βˆ€ x, CDifferentiable R (g Β· x)) -/ : parDistribDeriv (fun w => (fun x => f w x + g w x).toDistribution) = fun w dw => parDistribDeriv (fun w => (f w Β·).toDistribution) w dw + - parDistribDeriv (fun w => (g w Β·).toDistribution) w dw := by + parDistribDeriv (fun w => (g w Β·).toDistribution (R:=R)) w dw := by funext w dw; ext Ο†; simp[parDistribDeriv] sorry_proof @@ -308,21 +306,21 @@ theorem HAdd.hAdd.arg_a0a1.parDistribDeriv_rule (f g : W β†’ X β†’ R) ---------------------------------------------------------------------------------------------------- @[fun_prop] -theorem HSub.hSub.arg_a0a1.DistribDifferentiable_rule (f g : W β†’ X β†’ R) +theorem HSub.hSub.arg_a0a1.DistribDifferentiable_rule (f g : W β†’ X β†’ Y) /- (hf : βˆ€ x, CDifferentiable R (f Β· x)) (hg : βˆ€ x, CDifferentiable R (g Β· x)) -/ : - DistribDifferentiable (fun w => (fun x => f w x - g w x).toDistribution) := by + DistribDifferentiable (fun w => (fun x => f w x - g w x).toDistribution (R:=R)) := by intro _ Ο† hΟ†; simp; sorry_proof -- fun_prop (disch:=assumption) @[fun_trans] -theorem HSub.hSub.arg_a0a1.parDistribDeriv_rule (f g : W β†’ X β†’ R) +theorem HSub.hSub.arg_a0a1.parDistribDeriv_rule (f g : W β†’ X β†’ Y) /- (hf : βˆ€ x, CDifferentiable R (f Β· x)) (hg : βˆ€ x, CDifferentiable R (g Β· x)) -/ : parDistribDeriv (fun w => (fun x => f w x - g w x).toDistribution) = fun w dw => parDistribDeriv (fun w => (f w Β·).toDistribution) w dw - - parDistribDeriv (fun w => (g w Β·).toDistribution) w dw := by + parDistribDeriv (fun w => (g w Β·).toDistribution (R:=R)) w dw := by funext w dw; ext Ο†; simp[parDistribDeriv] sorry_proof @@ -334,7 +332,7 @@ theorem HSub.hSub.arg_a0a1.parDistribDeriv_rule (f g : W β†’ X β†’ R) @[fun_prop] theorem HMul.hMul.arg_a0a1.DistribDifferentiable_rule (f : W β†’ X β†’ R) (r : R) /- (hf : βˆ€ x, CDifferentiable R (f Β· x)) (hg : βˆ€ x, CDifferentiable R (g Β· x)) -/ : - DistribDifferentiable (fun w => (fun x => r * f w x).toDistribution) := by + DistribDifferentiable (fun w => (fun x => r * f w x).toDistribution (R:=R)) := by intro _ Ο† hΟ†; simp; sorry_proof -- fun_prop (disch:=assumption) @@ -344,11 +342,34 @@ theorem HMul.hMul.arg_a0a1.parDistribDeriv_rule (f : W β†’ X β†’ R) (r : R) parDistribDeriv (fun w => (fun x => r * f w x).toDistribution) = fun w dw => - r β€’ (parDistribDeriv (fun w => (f w Β·).toDistribution) w dw) := by + r β€’ (parDistribDeriv (fun w => (f w Β·).toDistribution (R:=R)) w dw) := by funext w dw; ext Ο†; simp[parDistribDeriv] sorry_proof +---------------------------------------------------------------------------------------------------- +-- Smul --------------------------------------------------------------------------------------------- +---------------------------------------------------------------------------------------------------- + +@[fun_prop] +theorem HSMul.hSMul.arg_a0a1.DistribDifferentiable_rule (f : W β†’ X β†’ Y) (r : R) + /- (hf : βˆ€ x, CDifferentiable R (f Β· x)) (hg : βˆ€ x, CDifferentiable R (g Β· x)) -/ : + DistribDifferentiable (fun w => (fun x => r β€’ f w x).toDistribution (R:=R)) := by + intro _ Ο† hΟ†; simp; sorry_proof -- fun_prop (disch:=assumption) + + +@[fun_trans] +theorem HSMul.hSMul.arg_a0a1.parDistribDeriv_rule (f : W β†’ X β†’ Y) (r : R) + /- (hf : βˆ€ x, CDifferentiable R (f Β· x)) (hg : βˆ€ x, CDifferentiable R (g Β· x)) -/ : + parDistribDeriv (fun w => (fun x => r β€’ f w x).toDistribution) + = + fun w dw => + r β€’ (parDistribDeriv (fun w => (f w Β·).toDistribution (R:=R)) w dw) := by + funext w dw; ext Ο†; simp[parDistribDeriv] + sorry_proof + + + ---------------------------------------------------------------------------------------------------- -- Div --------------------------------------------------------------------------------------------- ---------------------------------------------------------------------------------------------------- @@ -356,7 +377,7 @@ theorem HMul.hMul.arg_a0a1.parDistribDeriv_rule (f : W β†’ X β†’ R) (r : R) @[fun_prop] theorem HDiv.hDiv.arg_a0a1.DistribDifferentiable_rule (f : W β†’ X β†’ R) (r : R) /- (hf : βˆ€ x, CDifferentiable R (f Β· x)) (hg : βˆ€ x, CDifferentiable R (g Β· x)) -/ : - DistribDifferentiable (fun w => (fun x => f w x / r).toDistribution) := by + DistribDifferentiable (fun w => (fun x => f w x / r).toDistribution (R:=R)) := by intro _ Ο† hΟ†; simp; sorry_proof -- fun_prop (disch:=assumption) @@ -366,6 +387,6 @@ theorem HDiv.hDiv.arg_a0a1.parDistribDeriv_rule (f : W β†’ X β†’ R) (r : R) parDistribDeriv (fun w => (fun x => f w x / r).toDistribution) = fun w dw => - r⁻¹ β€’ (parDistribDeriv (fun w => (f w Β·).toDistribution) w dw) := by + r⁻¹ β€’ (parDistribDeriv (fun w => (f w Β·).toDistribution (R:=R)) w dw) := by funext w dw; ext Ο†; simp[parDistribDeriv] sorry_proof diff --git a/SciLean/Core/Distribution/ParametricDistribFwdDeriv.lean b/SciLean/Core/Distribution/ParametricDistribFwdDeriv.lean index 207ee380..aa1db660 100644 --- a/SciLean/Core/Distribution/ParametricDistribFwdDeriv.lean +++ b/SciLean/Core/Distribution/ParametricDistribFwdDeriv.lean @@ -24,8 +24,8 @@ set_default_scalar R @[fun_trans] noncomputable def parDistribFwdDeriv (f : X β†’ π’Ÿ'(Y,Z)) (x dx : X) : π’Ÿ'(Y,ZΓ—Z) := - let dz := parDistribDeriv f x dx |>.postComp (fun dz => ((0:Z),dz)) - let z := f x |>.postComp (fun z => (z,(0:Z))) + let dz := parDistribDeriv f x dx |>.postComp (fun dz ⊸ ((0:Z),dz)) + let z := f x |>.postComp (fun z ⊸ (z,(0:Z))) z + dz @@ -46,64 +46,52 @@ theorem comp_rule fun_trans [action_push,fwdDeriv] -@[simp, ftrans_simp] -theorem asdf (u : π’Ÿ'(X,Y)) (f : Y β†’ Z) (Ο† : π’Ÿ X) : - (u.postComp f).action Ο† = f (u.action Ο†) := sorry_proof +-- @[simp, ftrans_simp] +-- theorem asdf (u : π’Ÿ'(X,Y)) (f : Y ⊸ Z) (Ο† : π’Ÿ X) : +-- (u.postComp f) Ο† = f (u Ο†) := by rfl -@[simp, ftrans_simp] -theorem asdf' (u : π’Ÿ'(X,Y)) (f : Y β†’ Z) (Ο† : X β†’ R) : - (u.postComp f).extAction Ο† = f (u.extAction Ο†) := sorry_proof +-- @[simp, ftrans_simp] +-- theorem asdf' (u : π’Ÿ'(X,Y)) (f : Y ⊸ Z) (Ο† : X β†’ R) (L) : +-- (u.postComp f).extAction Ο† L = (u.extAction Ο† (fun x ⊸ fun y ⊸ L (f x) y)) := sorry_proof -@[simp, ftrans_simp] -theorem asdf'' (u : π’Ÿ'(X,U)) (f : U β†’ Y) (Ο† : X β†’ Z) (L : Y β†’ Z β†’ W) : - (u.postComp f).extAction' Ο† L = u.extAction' Ο† (fun u z => L (f u) z) := sorry_proof +-- @[simp, ftrans_simp] +-- theorem asdf'' (u : π’Ÿ'(X,U)) (f : U β†’ Y) (Ο† : X β†’ Z) (L : Y β†’ Z β†’ W) : +-- (u.postComp f).extAction' Ο† L = u.extAction' Ο† (fun u z => L (f u) z) := sorry_proof -@[simp, ftrans_simp] -theorem asdf''' (u : π’Ÿ'(X,Y)) (Ο† : X β†’ U) (ψ : X β†’ V) (L : Y β†’ (UΓ—V) β†’ W) : - u.extAction' (fun x => (Ο† x, ψ x)) L - = - u.extAction' Ο† (fun y u => L y (u,0)) - + - u.extAction' ψ (fun y v => L y (0,v)) := sorry_proof +-- @[simp, ftrans_simp] +-- theorem asdf''' (u : π’Ÿ'(X,Y)) (Ο† : X β†’ U) (ψ : X β†’ V) (L : Y β†’ (UΓ—V) β†’ W) : +-- u.extAction' (fun x => (Ο† x, ψ x)) L +-- =x` +-- u.extAction' Ο† (fun y u => L y (u,0)) +-- + +-- u.extAction' ψ (fun y v => L y (0,v)) := sorry_proof -@[simp, ftrans_simp] -theorem asdf'''' (u : π’Ÿ'(X,Y)) (Ο† : X β†’ R) (L : Y β†’ R β†’ Y) : - u.extAction' Ο† L - = - L (u.extAction Ο†) 1 := sorry_proof +-- @[simp, ftrans_simp] +-- theorem asdf'''' (u : π’Ÿ'(X,Y)) (Ο† : X β†’ R) (L : Y β†’ R β†’ Y) : +-- u.extAction' Ο† L +-- = +-- L (u.extAction Ο†) 1 := sorry_proof theorem bind_rule - (f : X β†’ Y β†’ π’Ÿ' Z) (g : X β†’ π’Ÿ' Y) + (f : X β†’ Y β†’ π’Ÿ'(Z,V)) (g : X β†’ π’Ÿ'(Y,U)) (L : U ⊸ V ⊸ W) (hf : DistribDifferentiable (fun (x,y) => f x y)) (hg : DistribDifferentiable g) : - parDistribFwdDeriv (fun x => (g x).bind (f x)) + parDistribFwdDeriv (fun x => (g x).bind (f x) L) = fun x dx => let ydy := parDistribFwdDeriv g x dx let zdz := fun y => parDistribFwdDeriv (f Β· y) x dx - ydy.bind' zdz (fun (r,dr) (s,ds) => (r*s, r*ds + s*dr)) := by + ydy.bind zdz (fun (r,dr) ⊸ fun (s,ds) ⊸ (L r s, L r ds + L dr s)) := by - unfold parDistribFwdDeriv Distribution.bind' + unfold parDistribFwdDeriv Distribution.bind autodiff funext x dx fun_trans [action_push,fwdDeriv] ext Ο† - simp only [ftrans_simp, action_push] - simp only [ftrans_simp, action_push] - - - - -theorem bind_rule' - (f : X β†’ Y β†’ π’Ÿ'(Z,V)) (g : X β†’ π’Ÿ'(Y,U)) (L : U β†’ V β†’ W) - (hf : DistribDifferentiable (fun (x,y) => f x y)) (hg : DistribDifferentiable g) - (hL₁ : βˆ€ u, IsSmoothLinearMap R (L u Β·)) (hLβ‚‚ : βˆ€ v, IsSmoothLinearMap R (L Β· v)) : - parDistribFwdDeriv (fun x => (g x).bind' (f x) L) - = - fun x dx => - let ydy := parDistribFwdDeriv g x dx - let zdz := fun y => parDistribFwdDeriv (f Β· y) x dx - ydy.bind' zdz (fun (r,dr) (s,ds) => (L r s, L r ds + L dr s)) := sorry_proof + simp only [ftrans_simp, action_push, postComp] + sorry_proof + sorry_proof + -- simp only [ftrans_simp, action_push] diff --git a/SciLean/Core/Distribution/ParametricDistribRevDeriv.lean b/SciLean/Core/Distribution/ParametricDistribRevDeriv.lean index 64341d05..76d143af 100644 --- a/SciLean/Core/Distribution/ParametricDistribRevDeriv.lean +++ b/SciLean/Core/Distribution/ParametricDistribRevDeriv.lean @@ -26,15 +26,13 @@ set_default_scalar R @[fun_trans] 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 z := βŸͺf x, Ο†βŸ« - (z, dz), sorry_proof⟩⟩ - + ⟨fun Ο† => + let dz := semiAdjoint R (fun dx => parDistribDeriv 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) : @@ -43,41 +41,30 @@ 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))) := by + udf.postComp (⟨fun (u,df') => (u, fun du => ydg.2 (df' du)), sorry_proof⟩) := by - unfold parDistribRevDeriv + 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 : βˆ€ x, HasSemiAdjoint R (βˆ‚ x':=x, f x' Ο†) := sorry_proof -- todo add: `DistribHasAdjDiff` fun_trans - theorem bind_rule - (f : X β†’ Y β†’ π’Ÿ' Z) (g : X β†’ π’Ÿ' Y) : - parDistribRevDeriv (fun x => (g x).bind (f x)) - = - fun x => - let ydg := parDistribRevDeriv g x - let zdf := fun y => parDistribRevDeriv (f Β· y) x - ydg.bind' zdf (fun (_,dg) (z,df) => (z, fun dr => dg dr + df dr)) := sorry_proof - - -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) + (f : X β†’ Y β†’ π’Ÿ'(Z,V)) (g : X β†’ π’Ÿ'(Y,U)) (L : U ⊸ V ⊸ W) : + parDistribRevDeriv (fun x => (g x).bind (f x) L) = fun x => let ydg := parDistribRevDeriv g x let zdf := fun y => parDistribRevDeriv (f Β· y) x - ydg.bind' zdf (fun (u,dg) (v,df) => + ydg.bind zdf (⟨fun (u,dg) => ⟨fun (v,df) => (L u v, fun dw => df (semiAdjoint R (L u Β·) dw) + - dg (semiAdjoint R (L Β· v) dw))) := by + dg (semiAdjoint R (L Β· v) dw)), sorry_proof⟩, sorry_proof⟩) := by - unfold parDistribRevDeriv bind' + unfold parDistribRevDeriv Distribution.bind funext x; ext Ο† simp sorry_proof @@ -91,7 +78,7 @@ theorem bind_rule' noncomputable def diracRevDeriv (x : X) : π’Ÿ'(X,RΓ—(Rβ†’X)) := - ⟨⟨fun Ο† => revDeriv R Ο† x, sorry_proof⟩⟩ + ⟨fun Ο† => revDeriv R Ο† x, sorry_proof⟩ @[fun_trans] @@ -101,13 +88,9 @@ theorem dirac.arg_xy.parDistribRevDeriv_rule = fun w => let xdx := revDeriv R x w - diracRevDeriv xdx.1 |>.postComp (fun (r,dΟ†) => (r, fun dr => xdx.2 (dΟ† dr))) := by + diracRevDeriv xdx.1 |>.postComp (⟨fun (r,dΟ†) => (r, fun dr => xdx.2 (dΟ† dr)), sorry_proof⟩) := by funext w; apply Distribution.ext _ _; intro Ο† have : HasAdjDiff R Ο† := sorry_proof -- this should be consequence of that `R` has dimension one - simp [diracRevDeriv,revDeriv, parDistribRevDeriv] + simp [diracRevDeriv,revDeriv, parDistribRevDeriv, postComp] fun_trans - - - -#check Distribution.postComp diff --git a/SciLean/Core/Distribution/SimpleExamples.lean b/SciLean/Core/Distribution/SimpleExamples.lean index e49d8eb8..dbadd619 100644 --- a/SciLean/Core/Distribution/SimpleExamples.lean +++ b/SciLean/Core/Distribution/SimpleExamples.lean @@ -49,6 +49,8 @@ theorem foo1_spec (t : R) : open Classical in +set_option pp.funBinderTypes true in + def foo2 (t' : R) := (βˆ‚ (t:=t'), ∫' (x:R) in Ioo 0 1, if x - t ≀ 0 then (1:R) else 0) rewrite_by fun_trans only [scalarGradient, scalarCDeriv] @@ -66,6 +68,7 @@ def foo2 (t' : R) := (βˆ‚ (t:=t'), ∫' (x:R) in Ioo 0 1, if x - t ≀ 0 then (1 fun_trans simp only [action_push, ftrans_simp] +#check instTCOr_1 theorem foo2_spec (t : R) : foo2 t = if 0 < t ∧ t < 1 then 1 else 0 := by rfl @@ -74,6 +77,8 @@ theorem foo2_spec (t : R) : #eval foo2 (-1.0) #eval foo2 2.0 +set_option pp.funBinderTypes true in + def foo3 (t' : R) := (βˆ‚ (t:=t'), ∫' (x:R) in Ioo (-1) 1, if x^2 - t ≀ 0 then (1:R) else 0) rewrite_by assuming (_ : 0 < t') fun_trans only [scalarGradient, scalarCDeriv] diff --git a/SciLean/Core/Distribution/SimpleExamples2D.lean b/SciLean/Core/Distribution/SimpleExamples2D.lean index fec4a952..25a7cdc8 100644 --- a/SciLean/Core/Distribution/SimpleExamples2D.lean +++ b/SciLean/Core/Distribution/SimpleExamples2D.lean @@ -71,16 +71,9 @@ def foo1' (t' : R) := derive_random_approx (βˆ‚ (t:=t'), ∫' (x : R) in Ioo 0 1, ∫' (y : R) in Ioo 0 1, if x ≀ t then (1:R) else 0) by - fun_trans only [scalarGradient, scalarCDeriv] - simp only [ftrans_simp] - simp only [Tactic.if_pull] - fun_trans only [scalarGradient, scalarCDeriv,ftrans_simp] - unfold Distribution.postExtAction - rw[postComp_restrict_extAction (x:=dirac t') (A:= Ioo 0 1) (Ο†:=fun _ => 1)] - simp [ftrans_simp, postComp_restrict_extAction] + fun_trans only [scalarGradient, scalarCDeriv, Tactic.if_pull, ftrans_simp] simp (disch:=sorry) only [action_push, ftrans_simp] rand_pull_E - simp #eval Rand.print_mean_variance (foo1' 0.3) 100 " of foo1'" @@ -150,18 +143,16 @@ 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 -set_option trace.Meta.Tactic.fun_prop true in + +-- set_option profiler true in +-- set_option trace.Meta.Tactic.fun_trans true in +-- set_option trace.Meta.Tactic.fun_prop true in def foo4 (t' : R) := derive_random_approx (βˆ‚ (t:=t'), ∫' (x : R) in Ioo 0 1, ∫' (y : R) in Ioo 0 1, if x ≀ t then x*y*t else x+y+t) by - fun_trans only [scalarGradient, scalarCDeriv] - simp only [Tactic.if_pull] - fun_trans only [scalarGradient, scalarCDeriv,ftrans_simp] + fun_trans only [scalarGradient, scalarCDeriv, Tactic.if_pull, ftrans_simp] simp (disch:=sorry) only [action_push, ftrans_simp] rand_pull_E simp diff --git a/SciLean/Core/Distribution/SurfaceDirac.lean b/SciLean/Core/Distribution/SurfaceDirac.lean index af3cceba..18cde50a 100644 --- a/SciLean/Core/Distribution/SurfaceDirac.lean +++ b/SciLean/Core/Distribution/SurfaceDirac.lean @@ -11,9 +11,12 @@ namespace SciLean variable {R} [RealScalar R] - {W} [Vec R W] + {W} [Vec R W] [Module ℝ W] {X} [SemiHilbert R X] [MeasureSpace X] {Y} [Vec R Y] [Module ℝ Y] + {Z} [Vec R Z] [Module ℝ Z] + {U} [Vec R U] + {V} [Vec R V] set_default_scalar R @@ -21,21 +24,21 @@ set_default_scalar R open Classical noncomputable def surfaceDirac (A : Set X) (f : X β†’ Y) (d : β„•) : π’Ÿ'(X,Y) := - ⟨fun Ο† ⊸ ∫' x in A, Ο† x β€’ f x βˆ‚(surfaceMeasure d)⟩ + fun Ο† ⊸ ∫' x in A, Ο† x β€’ f x βˆ‚(surfaceMeasure d) @[action_push] theorem surfaceDirac_action (A : Set X) (f : X β†’ Y) (d : β„•) (Ο† : π’Ÿ X) : - (surfaceDirac A f d).action Ο† = ∫' x in A, Ο† x β€’ f x βˆ‚(surfaceMeasure d) := sorry_proof + (surfaceDirac A f d) Ο† = ∫' x in A, Ο† x β€’ f x βˆ‚(surfaceMeasure d) := sorry_proof @[action_push] -theorem surfaceDirac_extAction (A : Set X) (f : X β†’ Y) (d : β„•) (Ο† : X β†’ R) : - (surfaceDirac A f d).extAction Ο† = ∫' x in A, Ο† x β€’ f x βˆ‚(surfaceMeasure d) := sorry_proof +theorem surfaceDirac_extAction (A : Set X) (f : X β†’ Y) (d : β„•) (Ο† : X β†’ V) (L : Y ⊸ V ⊸ W) : + (surfaceDirac A f d).extAction Ο† L = ∫' x in A, L (f x) (Ο† x) βˆ‚(surfaceMeasure d) := sorry_proof @[simp, ftrans_simp] -theorem surfaceDirac_dirac (f : X β†’ Y) (x : X) : surfaceDirac {x} f 0 = (dirac x).postComp (fun r => r β€’ (f x)) := by +theorem surfaceDirac_dirac (f : X β†’ Y) (x : X) : surfaceDirac {x} f 0 = (dirac x).postComp (fun r ⊸ r β€’ (f x)) := by ext Ο† unfold surfaceDirac; dsimp sorry_proof @@ -50,9 +53,9 @@ theorem ite_parDistribDeriv (A : W β†’ Set X) (f g : W β†’ X β†’ Y) : surfaceDirac (frontier (A w)) (fun x => (frontierSpeed R A w dw x) β€’ (f w x - g w x)) (finrank R X - 1) + ifD (A w) then - (parDistribDeriv (fun w => (f w Β·).toDistribution) w dw) + (parDistribDeriv (fun w => (f w Β·).toDistribution (R:=R)) w dw) else - (parDistribDeriv (fun w => (g w Β·).toDistribution) w dw) := sorry_proof + (parDistribDeriv (fun w => (g w Β·).toDistribution (R:=R)) w dw) := sorry_proof open Function in @@ -65,9 +68,9 @@ theorem ite_parDistribDeriv' (Ο† ψ : W β†’ X β†’ R) (f g : W β†’ X β†’ Y) : (surfaceDirac {x | Ο† w x = ψ w x} (fun x => frontierSpeed x β€’ (f w x - g w x)) (finrank R X - 1)) + ifD {x | Ο† w x ≀ ψ w x} then - (parDistribDeriv (fun w => (f w Β·).toDistribution) w dw) + (parDistribDeriv (fun w => (f w Β·).toDistribution (R:=R)) w dw) else - (parDistribDeriv (fun w => (g w Β·).toDistribution) w dw) := sorry_proof + (parDistribDeriv (fun w => (g w Β·).toDistribution (R:=R)) w dw) := sorry_proof open Function in @@ -76,7 +79,7 @@ theorem toDistribution.arg_f.parDistribDeriv_rule (f : W β†’ X β†’ Y) (hf : βˆ€ parDistribDeriv (fun w => Function.toDistribution (fun x => f w x)) = fun w dw => - (Function.toDistribution (fun x => cderiv R (f Β· x) w dw)) := by + (Function.toDistribution (fun x => cderiv R (f Β· x) w dw) (R:=R)) := by unfold parDistribDeriv funext x dx; ext Ο† @@ -109,10 +112,11 @@ theorem surfaceDirac_substitution [Fintype I] (Ο† ψ : X β†’ R) (f : X β†’ Y) (d (inv : ParametricInverseAt (fun x => Ο† x - ψ x) 0 p ΞΆ dom) (hdim : βˆ€ i, d = finrank (X₁ i)) : surfaceDirac {x | Ο† x = ψ x} f d = - βˆ‘ i, Distribution.prod' + βˆ‘ i, Distribution.prod (fun x₁ xβ‚‚ => p i x₁ xβ‚‚) (((fun x₁ => jacobian R (fun x => p i x (ΞΆ i x)) x₁ β€’ f (p i x₁ (ΞΆ i x₁))).toDistribution).restrict (dom i)) - (fun x₁ => (dirac (ΞΆ i x₁) : π’Ÿ' (Xβ‚‚ i))) := sorry + (fun x₁ => (dirac (ΞΆ i x₁) : π’Ÿ' (Xβ‚‚ i))) + (fun y ⊸ fun r ⊸ r β€’ y) := sorry_proof #exit diff --git a/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean b/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean index 5324cf0a..e1ef57a0 100644 --- a/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean +++ b/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean @@ -109,3 +109,43 @@ end AlgebraSimps instance : UniformSpace (X ⊸[K] Y) := sorry instance : Vec K (X ⊸[K] Y) := Vec.mkSorryProofs + +open BigOperators in +@[simp, ftrans_simp] +theorem SmoothLinearMap.fintype_sum_apply {I} [Fintype I] (f : I β†’ X⊸[K] Y) (x : X) : + (βˆ‘ i, f i) x = βˆ‘ i, f i x := by sorry_proof + +@[simp, ftrans_simp] +theorem SmoothLinearMap.indextype_sum_apply {I} [IndexType I] (f : I β†’ X⊸[K] Y) (x : X) : + (βˆ‘ i, f i) x = βˆ‘ i, f i x := by sorry_proof + + + +---------------------------------------------------------------------------------------------------- + + +@[fun_prop] +theorem SmoothLinearMap.mk'.arg_f.IsSmoothLinearMap_rule + (f : W β†’ X β†’ Y) + (hf : CDifferentiable K (fun (w,x) => f w x)) + (hf₁ : βˆ€ x, IsSmoothLinearMap K (f Β· x)) (hfβ‚‚ : βˆ€ w, IsSmoothLinearMap K (f w Β·)) : + IsSmoothLinearMap K (fun w => (fun x ⊸[K] f w x)) := sorry_proof + +@[fun_prop] +theorem SmoothLinearMap_apply_left + (f : W β†’ X ⊸[K] Y) (x : X) (hf : IsSmoothLinearMap K f) : + IsSmoothLinearMap K fun w => (f w) x := sorry_proof + +@[fun_prop] +theorem SmoothLinearMap.mk'.arg_f.CDifferentiable_rule + (f : W β†’ X ⊸[K] Y) (g : W β†’ X) (hf : CDifferentiable K f) (hg : CDifferentiable K g) : + CDifferentiable K (fun w => f w (g w)) := sorry_proof + + + +set_default_scalar K + +variable (f : X ⊸ Y) + +-- TODO: fix this!!! What is going on?? +#check f -- f : sorryAx (Type (max ?u.29009 ?u.28996)) true