...

SciLean/Core/Distribution/BungeeTest.lean

@@ -8,6 +8,9 @@ import SciLean.Core.Integral.ParametricInverse
 import SciLean.Core.Integral.Frontier
 import SciLean.Core
 
+import SciLean.Core.FunctionTransformations.Preimage
+import SciLean.Tactic.IfPull
+
 import SciLean.Util.RewriteBy
 
 open MeasureTheory
@@ -139,6 +142,7 @@ attribute [rand_pull_E] bind_assoc pure_bind
 theorem ite_apply {α β : Type _} {c : Prop} [Decidable c] (t e : α → β) (x : α) :
     (ite c t e) x = ite c (t x) (e x) := by if h : c then simp[h] else simp[h]
 
+
 -- theorem set_inter {α} (P Q : α → Prop) : {x | P x} ∩ {x | Q x} = {x | P x ∧ Q x} := by aesop
 
 -- open Lean Meta in
@@ -191,6 +195,10 @@ set_option trace.Meta.Tactic.fun_trans true in
     unfold timeToFall' bungeeTension
     fun_trans (config:={zeta:=false}) only [ftrans_simp, scalarGradient, Tactic.lift_lets_simproc]
 
+    enter[w,dw,1,1,1,1,w,1,x,1,2]
+    simp only
+    simp only [Tactic.if_pull]
+
     -- simp only [ftrans_simp, action_pus]
     -- rw [Distribution.mk_extAction (X:=R)]
     -- unfold scalarGradient

SciLean/Core/Distribution/Doodle.lean

@@ -33,26 +33,37 @@ attribute [ftrans_simp]
   preimage_id'
   mem_setOf_eq mem_ite_empty_right mem_inter_iff mem_ite_empty_right mem_univ mem_Ioo
   and_true
-
+  bind_pure bind_assoc pure_bind
 
 
 variable [Module ℝ Z] [MeasureSpace X] [Module ℝ Y]
 
 
-set_option profiler true in
-set_option trace.Meta.Tactic.fun_prop true in
-set_option trace.Meta.Tactic.fun_trans true in
-set_option trace.Meta.Tactic.simp.rewrite true in
+-- set_option profiler true in
+-- set_option trace.Meta.Tactic.fun_prop true in
+-- set_option trace.Meta.Tactic.fun_trans true in
+-- set_option trace.Meta.Tactic.simp.rewrite 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]
+    simp only [ftrans_simp]
     simp only [toDistrib_pull,restrict_pull]
     simp only [restrict_push]
     simp only [ftrans_simp,restrict_push]
     simp (disch:=sorry) only [action_push, ftrans_simp, restrict_push]
-    -- rand_pull_E
-    -- simp
+
+    conv =>
+      enter[2]
+      simp only [distrib_eval,ftrans_simp]
+      simp only [Tactic.if_pull]
+      simp (disch:=sorry) only [action_push, ftrans_simp, restrict_push]
+      simp only [distrib_eval,ftrans_simp]
+
+    simp only [distrib_eval,ftrans_simp]
+
+    rand_pull_E
+    simp (disch:=sorry) only [ftrans_simp]

SciLean/Core/Distribution/Eval.lean

@@ -19,17 +19,17 @@ set_default_scalar R
 
 open Classical
 
