fix distribution derivative

lecopivo · Mar 12, 2024 · cc84860 · cc84860
1 parent 799c8b2
commit cc84860
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/SciLean/Modules/Prob/DistribDeriv/DistribFwdDeriv.lean b/SciLean/Modules/Prob/DistribDeriv/DistribFwdDeriv.lean
@@ -1,3 +1,4 @@
+import SciLean.Core.FunctionTransformations
 import SciLean.Modules.Prob.DistribDeriv.DistribDeriv
 
 namespace SciLean.Prob

diff --git a/SciLean/Modules/Prob/DistribDeriv/Measure.lean b/SciLean/Modules/Prob/DistribDeriv/Measure.lean
@@ -45,8 +45,10 @@ theorem measure.distribDeriv_comp
     ⟪distribDeriv (fun y => (μ y).toDistribution) y dy, φ⟫ := by
 
   simp [distribDeriv]
-  rw [fderiv.comp_rule_at ℝ (fun y => ∫ (x : Z), φ x ∂(μ y)) f x hφ.diff hf]
-  dsimp
+  have h := fderiv.comp (𝕜:=ℝ) (x:=x) (g:=fun y => ∫ (x : Z), φ x ∂(μ y)) (f:=f) hφ.diff hf
+  -- rw[h] -- ugh
+  -- rw [fderiv.comp x (g:=fun y => ∫ (x : Z), φ x ∂(μ y)) (f:=f)f x hφ.diff hf]
+  sorry -- dsimp
 
 
 @[simp ↓]