From 90ab4480ba31ea3501b7b531cb766c0d643485b5 Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Wed, 26 Jul 2023 18:41:13 -0400
Subject: [PATCH] clean up of adjoint file

---
 SciLean/FTrans/Adjoint/Basic.lean | 99 -------------------------------
 1 file changed, 99 deletions(-)

diff --git a/SciLean/FTrans/Adjoint/Basic.lean b/SciLean/FTrans/Adjoint/Basic.lean
index 1f4184af..161da127 100644
--- a/SciLean/FTrans/Adjoint/Basic.lean
+++ b/SciLean/FTrans/Adjoint/Basic.lean
@@ -27,8 +27,6 @@ instance {E : ι → Type _} [∀ i, UniformSpace (E i)] [∀ i, CompleteSpace (
 instance (f : X →L[K] Y) : SciLean.Dagger f (ContinuousLinearMap.adjoint f : Y →L[K] X) := ⟨⟩
 variable (g : X → Y) (hg : SciLean.IsContinuousLinearMap K g)
 
-example 
-  : SciLean.IsContinuousLinearMap K fun (xy : X×₂Y) => xy.1 + (fun x =>L[K] g x)† xy.2 := by fprop
 
 -- Basic lambda calculus rules -------------------------------------------------
 --------------------------------------------------------------------------------
@@ -117,100 +115,3 @@ theorem pi_rule
     (fun x' =>L[K] ∑ i, (fun x =>L[K] f i x)† (x' i))
   := sorry
 
-#exit
-
-
-noncomputable
-def a := (fun (x : X) =>L[K] x)† 
-
-#check (fun (x : X) =>L[K] x)†
-
-#check a†
-
-def ProdLp (r : ℝ) (α β : Type _) := α × β
-
-#check ((1,2) : ProdLp 2 Nat Nat)
-
-instance 
-  {K : Type _}
-  {X : Type _} [Inner K X]
-  {Y : Type _} [Inner K Y]
-  : Inner K (X × Y) := sorry
-
-
-instance
-  {K : Type _} [IsROrC K]
-  {X : Type _} [NormedAddCommGroup X] [InnerProductSpace K X]
-  {Y : Type _} [NormedAddCommGroup Y] [InnerProductSpace K Y]
-  : InnerProductSpace K (X × Y) where
-  norm_sq_eq_inner := sorry
-  conj_symm := sorry
-  add_left := sorry
-  smul_left := sorry
-
-noncomputable
-def b := ContinuousLinearMap.adjoint (fun xy : X×Y =>L[K] f xy.1 xy.2)
-
-
-noncomputable
-def c := ContinuousLinearMap.adjoint (ContinuousLinearMap.mk' K (fun xy : X×Y => f xy.1 xy.2) sorry)
-
-#check c
-
-example :
-   (@IsContinuousLinearMap K DivisionSemiring.toSemiring (Prod X Y) instTopologicalSpaceProd Prod.instAddCommMonoidSum
-       Prod.module Z UniformSpace.toTopologicalSpace AddCommGroup.toAddCommMonoid NormedSpace.toModule fun xy =>
-       f xy.fst xy.snd)
-    =
-    (@IsContinuousLinearMap K DivisionSemiring.toSemiring (Prod X Y) UniformSpace.toTopologicalSpace
-        AddCommGroup.toAddCommMonoid NormedSpace.toModule Z UniformSpace.toTopologicalSpace AddCommGroup.toAddCommMonoid
-        NormedSpace.toModule fun xy => f xy.fst xy.snd)
-   := by rfl
-
-def hoh : InnerProductSpace K (X×Y) := by infer_instance
-
-#print hoh
-
-
-#check instTopologicalSpaceProd
-#check instUniformSpaceProd
-#exit
-
-theorem adjoint.let_rule
-  (g : X → Y) (hg : IsContinuousLinearMap K g)
-  (f : X → Y → Z) (hf : IsContinuousLinearMap K (fun xy : X×Y => f xy.1 xy.2))
-  (z : Z)
-  : ((fun x : X =>
-        let y := g x
-        f x y)† z)
-    =
-      let f' := (fun xy : X×Y =>L[K] f xy.1 xy.2)†
-      let g' := (fun x =>L[K] g x)†
-      let xy := f' z
-      let x' := g' xy.2
-      x + x' :=  sorry
--- by 
---   have h : (fun x => f x (g x)) = (fun xy : X×Y => f xy.1 xy.2) ∘ (fun x => (x, g x)) := by rfl
---   rw[h]
---   rw[fderiv.comp x hf (DifferentiableAt.prod (by simp) hg)]
---   rw[DifferentiableAt.fderiv_prod (by simp) hg]
---   ext dx; simp[ContinuousLinearMap.comp]
---   rfl
-#exit
-theorem fderiv.pi_rule_at
-  (x : X)
-  (f : (i : ι) → X → E i) (hf : ∀ i, DifferentiableAt K (f i) x)
-  : (fderiv K fun (x : X) (i : ι) => f i x) x
-    = 
-    fun dx =>L[K] fun i =>
-      fderiv K (f i) x dx
-  := fderiv_pi hf
-
-
-theorem fderiv.pi_rule
-  (f : (i : ι) → X → E i) (hf : ∀ i, Differentiable K (f i))
-  : (fderiv K fun (x : X) (i : ι) => f i x)
-    = 
-    fun x => fun dx =>L[K] fun i =>
-      fderiv K (f i) x dx
-  := by funext x; apply fderiv_pi (fun i => hf i x)