-@[action_push]
+@[distrib_eval]
 theorem action_extAction (T : 𝒟' X) (φ : 𝒟 X) :
     T φ = T.extAction' φ := sorry_proof
 
-@[action_push]
+@[simp,ftrans_simp]
 theorem extAction_vecDirac (x : X) (φ : X → Y)  (L : R ⊸ Y ⊸ Z) :
     (dirac x).extAction φ L
     =
     L 1 (φ x) := sorry_proof
 
-@[action_push]
+@[simp,ftrans_simp]
 theorem extAction_restrict_vecDirac (x : X) (A : Set X) (φ : X → Y) (L : R ⊸ Y ⊸ Z) :
     ((dirac x).restrict A).extAction φ L
     =
@@ -46,7 +46,7 @@ theorem postExtAction_postComp (x : 𝒟'(X,U)) (y : U ⊸ 𝒟'(Y,Z)) (φ : Y 
 variable [MeasureSpace X]
 
 open Rand in
-@[action_push]
+@[distrib_eval]
 theorem function_toDistribution_eval (f : X → Y) (A : Set X) (φ : X → U) (L : Y ⊸ U ⊸ V) [UniformRand A] :
   (f.toDistribution.restrict A).extAction φ L
   =
@@ -56,7 +56,7 @@ theorem function_toDistribution_eval (f : X → Y) (A : Set X) (φ : X → U) (L
 
 
 open Rand in
-@[action_push]
+@[distrib_eval]
 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
   =

SciLean/Core/Distribution/ParametricDistribDeriv.lean

@@ -172,15 +172,15 @@ theorem Bind.bind.arg_fx.DistribDifferentiable_rule
 
 @[fun_trans]
 theorem Bind.bind.arg_fx.parDistribDiff_rule
-    (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`
+    (f : W → X → 𝒟'(Y,V)) (g : W → 𝒟'(X,U)) (L : U ⊸ V ⊸ W)
+    (hf : DistribDifferentiable (fun (w,x) => f w x)) -- `f` has to be nice enough to accomodate action of `g`
     (hg : DistribDifferentiable g) :
-    parDistribDeriv (fun x => (g x).bind (f x) L)
+    parDistribDeriv (fun w => (g w).bind (f w) L)
     =
-    fun x dx =>
-      ((parDistribDeriv  g x dx).bind (f x · ) L)
+    fun w dw =>
+      ((parDistribDeriv g w dw).bind (f x · ) L)
       +
-      ((g x).bind (fun y => parDistribDeriv (f · y) x dx) L) := sorry_proof
+      ((g w).bind (fun x => parDistribDeriv (f · x) w dw) L) := sorry_proof
 
 
 

SciLean/Core/Distribution/ParametricDistribFwdDeriv.lean

@@ -82,8 +82,8 @@ theorem bind_rule
     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
+      let ydy := parDistribFwdDeriv g x dx  -- 𝒟'(Y,U×U)
+      let zdz := fun y => parDistribFwdDeriv (f · y) x dx -- Y → 𝒟'(Z,V×V)
       ydy.bind zdz (fun (r,dr) ⊸ fun (s,ds) ⊸ (L r s, L r ds + L dr s)) := by
 
   unfold parDistribFwdDeriv Distribution.bind

SciLean/Core/Distribution/SurfaceDirac.lean

@@ -27,6 +27,12 @@ def surfaceDirac (A : Set X) (f : X → Y) (d : ℕ) : 𝒟'(X,Y) :=
   fun φ ⊸ ∫' x in A, φ x • f x ∂(surfaceMeasure d)
 
 
+open Classical
+noncomputable
+def surfaceDirac' (A : Set X) (f : X → R) (u : 𝒟'(X,Y)) (d : ℕ) : 𝒟'(X,Y) := sorry
+  -- 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) φ = ∫' x in A, φ x • f x ∂(surfaceMeasure d) := sorry_proof

SciLean/Core/Rand/PushPullExpectation.lean

@@ -87,6 +87,22 @@ theorem pull_mean_add (x y : Rand X) :
       let y' ← y
       return x' + y' := sorry_proof
 
+@[rand_pull_E]
+theorem pull_mean_add_1 (x : Rand X) (y : X) :
+    x.mean + y
+    =
+    Rand.mean do
+      let x' ← x
+      return x' + y := sorry_proof
+
+@[rand_pull_E]
+theorem pull_mean_add_2 (x : X) (y : Rand X) :
+    x + y.mean
+    =
+    Rand.mean do
+      let y' ← y
+      return x + y' := sorry_proof
+
 @[rand_pull_E]
 theorem pull_mean_sub (x y : Rand X) :
     x.mean - y.mean
@@ -112,6 +128,15 @@ theorem pull_mean_mul (r : R) (x : Rand R) :
       let x' ← x
       return r * x' := sorry_proof
 
+@[rand_pull_E]
+theorem pull_mean_div (x : Rand R) (y : R) :
+    x.mean / y
+    =
+    Rand.mean do
+      let x' ← x
+      return x' / y:= sorry_proof
+
+
 @[rand_pull_E]
 theorem pull_mean_neg (x : Rand X) :
     - x.mean

SciLean/Doodle.lean

@@ -6,6 +6,12 @@ open SciLean
 set_default_scalar Float
 
 
+
+#check ∂>! x : Float, ((x*x)*x)
+
+#check HMul.hMul.arg_a0a1.
+
+
 #check ∂! x : Float, x*x
 
 def foo (x : Float) := ∂! (x':=x), x'*x'

SciLean/Modules/Prob/PushPullE.lean

@@ -50,3 +50,8 @@ theorem bind_pull_mean (x : Rand X) (f : X → Rand Y) :
     (x.bind (fun x' => pure (f x').mean)).mean
     =
     (x.bind f).mean := sorry
+
+
+@[rand_pull_E mid-1]
+theorem add_pull_mean (x : X) (f : Rand X) :
+    x + f.mean = Rand.mean (X:=X) (do let y ← f; pure (x + y)) := sorry_proof