From 1c50e9d1aaafea09d4d5e3f24d838e4f30392982 Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Fri, 1 Nov 2024 15:42:51 +0100
Subject: [PATCH] remove two main sorries from fderiv

---
 SciLean/Analysis/Calculus/FDeriv.lean         | 24 +++++++++++++++----
 .../Normed/IsContinuousLinearMap.lean         |  2 +-
 2 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/SciLean/Analysis/Calculus/FDeriv.lean b/SciLean/Analysis/Calculus/FDeriv.lean
index cbdbd95f..c5b2caa0 100644
--- a/SciLean/Analysis/Calculus/FDeriv.lean
+++ b/SciLean/Analysis/Calculus/FDeriv.lean
@@ -20,7 +20,7 @@ variable
   {X : Type _} [NormedAddCommGroup X] [NormedSpace K X]
   {Y : Type _} [NormedAddCommGroup Y] [NormedSpace K Y]
   {Z : Type _} [NormedAddCommGroup Z] [NormedSpace K Z]
-  {ι : Type _} [IndexType ι]
+  {ι : Type _} [Fintype ι]
   {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace K (E i)]
 
 namespace SciLean
@@ -38,8 +38,7 @@ theorem fderiv.id_rule :
 theorem fderiv.const_rule (x : X) :
     (fderiv K fun _ : Y => x)
     =
-    -- fun _ => fun =>[K] 0 := by -- todo: fix fun_prop
-    fun _ => ContinuousLinearMap.mk' K (fun _ => 0) (IsContinuousLinearMap.const_rule) := by
+    fun x => fun dy =>L[K] 0 := by
   ext x dx; simp
 
 @[fun_trans]
@@ -47,7 +46,14 @@ theorem fderiv.apply_rule (i : ι) :
     (fderiv K fun (x : (i : ι) → E i) => x i)
     =
     fun _ => fun dx =>L[K] dx i := by
-  funext x; sorry_proof -- somehow use fderiv_pi
+  funext x; ext dx
+  let φ := fun (i : ι) (x : (j : ι) → E j) => x i
+  have h := (fderiv_pi (𝕜:=K) (φ := φ) (h:=by fun_prop) (x:=x))
+       |> (congrArg DFunLike.coe ·)
+       |> (congrFun · dx)
+       |> (congrFun · i)
+  simp [φ] at h
+  simp[h.symm]
 
 @[fun_trans]
 theorem fderiv.comp_rule_at
@@ -145,7 +151,15 @@ open SciLean
 
 @[fun_trans]
 theorem isContinuousLinearMap_fderiv (f : X → Y) (hf : IsContinuousLinearMap K f) :
-    fderiv K f = fun _ => fun dx =>L[K] f dx := sorry_proof
+    fderiv K f = fun _ => fun dx =>L[K] f dx := by
+  ext x dx
+  let hf : IsBoundedLinearMap K f := by
+    have h : f = (fun x =>L[K] f x) := by rfl
+    rw[h]
+    apply ContinuousLinearMap.isBoundedLinearMap
+  rw[IsBoundedLinearMap.fderiv (f:=f) hf]
+  rfl
+
 
 -- Prod.mk -----------------------------------v---------------------------------
 --------------------------------------------------------------------------------
diff --git a/SciLean/Analysis/Normed/IsContinuousLinearMap.lean b/SciLean/Analysis/Normed/IsContinuousLinearMap.lean
index b35c5f3c..ff126145 100644
--- a/SciLean/Analysis/Normed/IsContinuousLinearMap.lean
+++ b/SciLean/Analysis/Normed/IsContinuousLinearMap.lean
@@ -14,6 +14,7 @@ variable (R : Type _) [Semiring R]
     {Y : Type _} [TopologicalSpace Y] [AddCommMonoid Y] [Module R Y]
 
 
+-- TODO: completely remove this is is the same as IsBoundedLinearMap
 @[fun_prop]
 structure IsContinuousLinearMap (f : X → Y) : Prop where
   linear : IsLinearMap R f
@@ -465,7 +466,6 @@ variable
 --------------------------------------------------------------------------------
 -- Differentiable --------------------------------------------------------------
 
-
 @[fun_prop]
 theorem SciLean.IsContinuousLinearMap.differentiable (f : X → Y) (hf : IsContinuousLinearMap K f) :
     Differentiable K f := by