play around with smooth maps

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
 
@@ -96,6 +97,29 @@ theorem ContCDiff.pi_rule (x : X)
     (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

SciLean/Core/FunctionSpaces/ContDiffMap.lean → SciLean/Core/FunctionSpaces/ContCDiffMap.lean

@@ -1,6 +1,8 @@
 import SciLean.Core.FunctionPropositions.ContCDiff
 import SciLean.Core.FunctionTransformations
 
+import SciLean.Core.Notation.CDeriv
+
 set_option linter.unusedVariables false
 
 namespace SciLean
@@ -17,7 +19,6 @@ variable
 local notation "∞" => (⊤ : ℕ∞)
 
 
-
 -- Function space --------------------------------------------------------------
 --------------------------------------------------------------------------------
 
@@ -31,9 +32,20 @@ instance : FunLike (ContCDiffMap K n X Y) X Y where
   coe f := f.toFun
   coe_injective' := sorry_proof
 
-macro X:term:25 " ⟿[" K:term "," n:term "]" Y:term:26 : term =>
+macro X:term:25 " ⟿[" K:term "," n:term "] " Y:term:26 : term =>
   `(ContCDiffMap $K $n $X $Y)
 
+macro X:term:25 " ⟿[" n:term "] " Y:term:26 : term =>
+  `(ContCDiffMap currentScalar% $n $X $Y)
+
+macro X:term:25 " ⟿ " Y:term:26 : term =>
+  `(ContCDiffMap currentScalar% ∞ $X $Y)
+
+@[app_unexpander ContCDiffMap] def unexpandContCDiffMap : Lean.PrettyPrinter.Unexpander
+  | `($(_) $R $n $X $Y) => `($X ⟿[$R,$n] $Y)
+  | _  => throw ()
+
+
 @[fun_prop]
 theorem ContCDiffMap_apply_right (f : X ⟿[K,n] Y) : ContCDiff K n (fun x => f x) := f.2
 
@@ -63,6 +75,14 @@ open Lean Parser Term
 macro "fun " x:funBinder " ⟿[" K:term "," n:term "] " b:term : term =>
   `(ContCDiffMap.mk' $K $n (fun $x => $b) (by fun_prop (disch:=norm_num; linarith)))
 
+open Lean Parser Term
+macro "fun " x:funBinder " ⟿[" n:term "] " b:term : term =>
+  `(ContCDiffMap.mk' currentScalar% $n (fun $x => $b) (by fun_prop (disch:=norm_num; linarith)))
+
+open Lean Parser Term
+macro "fun " x:funBinder " ⟿ " b:term : term =>
+  `(ContCDiffMap.mk' currentScalar% ∞ (fun $x => $b) (by fun_prop (disch:=norm_num; linarith)))
+
 @[app_unexpander ContCDiffMap.mk'] def unexpandContCDiffMapMk : Lean.PrettyPrinter.Unexpander
 
   | `($(_) $R $n $f:term $_:term) =>
@@ -91,6 +111,7 @@ section AlgebraSimps
 
 variable (f g : X ⟿[K,n] Y) (x : X) (r : K)
 
+
 @[simp, ftrans_simp]
 theorem ContCDiffMap.add_apply : (f + g) x = f x + g x := by rfl
 
@@ -104,14 +125,16 @@ theorem ContCDiffMap.neg_apply : (- f) x = - f x := by rfl
 theorem ContCDiffMap.smul_apply : (r • f) x = r • f x := by rfl
 
 @[simp, ftrans_simp]
-theorem ContCDiffMap.zero_apply : (0 : X⟿[K,n]Y) x = 0 := by sorry_proof
+theorem ContCDiffMap.zero_apply : (0 : X ⟿[K,n] Y) x = 0 := by sorry_proof
 
 end AlgebraSimps
 
 instance : TopologicalSpace (X ⟿[K,n] Y) := sorry
 instance : Vec K (X ⟿[K,n] Y) := Vec.mkSorryProofs
 
 
+-- set_option trace.Meta.Tactic.fun_prop.attr true
+
 
 -- The following two theorems are somehow related to catesian closedness of convenient vectors spaces
 @[fun_prop]
@@ -155,5 +178,19 @@ example : (cderiv K fun (w : K) => fun (x : K) ⟿[K,n] w*x + w)
           =
           fun w dw => fun (x : K) ⟿[K,n] dw*x + dw := by conv => lhs; fun_trans
 
--- set_option trace.Meta.Tactic.fun_prop true in
--- example : IsSmoothLinearMap K fun (f : X ⟿[K,n] Y) => fun (x : X) ⟿[K,n] f x := by fun_prop
+@[fun_prop]
+theorem ContCDiffMap_eval_CDifferentiable (h : 0 < n) :
+    CDifferentiable K (fun (fx : (X ⟿[K,n] Y)×X) => fx.1 fx.2) := by sorry_proof
+
+@[fun_prop]
+theorem ContCDiffMap_eval_CDifferentiable' :
+    CDifferentiable K (fun (fx : (X ⟿[K,∞] Y)×X) => fx.1 fx.2) := by sorry_proof
+
+
+@[fun_prop]
+theorem ContCDiffMap_apply_CDifferentiable (f : W → X ⟿[K,∞] Y) (g : W → X)
+    (hf : CDifferentiable K f) (hg : CDifferentiable K g) : CDifferentiable K (fun w => f w (g w)) := by sorry_proof
+
+@[fun_prop]
+theorem ContCDiffMap_apply_CDifferentiableAt (f : W → X ⟿[K,∞] Y) (g : W → X) (w : W)
+    (hf : CDifferentiableAt K f w) (hg : CDifferentiableAt K g w) : CDifferentiableAt K (fun w => f w (g w)) w := by sorry_proof

SciLean/Core/NotationOverField.lean

@@ -13,3 +13,22 @@ elab "open_notation_over_field" K:ident : command => do
    `(open SciLean.NotationOverField)
 
 macro "set_default_scalar " K:ident : command => `(open_notation_over_field $K)
+
+
+syntax "currentScalar%" : term
+
+macro_rules | `(currentScalar%) => Lean.Macro.throwError "\
+  There is no default scalar set right now. \
+  To set it, add this command somewhere to your file \
+  \n\n set_current_scalar R\
+  \n\n\
+  where R is the desired scalar, usually ℝ or Float.\n\n\
+  If you want to write code that is agnostic about the particular scalar \
+  type then introduce a generic type R with instance of `RealScalar R` \
+  \n\n  variable {R : Type _} [RealScalar R]\
+  \n  set_current_scalar R\
+  \n\n\
+  TODO: write a doc page about writing field polymorphic code and add a link here"
+
+macro "set_current_scalar" r:term : command =>
+  `(local macro_rules | `(currentScalar%) => `($r))

SciLean/Core/Rand/Distributions/WalkOnSpheres.lean

@@ -24,6 +24,7 @@ set_default_scalar Float
 
 def pi' := 3.14159265359
 
+
 open RealScalar in
 noncomputable
 def harmonicRec (n : ℕ) (φ : Vec3 → Float) (g : Vec3 → Y) (x : Vec3) : Y :=