Merge branch 'master' of github.com:lecopivo/SciLean

SciLean/Core.lean

@@ -5,6 +5,7 @@ import SciLean.Core.Objects.IsReal
 
 import SciLean.Core.FunctionPropositions
 import SciLean.Core.FunctionTransformations
+import SciLean.Core.FunctionSpaces
 import SciLean.Core.Monads
 import SciLean.Core.Notation
 

SciLean/Core/FunctionPropositions/ContCDiff.lean

@@ -2,6 +2,7 @@ import SciLean.Core.Objects.Vec
 import SciLean.Core.Objects.SemiInnerProductSpace
 import SciLean.Core.Objects.FinVec
 import SciLean.Core.Objects.Scalar
+import SciLean.Core.FunctionPropositions.CDifferentiable
 
 import SciLean.Core.Meta.ToAnyPoint
 
@@ -36,7 +37,6 @@ def ContCDiffAt (f : X → Y) (x : X) : Prop :=
 @[fun_prop]
 def ContCDiff (f : X → Y) : Prop := ∀ x, ContCDiffAt K n f x
 
-variable (X)
 @[fun_prop, to_any_point]
 theorem ContCDiffAt.id_rule (x : X) :
     ContCDiffAt K n (fun x : X => x) x := by sorry_proof
@@ -62,9 +62,64 @@ theorem ContCDiffAt.pi_rule (x : X)
     ContCDiffAt K n (fun x i => f x i) x := by sorry_proof
 
 @[fun_prop, to_any_point]
-theorem ContCDiffAt.ContCDiff_rule (x : X) (f : X → Y) (hf : ContCDiffAt K m f x) (h : n ≤ m) :
+theorem ContCDiffAt.le_rule (x : X) (f : X → Y) (hf : ContCDiffAt K m f x) (h : n ≤ m) :
     ContCDiffAt K n f x := sorry_proof
 
+@[fun_prop, to_any_point]
+theorem ContCDiff.le_rule (f : X → Y) (hf : ContCDiff K m f) (h : n ≤ m) :
+    ContCDiff K n f := sorry_proof
+
+@[fun_prop]
+theorem ContCDiff.ContCDiffAt_rule (x : X) (f : X → Y) (hf : ContCDiff K n f) :
+    ContCDiffAt K n f x := hf x
+
+@[fun_prop]
+theorem ContCDiff.id_rule :
+    ContCDiff K n (fun x : X => x) := by intro x; fun_prop
+
+@[fun_prop]
+theorem ContCDiff.const_rule (y : Y) :
+    ContCDiff K n (fun _ : X => y) := by intro x; fun_prop
+
+@[fun_prop]
+theorem ContCDiff.comp_rule
+    (f : Y → Z) (g : X → Y)
+    (hf : ContCDiff K n f) (hg : ContCDiff K n g) :
+    ContCDiff K n (fun x => f (g x)) := by intro x; fun_prop
+
+@[fun_prop]
+theorem ContCDiff.apply_rule
+    (i : ι) : ContCDiff K n (fun x : (i : ι) → E i => x i) := by intro x; fun_prop
+
+@[fun_prop]
+theorem ContCDiff.pi_rule (x : X)
+    (f : X → (i : ι) → E i)
+    (hf : ∀ i, ContCDiff K n (f · i)) :
+    ContCDiff K n (fun x i => f x i) := by intro x; apply ContCDiffAt.pi_rule; fun_prop
+
+
+----------------------------------------------------------------------------------------------------
+
+
+-- transition rules to CDifferentiable
+
+@[fun_prop]
+theorem CDifferentaibleAt.ContCDiffAt_rule (x : X) (f : X → Y) (hf : ContCDiffAt K n f x) (h : 0 < n) :
+    CDifferentiableAt K f x := sorry_proof
+
+@[fun_prop]
+theorem CDifferentaibleAt.ContCDiffAt_rule' (x : X) (f : X → Y) (hf : ContCDiffAt K ∞ f x) :
+    CDifferentiableAt K f x := by fun_prop (disch:=aesop)
+
+@[fun_prop]
+theorem CDifferentaible.ContCDiff_rule (f : X → Y) (hf : ContCDiff K n f) (h : 0 < n) :
+    CDifferentiable K f := by intro x; fun_prop (disch:=assumption)
+
+@[fun_prop]
+theorem CDifferentaible.ContCDiff_rule' (f : X → Y) (hf : ContCDiff K ∞ f) :
+    CDifferentiable K f := by intro x; fun_prop
+
+
 section NormedSpaces
 
 variable
