fix formating and proof of revFDeriv rule for smul

lecopivo · Jun 24, 2024 · 31a5972 · 31a5972
1 parent d20a4d6
commit 31a5972
Show file tree

Hide file tree

Showing 3 changed files with 63 additions and 49 deletions.
diff --git a/SciLean/Core/FunctionTransformations/RevFDeriv.lean b/SciLean/Core/FunctionTransformations/RevFDeriv.lean
@@ -178,14 +178,14 @@ variable
   {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, AdjointSpace K (E i)] [∀ i, CompleteSpace (E i)]
 
 
--- Prod.mk -----------------------------------v---------------------------------
+-- Prod.mk ----------------------------------- ---------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_trans]
 theorem SciLean.Prod.mk.arg_fstsnd.revFDeriv_rule_at
-  (g : X → Y) (f : X → Z) (x : X)
-  (hg : DifferentiableAt K g x) (hf : DifferentiableAt K f x)
-  : revFDeriv K (fun x => Prod.mk (g x) (f x)) x
+    (g : X → Y) (f : X → Z) (x : X)
+    (hg : DifferentiableAt K g x) (hf : DifferentiableAt K f x) :
+    revFDeriv K (fun x => Prod.mk (g x) (f x)) x
     =
     let ydg := revFDeriv K g x
     let zdf := revFDeriv K f x
@@ -214,8 +214,8 @@ theorem SciLean.Prod.mk.arg_fstsnd.revFDeriv_rule
 
 @[fun_trans]
 theorem SciLean.Prod.fst.arg_self.revFDeriv_rule_at
-  (f : X → Y×Z) (x : X) (hf : DifferentiableAt K f x)
-  : revFDeriv K (fun x => (f x).1) x
+    (f : X → Y×Z) (x : X) (hf : DifferentiableAt K f x) :
+    revFDeriv K (fun x => (f x).1) x
     =
     let yzdf := revFDeriv K f x
     (Prod.fst yzdf.1, fun dy => yzdf.2 (dy,0)) := by
@@ -225,8 +225,8 @@ theorem SciLean.Prod.fst.arg_self.revFDeriv_rule_at
 
 @[fun_trans]
 theorem SciLean.Prod.fst.arg_self.revFDeriv_rule
-  (f : X → Y×Z) (hf : Differentiable K f)
-  : revFDeriv K (fun x => (f x).1)
+    (f : X → Y×Z) (hf : Differentiable K f) :
+    revFDeriv K (fun x => (f x).1)
     =
     fun x =>
       let yzdf := revFDeriv K f x
@@ -240,8 +240,8 @@ theorem SciLean.Prod.fst.arg_self.revFDeriv_rule
 
 @[fun_trans]
 theorem SciLean.Prod.snd.arg_self.revFDeriv_rule_at
-  (f : X → Y×Z) (x : X) (hf : DifferentiableAt K f x)
-  : revFDeriv K (fun x => Prod.snd (f x)) x
+    (f : X → Y×Z) (x : X) (hf : DifferentiableAt K f x) :
+    revFDeriv K (fun x => Prod.snd (f x)) x
     =
     let yzdf := revFDeriv K f x
     (Prod.snd yzdf.1, fun dz => yzdf.2 (0,dz)) := by
@@ -251,8 +251,8 @@ theorem SciLean.Prod.snd.arg_self.revFDeriv_rule_at
 
 @[fun_trans]
 theorem SciLean.Prod.snd.arg_self.revFDeriv_rule
-  (f : X → Y×Z) (hf : Differentiable K f)
-  : revFDeriv K (fun x => Prod.snd (f x))
+    (f : X → Y×Z) (hf : Differentiable K f) :
+    revFDeriv K (fun x => Prod.snd (f x))
     =
     fun x =>
       let yzdf := revFDeriv K f x
@@ -324,12 +324,13 @@ theorem HSub.hSub.arg_a0a1.revFDeriv_rule
 
 @[fun_trans]
 theorem Neg.neg.arg_a0.revFDeriv_rule
-  (f : X → Y) (x : X)
-  : (revFDeriv K fun x => - f x) x
+    (f : X → Y) (x : X) :
+    (revFDeriv K fun x => - f x) x
     =
     let ydf := revFDeriv K f x
-    (-ydf.1, fun dy => - ydf.2 dy) :=
-by unfold revFDeriv; fun_trans
+    (-ydf.1, fun dy => - ydf.2 dy) := by
+
+  unfold revFDeriv; fun_trans
 
 
 -- HMul.hmul -------------------------------------------------------------------
