Merge remote-tracking branch 'origin/master'

.devcontainer/Dockerfile

@@ -0,0 +1,9 @@
+FROM mcr.microsoft.com/devcontainers/base:jammy
+
+USER vscode
+WORKDIR /home/vscode
+ENV HOME=/home/vscode
+
+RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+
+ENV PATH="/home/vscode/.elan/bin:${PATH}"

.devcontainer/devcontainer.json

@@ -0,0 +1,21 @@
+// For format details, see https://aka.ms/devcontainer.json. For config options, see the
+// README at: https://github.com/devcontainers/templates/tree/main/src/ubuntu
+{
+  "name": "Lean DevContainer on Ubuntu",
+  "build": {
+    "dockerfile": "Dockerfile"
+  },
+
+  "onCreateCommand": "lake exe cache get! && lake build",
+
+  "postStartCommand": "git config --global --add safe.directory ${containerWorkspaceFolder}",
+
+  "customizations": {
+    "vscode" : {
+      "extensions" : [
+        "leanprover.lean4",
+        "mhutchie.git-graph"
+      ]
+    }
+  }
+}

.github/workflows/main.yml

@@ -26,21 +26,15 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  build: 
+  build:
     runs-on: ubuntu-latest
     steps:
-      - name: Install elan
-        run: |
-          set -o pipefail
-          curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
-          ./elan-init -y --default-toolchain none
-          echo "$HOME/.elan/bin" >> $GITHUB_PATH
-      - name: Checkout
-        uses: actions/checkout@v3
-      - name: Download cached build
-        run: lake exe cache get
-      - name: Build SciLean
-        run: lake build
+      - name: checkout
+        uses: actions/checkout@v4
+      - name: lean action
+        uses: leanprover/lean-action@v1
+        with:
+          build-args: "--log-level=error"
       - name: Run Tests
         run: make test
       - name: Run Examples

SciLean/Analysis/Calculus/FwdFDeriv.lean

@@ -22,7 +22,7 @@ variable {K}
 -- Basic lambda calculus rules -------------------------------------------------
 --------------------------------------------------------------------------------
 
-namespace FwdFDeriv
+namespace fwdFDeriv
 
 @[fun_trans]
 theorem id_rule
@@ -115,19 +115,34 @@ theorem pi_rule
   rw[fderiv_pi (h:=by fun_prop)]
   simp
 
-
-open SciLean
-
 -- of linear function ----------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_trans]
-theorem fwdFDeriv_linear
+theorem linear_rule
   (f : X → Y) (hf : IsContinuousLinearMap K f) :
   fwdFDeriv K f
   =
   fun x dx => (f x, f dx) := by unfold fwdFDeriv; fun_trans
 
+end fwdFDeriv
+
+
+--------------------------------------------------------------------------------
+
+end SciLean
+open SciLean
+
+
+variable
+  {K : Type _} [RCLike K]
+  {X : Type _} [NormedAddCommGroup X] [NormedSpace K X]
+  {Y : Type _} [NormedAddCommGroup Y] [NormedSpace K Y]
+  {Z : Type _} [NormedAddCommGroup Z] [NormedSpace K Z]
+  {ι : Type _} [IndexType ι]
+  {E : ι → Type _} [∀ j, NormedAddCommGroup (E j)] [∀ j, NormedSpace K (E j)]
+
+
 
 -- Prod.mk ---------------------------------------------------------------------
 --------------------------------------------------------------------------------

SciLean/Data/Fintype/Quotient.lean

@@ -0,0 +1,19 @@
+import Mathlib.Data.Fintype.Quotient
+
+/-!
+
+This files contains missing API for `Quotient`.
+
+Hopefully this PR gets merged to mathlib and this file won't be necessary
+https://github.com/leanprover-community/mathlib4/pull/5576
+
+-/
+
+namespace Quotient
+
+variable {ι : Type*} [Fintype ι] [DecidableEq ι] {α : ι → Type*} [S : ∀ i, Setoid (α i)] {β : Sort*}
+
+/-- Lift a function on `∀ i, α i` to a function on `∀ i, Quotient (S i)`. -/
+def finLiftOn (q : ∀ i, Quotient (S i)) (f : (∀ i, α i) → β)
+    (h : ∀ (a b : ∀ i, α i), (∀ i, a i ≈ b i) → f a = f b) : β :=
+  (Quotient.finChoice q).liftOn (β:=β) f h

notes.org

@@ -21,7 +21,7 @@
 *** TODO Lean Framework
 
    Implement these to in the order to get these examples working:
-     1. Harmonic Oscilator
+     1. Harmonic Oscillator
      2. Pendulum
      3. NBody
      4. NPendulum in 2D

test/deriving/structure_ops.lean

@@ -92,8 +92,18 @@ def UniformSpace.ofEquiv {X Y : Type*} [UniformSpace X] [TopologicalSpace Y] (f
   comp := sorry_proof
   nhds_eq_comap_uniformity := sorry_proof
 
-instance {R X Y : Type*} [RCLike R] [Vec R X] [Vec R Y] : Vec R ((_ : X) × Y) := Vec.mkSorryProofs
+instance {X Y : Type*} [AddCommGroup X] [AddCommGroup Y] : AddCommGroup ((_ : X) × Y) where
+  add_assoc := sorry_proof
+  zero_add := sorry_proof
+  add_zero := sorry_proof
+  nsmul n ⟨x,y⟩ := ⟨n•x, n•y⟩
+  zsmul i ⟨x,y⟩ := ⟨i•x, i•y⟩
+  zsmul := sorry_proof
+  neg_add_cancel := sorry_proof
+  add_comm := sorry_proof
+
 
+instance {R X Y : Type*} [RCLike R] [Vec R X] [Vec R Y] : Vec R ((_ : X) × Y) := Vec.mkSorryProofs
 
 instance {X Y} [Add R] [Inner R X] [Inner R Y] : Inner R ((_ : X) × Y) where
   inner | ⟨x1, y1⟩, ⟨x2, y2⟩ => inner x1 x2 + inner y1 y2

todo.org

@@ -68,7 +68,7 @@
 
 * Differentiability at point
 
-  Try define smoothenss/differentiability at a point. I really want to work with =1/x= without problems and assume that it is differentiable for every =x≠0=.
+  Try define smoothness/differentiability at a point. I really want to work with =1/x= without problems and assume that it is differentiable for every =x≠0=.
 
 * Machine learning
 
@@ -106,13 +106,13 @@
 
   - working with polynomials, differential forms, tensor products
 
-**  Goal is to get isomophisms:
+**  Goal is to get isomorphisms:
 
     𝓟[U×V, K] ≅ 𝓟[U, 𝓟[V, K]]
 
   - Using these isomorphisms we can get polynomial to a form 𝓟[ℝ, K] and on that we can define HornerForm is K has HornerForm
 
-  - In some sense these ismorphisms must be true:
+  - In some sense these isomorphisms must be true:
 
     𝓐[U×V, K] ≅ 𝓐[U, 𝓐[V, K]]
 
@@ -133,7 +133,7 @@
 * Approximating Spaces
 
   - Define abstract interface for a type to approximate another type
-  - will be usefull for creating finite elements, hybrid methods
+  - will be useful for creating finite elements, hybrid methods
     or finite elements
 
 * Manifolds through Quot