tactics to prove ContinuousLinearMap and Differentiable

SciLean/FTrans/FDeriv/Basic.lean

@@ -5,11 +5,13 @@ import Mathlib.Analysis.Calculus.FDeriv.Comp
 import Mathlib.Analysis.Calculus.FDeriv.Prod
 import Mathlib.Analysis.Calculus.FDeriv.Linear
 
+
 import SciLean.Tactic.LSimp.Elab
+import SciLean.FunctionSpaces.ContinuousLinearMap.Basic
 
 namespace SciLean
 
-open Filter Asymptotics ContinuousLinearMap Set Metric
+-- open Filter Asymptotics ContinuousLinearMap Set Metric
 
 
 -- Basic lambda calculus rules -------------------------------------------------
@@ -28,16 +30,6 @@ variable {ι : Type _} [Fintype ι]
 variable {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace K (E i)]
 
 
--- #check ContinuousLinearMap.mk
-
--- def _root_.ContinuousLinearMap.mk' (f : X → Y) (h₁ : IsLinearMap K f := by sorry) (h₂ : Continuous f := by continuity)
---   : X →L[K] Y := ⟨⟨⟨f, h₁.map_add⟩, h₁.map_smul⟩, by aesop⟩
-
--- #check ContinuousLinearMap.mk' (K := K) fun (x : X) => x
-
--- macro " fun " x:ident " →L[" R:term "] " b:term : term => `(ContinuousLinearMap.mk' (K:=$R) fun $x => $b)
-
-
 @[ftrans]
 theorem fderiv.id_rule 
   : (fderiv K fun x : X => x) = fun _ => ContinuousLinearMap.id K X -- fun _ => fun dx →L[K] dx 
@@ -59,11 +51,18 @@ theorem fderiv.let_rule_at
         let y := g x 
         f x y) x
     =
-    let y  := g x
-    let dg := fderiv K g x
-    let df := fderiv K (fun xy : X×Y => f xy.1 xy.2) (x,y)
-    df.comp ((id K X).prod dg)
-  := by sorry_proof
+    fun dx =>L[K] 
+      let y  := g x
+      let dg := fderiv K g x
+      let df := fderiv K (fun xy : X×Y => f xy.1 xy.2) (x,y)
+      df (dx, (dg dx)) := 
+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
 
 
 theorem fderiv.let_rule
@@ -73,37 +72,32 @@ theorem fderiv.let_rule
        let y := g x
        f x y)
     =
-    fun x =>
+    fun x => fun dx =>L[K]
       let y  := g x
       let dg := fderiv K g x
       let df := fderiv K (fun xy : X×Y => f xy.1 xy.2) (x,y)
-      df.comp ((id K X).prod dg)
-    -- fun x => fun dx →L[K]
-    --   let y  := g x
-    --   let dy := fderiv K g x dx
-    --   fderiv K (fun xy : X×Y => f xy.1 xy.2) (x,y) (dx,dy)
-  := by sorry_proof
+      df (dx, (dg dx)) := 
+by
+  funext x
+  apply fderiv.let_rule_at x _ (hg x) _ (hf (x,g x))
 
 
 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
     = 
-    ContinuousLinearMap.pi fun i => fderiv K (f i) x
-    -- fun x => fun dx →L[K] fun i =>
-    --   fderiv K (f i) x dx
+    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 => 
-      ContinuousLinearMap.pi fun i => fderiv K (f i) x
-    -- fun x => fun dx →L[K] fun i =>
-    --   fderiv K (f i) x dx
+    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)
 
 
@@ -178,7 +172,7 @@ def fderiv.ftransInfo : FTrans.Info where
       let proof ← mkAppM ``fderiv.let_rule #[g,hg,f,hf]
       let rhs := (← inferType proof).getArg! 2
 
-      let goal : MVarId := sorry
+      -- let goal : MVarId := sorry
 
 
       dbg_trace "g = {← ppExpr g}"
@@ -189,9 +183,7 @@ def fderiv.ftransInfo : FTrans.Info where
 
   applyLambdaLambdaRule e := return none
 
-  discharger := 
-    let a : MacroM Syntax := `(tactic| simp)
-    sorry
+  discharger := `(tactic| simp)
 
 #check MacroM
 -- do
@@ -217,17 +209,25 @@ def fderiv.ftransInfo : FTrans.Info where
 #eval show Lean.CoreM Unit from do
   FTrans.infoExt.insert ``fderiv fderiv.ftransInfo
 
+set_option trace.Meta.Tactic.ftrans.step true
+set_option trace.Meta.Tactic.simp.rewrite true
+set_option trace.Meta.Tactic.simp.discharge true
+
+
 example :
   (fderiv K λ x : X => x)
   =
-  fun _ => 1
+  fun _ => fun dx =>L[K] dx
 := 
   by ftrans only; rfl
 
+
+#exit 
+
 example (x : X) :
   (fderiv K λ _ : Y => x)
   =
-  fun _ => 0
+  fun _ => fun dx =>L[K] 0
 := 
   by ftrans only
 

SciLean/FunctionSpaces/ContinuousLinearMap/Basic.lean

@@ -0,0 +1,223 @@
+import Mathlib.Topology.Algebra.Module.Basic
+
+import SciLean.FunctionSpaces.ContinuousLinearMap.Init
+
+namespace SciLean
+
+
+variable (R : Type _) [Semiring R]
+    {X : Type _} [TopologicalSpace X] [AddCommMonoid X] [Module R X]
+    {Y : Type _} [TopologicalSpace Y] [AddCommMonoid Y] [Module R Y]
+
+
+structure IsContinuousLinearMap (f : X → Y) : Prop where
+  map_add' : ∀ x y, f (x + y) = f x + f y
+  map_smul' : ∀ (r : R) (x : X), f (r • x) = r • f x
+  cont : Continuous f := by continuity
+
+
+-- Attribute and Tactic --------------------------------------------------------
+--------------------------------------------------------------------------------
+
+
+-- attribute
+macro "is_continuous_linear_map" : attr =>
+  `(attr|aesop safe apply (rule_sets [$(Lean.mkIdent `IsContinuousLinearMap):ident]))
+
+-- tactic
+macro "is_continuous_linear_map" : tactic =>
+  `(tactic| aesop (options := { terminal := true }) (rule_sets [$(Lean.mkIdent `IsContinuousLinearMap):ident]))
+
+
+
+-- Lambda function notation ----------------------------------------------------
+--------------------------------------------------------------------------------
+
+
+def ContinuousLinearMap.mk'
+  (f : X → Y) (hf : IsContinuousLinearMap R f := by is_continuous_linear_map) 
+  : X →L[R] Y :=
+  ⟨⟨⟨f, hf.map_add'⟩, hf.map_smul'⟩, hf.cont⟩
+
+
+macro "fun " x:ident " =>L[" R:term "] " b:term : term =>
+  `(ContinuousLinearMap.mk' $R fun $x => $b)
+
+macro "fun " x:ident " : " X:term " =>L[" R:term "] " b:term : term =>
+  `(ContinuousLinearMap.mk' $R fun ($x : $X) => $b)
+
+macro "fun " "(" x:ident " : " X:term ")" " =>L[" R:term "] " b:term : term =>
+  `(ContinuousLinearMap.mk' $R fun ($x : $X) => $b)
+
+@[app_unexpander ContinuousLinearMap.mk'] def unexpandContinuousLinearMapMk : Lean.PrettyPrinter.Unexpander
+
+  | `($(_) $R $f:term) =>
+    match f with
+    | `(fun $x':ident => $b:term) => `(fun $x' =>L[$R] $b)
+    | `(fun ($x':ident : $ty) => $b:term) => `(fun ($x' : $ty) =>L[$R] $b)
+    | `(fun $x':ident : $ty => $b:term) => `(fun $x' : $ty =>L[$R] $b)
+    | _  => throw ()
+  | _  => throw ()
+
+
+@[simp]
+theorem ContinuousLinearMap.mk'_eval
+  (x : X) (f : X → Y) (hf : IsContinuousLinearMap R f) 
+  : ContinuousLinearMap.mk' R (fun x => f x) hf x = f x := by rfl
+
+
+-- Basic rules -----------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+namespace IsContinuousLinearMap
+
+variable 
+  {R : Type _} [Semiring R]
+  {X : Type _} [TopologicalSpace X] [AddCommMonoid X] [Module R X]
+  {Y : Type _} [TopologicalSpace Y] [AddCommMonoid Y] [Module R Y]
+  {Z : Type _} [TopologicalSpace Z] [AddCommMonoid Z] [Module R Z]
+  {ι : Type _} [Fintype ι]
+  {E : ι → Type _} [∀ i, TopologicalSpace (E i)] [∀ i, AddCommMonoid (E i)] [∀ i, Module R (E i)]
+
+
+theorem by_morphism {f : X → Y} (g : X →L[R] Y) (h : ∀ x, f x = g x) 
+  : IsContinuousLinearMap R f :=
+by
+  have h' : f = g := by funext x; apply h
+  rw[h']
+  constructor
+  apply g.1.1.2
+  apply g.1.2
+  apply g.2
+
+
+@[is_continuous_linear_map]
+theorem id_rule 
+  : IsContinuousLinearMap R fun x : X => x 
+:= 
+  by_morphism (ContinuousLinearMap.id R X) (by simp)
+
+
+@[is_continuous_linear_map]
+theorem zero_rule 
+  : IsContinuousLinearMap R fun _ : X => (0 : Y) 
+:= 
+  by_morphism 0 (by simp)
+
+
+@[aesop unsafe apply (rule_sets [IsContinuousLinearMap])]
+theorem comp_rule 
+  (g : X → Y) (hg : IsContinuousLinearMap R g)
+  (f : Y → Z) (hf : IsContinuousLinearMap R f)
+  : IsContinuousLinearMap R fun x => f (g x) 
+:= 
+  by_morphism ((fun y =>L[R] f y).comp (fun x =>L[R] g x)) 
+  (by simp[ContinuousLinearMap.comp])
+
+
+@[aesop unsafe apply (rule_sets [IsContinuousLinearMap])]
+theorem scomb_rule 
+  (g : X → Y) (hg : IsContinuousLinearMap R g)
+  (f : X → Y → Z) (hf : IsContinuousLinearMap R (fun (xy : X×Y) => f xy.1 xy.2))
+  : IsContinuousLinearMap R fun x => f x (g x) 
+:= 
+  by_morphism ((fun (xy : X×Y) =>L[R] f xy.1 xy.2).comp ((ContinuousLinearMap.id R X).prod (fun x =>L[R] g x))) 
+  (by simp[ContinuousLinearMap.comp])
+
+
+@[is_continuous_linear_map]
+theorem pi_rule
+  (f : (i : ι) → X → E i) (hf : ∀ i, IsContinuousLinearMap R (f i))
+  : IsContinuousLinearMap R (fun x i => f i x) 
+:=
+  by_morphism (ContinuousLinearMap.pi fun i => fun x =>L[R] f i x)
+  (by simp)
+
+
+@[is_continuous_linear_map]
+theorem morph_rule (f : X →L[R] Y) : IsContinuousLinearMap R fun x => f x := 
+  by_morphism f (by simp)
+
+
+-- Id --------------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[is_continuous_linear_map]
+theorem _root_.id.arg_a.IsContinuousLinearMap
+  : IsContinuousLinearMap R (id : X → X)
+:= 
+  by_morphism (ContinuousLinearMap.id R X) (by simp)
+
+
+-- Prod ------------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[is_continuous_linear_map]
+theorem _root_.Prod.mk.arg_fstsnd.IsContinuousLinearMap_comp
+  (g : X → Y) (hg : IsContinuousLinearMap R g)
+  (f : X → Z) (hf : IsContinuousLinearMap R f)
+  : IsContinuousLinearMap R fun x => (g x, f x)
+:= 
+  by_morphism ((fun x =>L[R] g x).prod (fun x =>L[R] f x)) 
+  (by simp)
+
+
+@[is_continuous_linear_map]
+theorem _root_.Prod.fst.arg_self.IsContinuousLinearMap
+  : IsContinuousLinearMap R (@Prod.fst X Y)
+:=
+  by_morphism (ContinuousLinearMap.fst R X Y) 
+  (by simp)
+
+
+@[is_continuous_linear_map]
+theorem _root_.Prod.fst.arg_self.IsContinuousLinearMap_comp
+  (f : X → Y×Z) (hf : SciLean.IsContinuousLinearMap R f)
+  : SciLean.IsContinuousLinearMap R fun (x : X) => (f x).fst
+:= 
+  by_morphism ((ContinuousLinearMap.fst R Y Z).comp (fun x =>L[R] f x))
+  (by simp)
+
+
+@[is_continuous_linear_map]
+theorem _root_.Prod.snd.arg_self.IsContinuousLinearMap
+  : IsContinuousLinearMap R fun (xy : X×Y) => xy.snd
+:=
+  by_morphism (ContinuousLinearMap.snd R X Y) 
+  (by simp)
+
+
+@[is_continuous_linear_map]
+theorem _root_.Prod.snd.arg_self.IsContinuousLinearMap_comp
+  (f : X → Y×Z) (hf : SciLean.IsContinuousLinearMap R f)
+  : SciLean.IsContinuousLinearMap R fun (x : X) => (f x).snd
+:= 
+  by_morphism ((ContinuousLinearMap.snd R Y Z).comp (fun x =>L[R] f x))
+  (by simp)
+
+
+section Tests
+
+variable (f : X → X) (hf : IsContinuousLinearMap R f) (g : X → X) (hg : IsContinuousLinearMap R g) (x : X) (h : X →L[R] X)
+
+#check fun x =>L[R] h x
+
+#check fun x =>L[R] (x : X)
+
+#check (fun x =>L[R] f x) x
+
+#check fun x =>L[R] f (f x)
+
+#check fun x =>L[R] (f x, x)
+
+variable (g : X → Y×Z)  (hg : Continuous g) (f : Y×Z → X) (hf : Continuous f)
+
+theorem hihi : Continuous (fun xy : X×Y => xy.1) := by continuity
+
+theorem huhu : Continuous (fun x => f (g x)) := by continuity
+
+theorem hehe : IsContinuousLinearMap R (@Prod.fst X Y) := by is_continuous_linear_map
+
+theorem hoho : Continuous (fun x : X => (g x).1) := by continuity
+
+

SciLean/FunctionSpaces/ContinuousLinearMap/Init.lean

@@ -0,0 +1,3 @@
+import Aesop
+
+declare_aesop_rule_sets [IsContinuousLinearMap]