@@ -108,6 +163,14 @@ theorem Prod.mk.arg_fstsnd.ContCDiffAt_rule (x : X)
   := by sorry_proof
 
 
+@[fun_prop]
+theorem Prod.mk.arg_fstsnd.ContCDiff_rule
+  (g : X → Y) (hg : ContCDiff K n g)
+  (f : X → Z) (hf : ContCDiff K n f)
+  : ContCDiff K n (fun x => (g x, f x))
+  := by intro x; fun_prop
+
+
 -- Prod.fst --------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
@@ -117,6 +180,12 @@ theorem Prod.fst.arg_self.ContCDiffAt_rule (x : X)
     ContCDiffAt K n (fun x => (f x).1) x := by sorry_proof
 
 
+@[fun_prop]
+theorem Prod.fst.arg_self.ContCDiff_rule
+    (f : X → Y×Z) (hf : ContCDiff K n f) :
+    ContCDiff K n (fun x => (f x).1):= by intro x; fun_prop
+
+
 -- Prod.snd --------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
@@ -125,6 +194,11 @@ theorem Prod.snd.arg_self.ContCDiffAt_rule (x : X)
     (f : X → Y×Z) (hf : ContCDiffAt K n f x) :
     ContCDiffAt K n (fun x => (f x).2) x := by sorry_proof
 
+@[fun_prop]
+theorem Prod.snd.arg_self.ContCDiff_rule
+    (f : X → Y×Z) (hf : ContCDiff K n f) :
+    ContCDiff K n (fun x => (f x).2) := by sorry_proof
+
 
 -- Neg.neg ---------------------------------------------------------------------
 --------------------------------------------------------------------------------
@@ -134,6 +208,11 @@ theorem Neg.neg.arg_a0.ContCDiffAt_rule
     (x : X) (f : X → Y) (hf : ContCDiffAt K n f x) :
     ContCDiffAt K n (fun x => - f x) x := by sorry_proof
 
+@[fun_prop]
+theorem Neg.neg.arg_a0.ContCDiff_rule
+    (f : X → Y) (hf : ContCDiff K n f) :
+    ContCDiff K n (fun x => - f x) := by sorry_proof
+
 
 -- HAdd.hAdd -------------------------------------------------------------------
 --------------------------------------------------------------------------------
@@ -143,6 +222,11 @@ theorem HAdd.hAdd.arg_a0a1.ContCDiffAt_rule
     (x : X) (f g : X → Y) (hf : ContCDiffAt K n f x) (hg : ContCDiffAt K n g x) :
     ContCDiffAt K n (fun x => f x + g x) x := by sorry_proof
 
+@[fun_prop]
+theorem HAdd.hAdd.arg_a0a1.ContCDiff_rule
+    (f g : X → Y) (hf : ContCDiff K n f) (hg : ContCDiff K n g) :
+    ContCDiff K n (fun x => f x + g x) := by sorry_proof
+
 
 -- HSub.hSub -------------------------------------------------------------------
 --------------------------------------------------------------------------------
@@ -152,6 +236,11 @@ theorem HSub.hSub.arg_a0a1.ContCDiffAt_rule
     (x : X) (f g : X → Y) (hf : ContCDiffAt K n f x) (hg : ContCDiffAt K n g x) :
     ContCDiffAt K n (fun x => f x - g x) x := by sorry_proof
 
