cderiv rule for if with condition depending on x

lecopivo · Nov 27, 2023 · fe9321e · fe9321e
1 parent ce8dc90
commit fe9321e
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/SciLean/Core/FunctionTransformations/CDeriv.lean b/SciLean/Core/FunctionTransformations/CDeriv.lean
@@ -727,6 +727,18 @@ by
   case isFalse h => ext y; simp[h]
 
 
+-- not sure about the differentiability condition on `e`
+theorem ite.arg_chte.cderiv_rule
+  (c : X → Prop) [dec : ∀ x, Decidable (c x)] (t e : X → Y)
+  (ht : ∀ x ∈ closure c, IsDifferentiableAt K t x) (he : ∀ x ∈ (interior c)ᶜ, IsDifferentiableAt K e x)
+  (hc : (∀ x, x ∈ frontier c → cderiv K t x = cderiv K e x))
+  : cderiv K (fun x => ite (c x) (t x) (e x))
+    =
+    fun y =>
+      ite (c y) (cderiv K t y) (cderiv K e y) := 
+by
+  sorry_proof
+
 
 --------------------------------------------------------------------------------