Skip to content

Commit

Permalink
clean up of adjoint file
Browse files Browse the repository at this point in the history
  • Loading branch information
lecopivo committed Jul 26, 2023
1 parent aac73e4 commit 90ab448
Showing 1 changed file with 0 additions and 99 deletions.
99 changes: 0 additions & 99 deletions SciLean/FTrans/Adjoint/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 -------------------------------------------------
--------------------------------------------------------------------------------
Expand Down Expand Up @@ -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)

0 comments on commit 90ab448

Please sign in to comment.