nested discontinuity test

lecopivo · May 17, 2024 · 698064b · 698064b
1 parent cadca70
commit 698064b
Show file tree

Hide file tree

Showing 2 changed files with 23 additions and 0 deletions.
diff --git a/SciLean/Core/Integral/Common.lean b/SciLean/Core/Integral/Common.lean
@@ -19,6 +19,7 @@ attribute [ftrans_simp] MeasureTheory.Measure.restrict_empty MeasureTheory.Measu
 
 attribute [ftrans_simp] ENNReal.one_toReal ENNReal.zero_toReal
 
+attribute [ftrans_simp] Set.mem_inter_iff
 
 ----------------------------------------------------------------------------------------------------
 -- Measure simp theorems ---------------------------------------------------------------------------

diff --git a/test/prob_ad/neste_discont_1d.lean b/test/prob_ad/neste_discont_1d.lean
@@ -0,0 +1,22 @@
+import SciLean.Core.Integral.Common
+
+open SciLean MeasureTheory Set
+
+variable
+  {R : Type} [RealScalar R] [MeasureSpace R]
+
+set_default_scalar R
+
+example (w : R) :
+    (∂ w':=w,
+      ∫' x in Icc (0:R) 1,
+        if x ≤ w' then if x + w' ≤ 0 then (1:R) else 0 else 0)
+    =
+    let ds := if 0 ≤ w ∧ w ≤ 1 then if w + w ≤ 0 then 1 else 0 else 0;
+    let ds_1 := if (0 ≤ -w ∧ -w ≤ 1) ∧ -w ≤ w then -1 else 0;
+    let sf' := ds_1 + ds;
+    sf' := by
+
+  conv =>
+    lhs
+    integral_deriv