+@[fun_prop]
+theorem HSub.hSub.arg_a0a1.ContCDiff_rule
+    (f g : X → Y) (hf : ContCDiff K n f) (hg : ContCDiff K n g) :
+    ContCDiff K n (fun x => f x - g x) := by sorry_proof
+
 
 -- HMul.hMul -------------------------------------------------------------------
 --------------------------------------------------------------------------------
@@ -161,6 +250,11 @@ def HMul.hMul.arg_a0a1.ContCDiffAt_rule
     (x : X) (f g : X → K) (hf : ContCDiffAt K n f x) (hg : ContCDiffAt K n g x) :
     ContCDiffAt K n (fun x => f x * g x) x := by sorry_proof
 
+@[fun_prop]
+def HMul.hMul.arg_a0a1.ContCDiff_rule
+    (f g : X → K) (hf : ContCDiff K n f) (hg : ContCDiff K n g) :
+    ContCDiff K n (fun x => f x * g x) := by sorry_proof
+
 
 -- SMul.sMul -------------------------------------------------------------------
 --------------------------------------------------------------------------------
@@ -182,6 +276,23 @@ theorem HSMul.hSMul.arg_a1.ContCDiffAt_rule_int
     ContCDiffAt K n (fun x => c • f x) x := by sorry_proof
 
 
+@[fun_prop]
+def HSMul.hSMul.arg_a0a1.ContCDiff_rule
+  (f : X → K) (g : X → Y) (hf : ContCDiff K n f) (hg : ContCDiff K n g)
+  : ContCDiff K n (fun x => f x • g x)
+  := by intro x; fun_prop
+
+@[fun_prop]
+theorem HSMul.hSMul.arg_a1.ContCDiff_rule_n
+    (c : ℕ) (f : X → Y)  (hf : ContCDiff K n f) :
+    ContCDiff K n (fun x => c • f x) := by intro x; fun_prop
+
+@[fun_prop]
+theorem HSMul.hSMul.arg_a1.ContCDiff_rule_int
+    (c : ℤ) (f : X → Y) (hf : ContCDiff K n f) :
+    ContCDiff K n (fun x => c • f x) := by intro x; fun_prop
+
+
 -- HDiv.hDiv -------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
@@ -199,13 +310,32 @@ def HDiv.hDiv.arg_a0.ContCDiffAt_rule (x : X)
   fun_prop (disch:=intros; assumption)
 
 
+@[fun_prop]
+def HDiv.hDiv.arg_a0a1.ContCDiff_rule
+    (f : X → K) (g : X → K)
+    (hf : ContCDiff K n f) (hg : ContCDiff K n g) (hx : ∀ x, g x ≠ 0) :
+    ContCDiff K n (fun x => f x / g x) := by intro x; fun_prop (disch:=aesop)
+
+@[fun_prop,to_any_point]
+def HDiv.hDiv.arg_a0.ContCDiff_rule
+    (f : X → K) (r : K)
+    (hf : ContCDiff K n f) (hr : r ≠ 0) :
+    ContCDiff K n (fun x => f x / r) := by
+  fun_prop (disch:=intros; assumption)
+
+
 -- HPow.hPow -------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_prop,to_any_point]
 def HPow.hPow.arg_a0.ContCDiffAt_rule
-    (n : Nat) (x : X) (f : X → K) (hf : ContCDiffAt K n f x) :
-    ContCDiffAt K n (fun x => f x ^ n) x := by sorry_proof
+    (m : Nat) (x : X) (f : X → K) (hf : ContCDiffAt K n f x) :
+    ContCDiffAt K n (fun x => f x ^ m) x := by sorry_proof
+
+@[fun_prop]
+def HPow.hPow.arg_a0.ContCDiff_rule
+    (m : Nat)  (f : X → K) (hf : ContCDiff K n f) :
+    ContCDiff K n (fun x => f x ^ m) := by intro x; fun_prop
 
 
 -- IndexType.sum ----------------------------------------------------------------