@@ -339,9 +340,9 @@ open ComplexConjugate
 
 @[fun_trans]
 theorem HMul.hMul.arg_a0a1.revFDeriv_rule_at
-  (f g : X → K) (x : X)
-  (hf : DifferentiableAt K f x) (hg : DifferentiableAt K g x)
-  : (revFDeriv K fun x => f x * g x) x
+    (f g : X → K) (x : X)
+    (hf : DifferentiableAt K f x) (hg : DifferentiableAt K g x) :
+    (revFDeriv K fun x => f x * g x) x
     =
     let ydf := revFDeriv K f x
     let zdg := revFDeriv K g x
@@ -352,77 +353,80 @@ theorem HMul.hMul.arg_a0a1.revFDeriv_rule_at
 
 @[fun_trans]
 theorem HMul.hMul.arg_a0a1.revFDeriv_rule
-  (f g : X → K)
-  (hf : Differentiable K f) (hg : Differentiable K g)
-  : (revFDeriv K fun x => f x * g x)
+    (f g : X → K)
+    (hf : Differentiable K f) (hg : Differentiable K g) :
+    (revFDeriv K fun x => f x * g x)
     =
     fun x =>
       let ydf := revFDeriv K f x
       let zdg := revFDeriv K g x
-      (ydf.1 * zdg.1, fun dx' => (conj zdg.1) • ydf.2 dx' + (conj ydf.1) • zdg.2 dx') :=
-by funext; fun_trans
+      (ydf.1 * zdg.1, fun dx' => (conj zdg.1) • ydf.2 dx' + (conj ydf.1) • zdg.2 dx') := by
+
+  funext; fun_trans
 
 
 -- SMul.smul -------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_trans]
 theorem HSMul.hSMul.arg_a0a1.revFDeriv_rule_at
-  (f : X → K) (g : X → Y) (x : X)
-  (hf : DifferentiableAt K f x) (hg : DifferentiableAt K g x)
-  : (revFDeriv K fun x => f x • g x) x
+    (f : X → K) (g : X → Y) (x : X)
+    (hf : DifferentiableAt K f x) (hg : DifferentiableAt K g x) :
+    (revFDeriv K fun x => f x • g x) x
     =
     let ydf := revFDeriv K f x
     let zdg := revFDeriv K g x
-    (ydf.1 • zdg.1, fun dx' => ydf.2 (inner dx' zdg.1) + (conj ydf.1) • zdg.2 dx') := by
+    (ydf.1 • zdg.1, fun dx' => ydf.2 (inner zdg.1 dx') + (conj ydf.1) • zdg.2 dx') := by
   unfold revFDeriv
   fun_trans
   funext y; rw[add_comm]; congr
-  sorry_proof
+  rw[smul_adjoint (hA:=by fun_prop)]; simp
 
 
 @[fun_trans]
 theorem HSMul.hSMul.arg_a0a1.revFDeriv_rule
-  (f : X → K) (g : X → Y)
-  (hf : Differentiable K f) (hg : Differentiable K g)
-  : (revFDeriv K fun x => f x • g x)
+    (f : X → K) (g : X → Y)
+    (hf : Differentiable K f) (hg : Differentiable K g) :
+    (revFDeriv K fun x => f x • g x)
     =
     fun x =>
       let ydf := revFDeriv K f x
       let zdg := revFDeriv K g x
-      (ydf.1 • zdg.1, fun dx' => ydf.2 (inner dx' zdg.1) + (conj ydf.1) • zdg.2 dx') :=
-by funext; fun_trans
+      (ydf.1 • zdg.1, fun dx' => ydf.2 (inner zdg.1 dx') + (conj ydf.1) • zdg.2 dx') := by
+
+  funext; fun_trans
 
 
 -- HDiv.hDiv -------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_trans]
 theorem HDiv.hDiv.arg_a0a1.revFDeriv_rule_at
