fix up parametric discontinuities tests

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

Hide file tree

Showing 5 changed files with 59 additions and 2 deletions.
diff --git a/SciLean/Core/FunctionTransformations/Preimage.lean b/SciLean/Core/FunctionTransformations/Preimage.lean
@@ -38,8 +38,9 @@ theorem Prod.mk.arg_fstsnd.preimage_rule_prod (f : α → β) (g : α → γ) (B
     =
     f ⁻¹' B ∩ g ⁻¹' C := sorry_proof
 
-
+@[pp_dot]
 def _root_.Set.fst (A : Set (α×β)) (b : β) : Set α := {x | (x,b) ∈ A}
+@[pp_dot]
 def _root_.Set.snd (A : Set (α×β)) (a : α) : Set β := {y | (a,y) ∈ A}
 
 @[fun_trans]

diff --git a/test/prob_ad/affine_discont_1d.lean b/test/prob_ad/affine_discont_1d.lean
@@ -14,10 +14,25 @@ example (w : R) (a b c : R) (ha : a ≠ 0) :
       ∫' x in Icc (0:R) 1,
         if a * x + b ≤ c * w' then (1:R) else 0)
     =
-    if 0 ≤ w ∧ w ≤ 1 then 1 else 0 := by
+    sorry := by
 
   conv =>
     lhs
     integral_deriv
 
   sorry_proof
+
+
+
+
+variable (w : R) (a b c : R) (ha : a ≠ 0)
+
+
+/--
+info: let ds := ∫' x, (Scalar.abs a)⁻¹ * c ∂(surfaceMeasure 0).restrict ({x | a * x + b - c * w = 0} ∩ Icc 0 1);
+ds : R
+-/
+#guard_msgs in
+#check (∂ w':=w,
+      ∫' x in Icc (0:R) 1,
+        if a * x + b ≤ c * w' then (1:R) else 0) rewrite_by integral_deriv
diff --git a/test/prob_ad/affine_discont_2d.lean b/test/prob_ad/affine_discont_2d.lean
@@ -22,3 +22,25 @@ example (w : R) (a b c d : R) :
     autodiff
 
   sorry_proof
+
+
+
+variable (w : R) (a b c d : R)
+
+
+
+
+/--
+info: let ds :=
+  ∫' x,
+    jacobian R (fun x => (planeDecomposition (a, b) ⋯) ((d * w - c) / Scalar.sqrt (a ^ 2 + b ^ 2), x)) x *
+      ((Scalar.sqrt (a ^ 2 + b ^ 2))⁻¹ *
+        d) ∂volume.restrict
+      (((fun x12 => (planeDecomposition (a, b) ⋯) x12) ⁻¹' Icc 0 1 ×ˢ Icc 0 1).snd
+        ((d * w - c) / Scalar.sqrt (a ^ 2 + b ^ 2)));
+ds : R
+-/
+#guard_msgs in
+#check (∂ w':=w,
+      ∫' x in Icc (0:R) 1, ∫' y in Icc (0:R) 1,
+        if a * x + b * y + c ≤ d * w' then (1:R) else 0) rewrite_by integral_deriv; autodiff
diff --git a/test/prob_ad/neste_discont_1d.lean → test/prob_ad/nested_discont_1d.lean b/test/prob_ad/neste_discont_1d.lean → test/prob_ad/nested_discont_1d.lean
diff --git a/test/prob_ad/simple_discont_2d.lean b/test/prob_ad/simple_discont_2d.lean
@@ -22,3 +22,22 @@ example (w : R) :
     autodiff
 
   sorry_proof
+
+
+
+variable (w : R)
+
+/--
+info: let ds :=
+  ∫' x,
+    jacobian R (fun x => (planeDecomposition (1, 1) ⋯) (w / Scalar.sqrt (1 + 1), x)) x *
+      (Scalar.sqrt
+          (1 +
+            1))⁻¹ ∂volume.restrict
+      (preimageSnd ((fun x12 => (planeDecomposition (1, 1) ⋯) x12) ⁻¹' Icc 0 1 ×ˢ Icc 0 1) (w / Scalar.sqrt (1 + 1)));
+ds : R
+-/
+#guard_msgs in
+#check (∂ w':=w,
+      ∫' x in Icc (0:R) 1, ∫' y in Icc (0:R) 1,
+        if x + y ≤ w' then (1:R) else 0) rewrite_by integral_deriv; autodiff