@@ -217,6 +347,12 @@ theorem IndexType.sum.arg_f.ContCDiffAt_rule
   : ContCDiffAt K n (fun x => ∑ i, f x i) x := by sorry_proof
 
 
+@[fun_prop]
+theorem IndexType.sum.arg_f.ContCDiff_rule
+  (f : X → ι → Y) (hf : ∀ i, ContCDiff K n (fun x => f x i))
+  : ContCDiff K n (fun x => ∑ i, f x i) := by intro x; fun_prop
+
+
 --------------------------------------------------------------------------------
 
 section InnerProductSpace
@@ -237,19 +373,36 @@ theorem Inner.inner.arg_a0a1.ContCDiffAt_rule
     (hf : ContCDiffAt R n f x) (hg : ContCDiffAt R n g x) :
     ContCDiffAt R n (fun x => ⟪f x, g x⟫[R]) x := by sorry_proof
 
+@[fun_prop]
+theorem Inner.inner.arg_a0a1.ContCDiff_rule
+    (f : X → Y) (g : X → Y)
+    (hf : ContCDiff R n f) (hg : ContCDiff R n g) :
+    ContCDiff R n (fun x => ⟪f x, g x⟫[R]) := by intro x; fun_prop
+
 @[fun_prop,to_any_point]
 theorem SciLean.Norm2.norm2.arg_a0.ContCDiffAt_rule
   (f : X → Y) (x : X) (hf : ContCDiffAt R n f x)
   : ContCDiffAt R n (fun x => ‖f x‖₂²[R]) x := by
   simp[← SemiInnerProductSpace.inner_norm2]
   fun_prop
 
+@[fun_prop]
+theorem SciLean.Norm2.norm2.arg_a0.ContCDiff_rule
+  (f : X → Y) (hf : ContCDiff R n f)
+  : ContCDiff R n (fun x => ‖f x‖₂²[R]) := by intro x; fun_prop
+
 @[fun_prop,to_any_point]
 theorem SciLean.norm₂.arg_x.ContCDiffAt_rule
     (f : X → Y) (x : X)
     (hf : ContCDiffAt R n f x) (hx : f x≠0) :
     ContCDiffAt R n (fun x => ‖f x‖₂[R]) x := by sorry_proof
 
+@[fun_prop]
+theorem SciLean.norm₂.arg_x.ContCDiff_rule
+    (f : X → Y)
+    (hf : ContCDiff R n f) (hx : ∀ x, f x≠0) :
+    ContCDiff R n (fun x => ‖f x‖₂[R]) := by intro x; fun_prop (disch:=aesop)
+
 end InnerProductSpace
 
 namespace SciLean
@@ -277,5 +430,21 @@ theorem BasisDuality.toDual.arg_x.ContCDiffAt_rule (x)
 theorem BasisDuality.fromDual.arg_x.ContCDiffAt_rule (x)
   : ContCDiffAt K n (fun x : X => BasisDuality.fromDual x) x := by sorry_proof
 
+@[fun_prop]
+theorem Basis.proj.arg_x.ContCDiff_rule (i : IX)
+  : ContCDiff K n (fun x : X => ℼ i x) := by sorry_proof
+
+@[fun_prop]
+theorem DualBasis.dualProj.arg_x.ContCDiff_rule (i : IX)
+  : ContCDiff K n (fun x : X => ℼ' i x) := by sorry_proof
+
+@[fun_prop]
+theorem BasisDuality.toDual.arg_x.ContCDiff_rule
+  : ContCDiff K n (fun x : X => BasisDuality.toDual x) := by sorry_proof
+
+@[fun_prop]
+theorem BasisDuality.fromDual.arg_x.ContCDiff_rule
+  : ContCDiff K n (fun x : X => BasisDuality.fromDual x) := by sorry_proof
+
 end OnFinVec
 end SciLean