-  (f g : X → K) (x : X)
-  (hf : DifferentiableAt K f x) (hg : DifferentiableAt K g x) (hx : g x ≠ 0)
-  : (revFDeriv K fun x => f x / g x) x
+    (f g : X → K) (x : X)
+    (hf : DifferentiableAt K f x) (hg : DifferentiableAt K g x) (hx : g x ≠ 0) :
+    (revFDeriv K fun x => f x / g x) x
     =
     let ydf := revFDeriv K f x
     let zdg := revFDeriv K g x
     (ydf.1 / zdg.1,
-     fun dx' => ((conj zdg.1)^2)⁻¹ • (conj zdg.1 • ydf.2 dx' - conj ydf.1 • zdg.2 dx')) :=
-by
+     fun dx' => ((conj zdg.1)^2)⁻¹ • (conj zdg.1 • ydf.2 dx' - conj ydf.1 • zdg.2 dx')) := by
+
   unfold revFDeriv
   fun_trans (disch:=assumption)
 
 
 @[fun_trans]
 theorem HDiv.hDiv.arg_a0a1.revFDeriv_rule
-  (f g : X → K)
-  (hf : Differentiable K f) (hg : Differentiable K g) (hx : ∀ x, g x ≠ 0)
-  : (revFDeriv K fun x => f x / g x)
+    (f g : X → K)
+    (hf : Differentiable K f) (hg : Differentiable K g) (hx : ∀ x, g x ≠ 0) :
+    (revFDeriv K fun x => f x / g x)
     =
     fun x =>
       let ydf := revFDeriv K f x
       let zdg := revFDeriv K g x
       (ydf.1 / zdg.1,
        fun dx' => ((conj zdg.1)^2)⁻¹ • (conj zdg.1 • ydf.2 dx' - conj ydf.1 • zdg.2 dx')) := by
+
   funext
   fun_trans (disch:=apply hx)
 
@@ -443,10 +447,11 @@ by unfold revFDeriv; fun_trans
 
 @[fun_trans]
 def HPow.hPow.arg_a0.revFDeriv_rule
-  (f : X → K) (n : Nat) (hf : Differentiable K f)
-  : revFDeriv K (fun x => f x ^ n)
+    (f : X → K) (n : Nat) (hf : Differentiable K f) :
+    revFDeriv K (fun x => f x ^ n)
     =
     fun x =>
       let ydf := revFDeriv K f x
-      (ydf.1 ^ n, fun dx' => (n * (conj ydf.1 ^ (n-1))) • ydf.2 dx') :=
-by funext; fun_trans
+      (ydf.1 ^ n, fun dx' => (n * (conj ydf.1 ^ (n-1))) • ydf.2 dx') := by
+
+  funext; fun_trans
diff --git a/SciLean/Mathlib/Analysis/AdjointSpace/Adjoint.lean b/SciLean/Mathlib/Analysis/AdjointSpace/Adjoint.lean
@@ -47,7 +47,6 @@ theorem adjoint_ex (A : E → F) (hA : IsContinuousLinearMap 𝕜 A) :
 theorem adjoint_clm {A : E → F} (hA : IsContinuousLinearMap 𝕜 A) : IsContinuousLinearMap 𝕜 (A†) :=
     sorry_proof
 
-
 /-- The fundamental property of the adjoint. -/
 theorem adjoint_inner_left (A : E → F) (hA : IsContinuousLinearMap 𝕜 A) (x : E) (y : F) :
     ⟪(A†) y, x⟫ = ⟪y, A x⟫ := by
@@ -70,6 +69,14 @@ theorem adjoint_adjoint (A : E → F) (hA : IsContinuousLinearMap 𝕜 A) : A†
   rw[← adjoint_ex _ (adjoint_clm hA)]
   apply adjoint_inner_left _ hA
 
+theorem smul_adjoint (A : E → F) (hA : IsContinuousLinearMap 𝕜 A) (c : 𝕜) (y : F) :
+    c • adjoint 𝕜 A y = adjoint 𝕜 A (c • y) := by
+
+  apply AdjointSpace.ext_inner_right 𝕜; intro v
+  rw[AdjointSpace.inner_smul_left]
+  simp[adjoint_inner_left (hA:=hA)]
+  rw[AdjointSpace.inner_smul_left]
+
 
 /-- The adjoint of the composition of two operators is the composition of the two adjoints
 in reverse order. -/
@@ -132,7 +139,7 @@ theorem proj_rule [DecidableEq ι]
     fun x => (fun j => if h : i=j then h ▸ x else 0) := by
   rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
   intro x y
-  simp[Inner.inner]
+  rw[inner_forall_split]
   sorry_proof
 
 @[fun_trans]

diff --git a/SciLean/Mathlib/Analysis/AdjointSpace/Basic.lean b/SciLean/Mathlib/Analysis/AdjointSpace/Basic.lean
@@ -294,5 +294,7 @@ instance : AdjointSpace 𝕜 ((i : ι) → E i) where
   smul_left := by simp[inner_smul_left,Finset.mul_sum]
 
 
-
 theorem inner_prod_split (x y : X×Y) : ⟪x,y⟫_𝕜 = ⟪x.1,y.1⟫_𝕜 + ⟪x.2,y.2⟫_𝕜 := by rfl
+
+theorem inner_forall_split (f g : (i : ι) → E i) :
+    ⟪f,g⟫_𝕜 = ∑ i, ⟪f i, g i⟫_𝕜 := by rfl