Scientific Computing in Lean

https://lecopivo.github.io/scientific-computing-lean
Admin
Scientific Computing in Lean is a comprehensive guide and reference on using the Lean 4 programming...
Tokens:46,694
Snippets:331
Trust Score:9.7
Update:1 month ago
Show doc for...
Tokens:
Raw
### Sum and minimum reduction examples

Source: https://lecopivo.github.io/scientific-computing-lean/Working-with-Arrays/Tensor-Operations

Examples of summing elements and finding the minimum value in an array.

```Lean
#eval ⊞[1.0,2.0,3.0].foldl (·+·) 0
```

```Lean
#eval ⊞[1.0,2.0,3.0].reduce (min · ·)
```

```Lean
#eval ⊞[1.0,2.0,3.0].foldl (min · ·) 0
```

--------------------------------

### General Differentiation Setup

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Symbolic-Differentiation

Standard setup for differentiating a function between two normed spaces over an RCLike field.

```lean
variable {𝕜 : Type} [RCLike 𝕜] {X : Type} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {Y : Type} [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] set_default_scalar 𝕜 example (f g : X → Y) (hf : Differentiable 𝕜 f) (hg : Differentiable 𝕜 g) : (∂ x, (f x + g x)) = (∂ f) + (∂ g) := byx₀✝²:ℝhx₀✝²:x₀✝² ≠ 0x₀✝¹:ℝhx₀✝¹:x₀✝¹ ≠ 0x₀✝:ℝhx₀✝:x₀✝ ≠ 0x₀:ℝ × ℝhx₀:x₀ ≠ 0ε:ℝhε:0 < ε𝕜:Typeinst✝⁴:RCLike 𝕜X:Typeinst✝³:NormedAddCommGroup Xinst✝²:NormedSpace 𝕜 XY:Typeinst✝¹:NormedAddCommGroup Yinst✝:NormedSpace 𝕜 Yf:X → Yg:X → Yhf:Differentiable 𝕜 fhg:Differentiable 𝕜 g⊢ ∂ x, (f x + g x) = ∂ f + ∂ g ext x dxh.hx₀✝²:ℝhx₀✝²:x₀✝² ≠ 0x₀✝¹:ℝhx₀✝¹:x₀✝¹ ≠ 0x₀✝:ℝhx₀✝:x₀✝ ≠ 0x₀:ℝ × ℝhx₀:x₀ ≠ 0ε:ℝhε:0 < ε𝕜:Typeinst✝⁴:RCLike 𝕜X:Typeinst✝³:NormedAddCommGroup Xinst✝²:NormedSpace 𝕜 XY:Typeinst✝¹:NormedAddCommGroup Yinst✝:NormedSpace 𝕜 Yf:X → Yg:X → Yhf:Differentiable 𝕜 fhg:Differentiable 𝕜 gx:Xdx:X⊢ (∂ (x:=x), (f x + g x)) dx = ((∂ f + ∂ g) x) dx; fun_transAll goals completed! 🐙
```

--------------------------------

### Compute Gradient Examples

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Symbolic-Differentiation

Examples of computing gradients for specific functions using the ∇! notation.

```lean
(1, 0) : ℝ × ℝ
```

```lean
2 • x₀ : X
```

```lean
y : X
```

--------------------------------

### Example Usage of Quotients

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Working-with-Quotients

Demonstrates creating variables, performing operations, and comparing string representations before and after normalization.

```lean
def var (n : Nat) : ExprMonoid := ⟦.var n⟧ def e := var 0 * var 1 * 1 * 1 * var 0  -- show the mathematical element "(#0 * (#1 * (#0 * 1)))"#eval e.toString -- show the underlining representation "((((#0 * #1) * 1) * 1) * #0)"#eval e.toStringRepr -- show the underlining representation after normalization "(#0 * (#1 * (#0 * 1)))"#eval e.normalize.toStringRepr 
```

--------------------------------

### Product Size Calculation

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Typeclasses-as-Interfaces-and-Function-Overloading

Examples for calculating the size of product types, including both standard and flat (associativity-agnostic) versions.

```Lean
example : prodSize (Nat × Nat × Nat) = 3 := by decide
example : prodSize ((Nat × Nat) × Nat) = 2 := by decide

example : flatProdSize (Nat x Nat x Nat) = 3 := by decide
example : flatProdSize ((Nat x Nat) x Nat) = 3 := by decide
```

--------------------------------

### Algebraic Simplification Hint

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Symbolic-Differentiation

Example of using ring_nf and manual assumptions to handle algebraic expressions in proofs.

```Lean
  ring_nf --  m * (sqrt (k / m) * (sqrt (k / m) ==> m * sqrt (k * m⁻¹) ^ 2
  have h : m * sqrt (k * m⁻¹) ^ 2 = k := sorry_proof
  simp[h]
```

--------------------------------

### Evaluate Sum for Lists

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Typeclasses-as-Interfaces-and-Function-Overloading

Examples of evaluating the sum function on lists.

```lean
#eval sum [1, 2, 3, 4] 
#eval sum [[1, 2, 3], [4]] 
```

--------------------------------

### Symbolic Differentiation Example

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Automatic-Differentiation

Demonstrates the expression generated by symbolic differentiation for a power function.

```Lean
open SciLean Scalar 
fun x => 
  let y := x * x * x * x * x * x * x;
  let y_1 := x * x * x * x * x * x;
  let y_2 := x * x * x * x * x;
  let y_3 := x * x * x * x;
  let y_4 := x * x * x;
  let y_5 := x * x;
  let dy := x + x;
  let dy := y_5 + dy * x;
  let dy := y_4 + dy * x;
  let dy := y_3 + dy * x;
  let dy := y_2 + dy * x;
  let dy := y_1 + dy * x;
  y + dy * x : ℝ → ℝ
```

```Lean
#check ∂! (x : ℝ), x * x * x * x * x * x * x * x
```

--------------------------------

### Composition Rules for Function Transformations

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Function-Transformation

Examples of generalized composition rules for various function transformations like derivatives and adjoints.

```lean
      (∂ (f ∘ g) x dx) = (∂ f (g x) (∂ g x dx))

     (∂> (f ∘ g) x dx) = let (y,dy) := ∂> g x dx
                         (∂> f y dy)

        (<∂ (f ∘ g) x) = let (y,dg) := <∂ g x;
                         let (z,df) := <∂ f y;
                         (z, dg ∘ df)

     adjoint ℝ (A ∘ B) = adjoint ℝ B ∘ adjoint ℝ A
```

--------------------------------

### Sum Array Overload

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Typeclasses-as-Interfaces-and-Function-Overloading

Example usage of a custom sum function for arrays.

```Lean
example : sum (#[1,3,4], [#[(10,5),(20,8)], #[100]], 1000) = 1251 := by
  native_decide
```

--------------------------------

### Defining a Vector Space in Mathlib

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Symbolic-Differentiation

Example of introducing a new abstract vector space over a field R using AddCommGroup and Module.

```lean
variable {𝕜 : Type} [Field 𝕜] {X : Type} [AddCommGroup X] [Module 𝕜 X] example (s r : 𝕜) (x y : X) : (s + r) • (x + y) = s • x + r • x + s • y + r • y := byx₀✝²:ℝhx₀✝²:x₀✝² ≠ 0x₀✝¹:ℝhx₀✝¹:x₀✝¹ ≠ 0x₀✝:ℝhx₀✝:x₀✝ ≠ 0x₀:ℝ × ℝhx₀:x₀ ≠ 0ε:ℝhε:0 < ε𝕜:Typeinst✝²:Field 𝕜X:Typeinst✝¹:AddCommGroup Xinst✝:Module 𝕜 Xs:𝕜r:𝕜x:Xy:X⊢ (s + r) • (x + y) = s • x + r • x + s • y + r • y simp only [add_smul,smul_add,add_assoc]All goals completed! 🐙
```

--------------------------------

### Identity Rules for Function Transformations

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Function-Transformation

Examples of how different function transformations handle the identity function.

```lean
  (fderiv ℝ (fun x : ℝ => x)) = (fun _ => fun dx =>L[ℝ] dx)

        (∂> (fun x : ℝ => x)) = fun x dx => (x,dx)

        (<∂ (fun x : ℝ => x)) = fun x => (x, fun dx => dx)

 (adjoint ℝ (fun x : ℝ => x)) = fun x => x
```

--------------------------------

### Forward Mode Differentiation Example

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Automatic-Differentiation

Demonstrates the expression generated by forward-mode automatic differentiation for a power function.

```Lean
fun x dx => 
  let zdz := x * x;
  let zdz_1 := x * dx + dx * x;
  let zdz_2 := zdz * x;
  let zdz := zdz * dx + zdz_1 * x;
  let zdz_3 := zdz_2 * x;
  let zdz := zdz_2 * dx + zdz * x;
  let zdz_4 := zdz_3 * x;
  let zdz := zdz_3 * dx + zdz * x;
  let zdz_5 := zdz_4 * x;
  let zdz := zdz_4 * dx + zdz * x;
  let zdz_6 := zdz_5 * x;
  let zdz := zdz_5 * dx + zdz * x;
  let zdz_7 := zdz_6 * x;
  let zdz := zdz_6 * dx + zdz * x;
  (zdz_7, zdz) : ℝ → ℝ → ℝ × ℝ
```

```Lean
#check ∂>! (x : ℝ), x * x * x * x * x * x * x * x
```

--------------------------------

### Map operations on arrays

Source: https://lecopivo.github.io/scientific-computing-lean/Working-with-Arrays/Tensor-Operations

Examples of using mapMono to apply functions to vectors, matrices, and higher-rank arrays.

```Lean
#eval ⊞[1.0,2.0,3.0].mapMono (fun x => sqrt x)
```

```Lean
#eval ⊞[1.0,2.0;3.0,4.0].mapMono (fun x => sqrt x)
```

```Lean
#check (⊞ (i j k : Fin 2) => i.1.toFloat + 2 * j.1.toFloat + 4 * k.1.toFloat)
```

```Lean
#eval (⊞ (i j k : Fin 2) => i.1.toFloat + 2 * j.1.toFloat + 4 * k.1.toFloat).mapMono sqrt
```

--------------------------------

### Reshaping Array to Matrix

Source: https://lecopivo.github.io/scientific-computing-lean/Working-with-Arrays/Basic-Operations

Example of converting a flat array into a 2x2 matrix with a proof of size validity.

```lean
⊞[1.0, 2.0, 3.0, 4.0].reshape (Fin 2 × Fin 2) ⋯ : Float^[2, 2]#check ⊞[1.0, 2.0, 3.0, 4.0].reshape (Fin 2 × Fin 2) (byf:Fin 10 → Float⊢ size (Fin 2 × Fin 2) = size (Fin 4) decideAll goals completed! 🐙)
```

--------------------------------

### Evaluate Normalized Expression

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Working-with-Quotients

Example of normalizing a nested multiplication expression.

```Lean
`WorkingWithQuotients.Expr.mul   (WorkingWithQuotients.Expr.var 0)   (WorkingWithQuotients.Expr.mul     (WorkingWithQuotients.Expr.var 1)     (WorkingWithQuotients.Expr.mul       (WorkingWithQuotients.Expr.var 2)       (WorkingWithQuotients.Expr.mul (WorkingWithQuotients.Expr.var 3) (WorkingWithQuotients.Expr.one))))`#eval Expr.mul (.mul (.var 0) (.mul .one (.var 1))) (.mul (.var 2) (.var 3)) |>.normalize 
```

--------------------------------

### Compute Gradients of Vectors and Matrices

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Symbolic-Differentiation

Examples of using the gradient operator ∇! to compute gradients for vector and matrix expressions in Lean.

```Lean
set_default_scalar Float 
⊞[1.000000, 0.000000, 0.000000]
#eval ∇! (x:=⊞[1.0,2.0,3.0]), x[0] 
⊞[2.000000, 4.000000, 6.000000]
#eval ∇! (x:=⊞[1.0,2.0,3.0]), ‖x‖₂² 
⊞[0.000000, 1.000000, 0.000000]
#eval ∇! (x:=⊞[1.0,2.0,3.0]), ⟪x, ⊞[0.0,1.0,0.0]⟫ 
def matrix1 := ⊞[1.0,2.0;3.0,4.0] 
⊞[0.000000, 1.000000, 0.000000, 0.000000]
#eval ∇! (A:=matrix1), A[0,1] 
⊞[2.000000, 4.000000, 6.000000, 8.000000]
#eval ∇! (A:=matrix1), ‖A‖₂² 
⊞[0.000000, 1.000000, 0.000000, 0.000000]
#eval ∇! (A:=matrix1), ⟪A, ⊞[0.0,1.0;0.0,0.0]⟫
```

--------------------------------

### Differentiate a MapMono operation

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Function-Transformation

Example of differentiating a map operation on a DataArrayN that depends on a parameter.

```Lean
∂ s, DataArrayN.mapMono (fun x => s * x + s) ⊞[1.0, 2.0, 3.0] : Float → Float^[3]
```

```Lean
#check ∂ (s : Float), ⊞[1.0,2.0,3.0].mapMono (fun x => s * x + s) 
```

--------------------------------

### Tracing Instances with pp.all

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Typeclasses-as-Interfaces-and-Function-Overloading

Enable the pp.all option to reveal implicit arguments and the specific instances used in an expression.

```lean
set_option pp.all true in #check fun x : Int => - x
```

```lean
fun (x : Int) => @Neg.neg.{0} Int Int.instNegInt x : Int → Int
```

--------------------------------

### Create an Array in Lean

Source: https://lecopivo.github.io/scientific-computing-lean/Working-with-Arrays

Demonstrates creating an array using literal syntax and sequential pushing.

```Lean
#[1.0,2.0,3.0]
```

```Lean
(((Array.mkEmpty 3).push 1.0 ).push 2.0).push 3.0
```

--------------------------------

### Summation and Product Reductions

Source: https://lecopivo.github.io/scientific-computing-lean/Working-with-Arrays/Tensor-Operations

Demonstrates summation and product operations over arrays and matrices using SciLean notation.

```lean
def x := ⊞[1.0,2.0,3.0,4.0] def B := ⊞[1.0,2.0;3.0,4.0] #eval ∑ i, x[i]
```

```lean
#eval ∏ i, x[i]
```

```lean
#eval ∑ i j, B[i,j]
```

```lean
#eval ∏ i j, B[i,j]
```

--------------------------------

### Evaluate Failed Sum

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Typeclasses-as-Interfaces-and-Function-Overloading

Example of a failed synthesis when a type lacks a Sum instance.

```lean
#eval sum [("dog", 15), ("cat", 2), ("elephant", 400)] 
```

--------------------------------

### Inspecting Instance Definitions

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Typeclasses-as-Interfaces-and-Function-Overloading

Use the #print command to view the underlying definition of a specific typeclass instance.

```lean
#print Int.instNegInt
```

```lean
def Int.instNegInt : Neg ℤ := { neg := Int.neg }
```

--------------------------------

### Implement Sum for Products

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Typeclasses-as-Interfaces-and-Function-Overloading

Inductive step for the Sum typeclass to handle product types.

```lean
instance [Sum X] [Sum Y] : Sum (Prod X Y) where sum := fun (x, y) => sum x + sum y 
```

--------------------------------

### Apply fwdFDeriv' let_rule

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Function-Transformation

Demonstrates the application of the forward derivative rule for let-bindings within a Lean theorem proof.

```Lean
theorem fwdFDeriv'.let_rule (f : X → Y → Z) (hf : Differentiable R ↿f) (g : X → Y) (hg : Differentiable R g) : fwdFDeriv' R (fun x => let y := g x; f x y) = fun xdx => let ydy := fwdFDeriv' R g xdx let xydxy := ((xdx.1,ydy.1),(xdx.2,ydy.2)) fwdFDeriv' R (fun (x,y) => f x y) xydxy := byR:Typeinst✝⁶:RealScalar RX:Typeinst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace R XY:Typeinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace R YZ:Typeinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace R Zf:X → Y → Zhf:Differentiable R ↿fg:X → Yhg:Differentiable R g⊢ (fwdFDeriv' R fun x =>     let y := g x;     f x y) =   fun xdx =>   let ydy := fwdFDeriv' R g xdx;   let xydxy := ((xdx.1, ydy.1), xdx.2, ydy.2);   fwdFDeriv' R     (fun x =>       match x with       | (x, y) => f x y)     xydxy unfold fwdFDeriv'R:Typeinst✝⁶:RealScalar RX:Typeinst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace R XY:Typeinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace R YZ:Typeinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace R Zf:X → Y → Zhf:Differentiable R ↿fg:X → Yhg:Differentiable R g⊢ (fun xdx =>     ((fun x =>           let y := g x;           f x y)         xdx.1,       (∂ (x:=xdx.1),           let y := g x;           f x y)         xdx.2)) =   fun xdx =>   let ydy := (g xdx.1, (∂ g xdx.1) xdx.2);   let xydxy := ((xdx.1, ydy.1), xdx.2, ydy.2);   ((fun x =>         match x with         | (x, y) => f x y)       xydxy.1,     (∂ (x:=xydxy.1),         match x with         | (x, y) => f x y)       xydxy.2); fun_transAll goals completed! 🐙
```

--------------------------------

### Optimized Iteration for Matrix Initialization

Source: https://lecopivo.github.io/scientific-computing-lean/Working-with-Arrays/Basic-Operations

Uses a single loop over the product range to populate a mutable matrix.

```Lean
def outerProduct'' {n m : Nat} (x : Float^[n]) (y : Float^[m]) := Id.run do let mut A : Float^[n,m] := 0 for (i,j) in (fullRange (Fin n × Fin m)) do A[i,j] := x[i]*y[j] return A
```

--------------------------------

### Product and Projection Rules for fwdFDeriv'

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Function-Transformation

Defines rules for product construction and tuple projections.

```Lean
@[fun_trans] theorem Prod.mk.arg_fstsnd.fwdFDeriv'_rule (g : X → Y) (f : X → Z) (hg : Differentiable R g) (hf : Differentiable R f) : fwdFDeriv' R (fun x : X => (g x, f x)) = fun xdx => let ydy := fwdFDeriv' R g xdx let zdz := fwdFDeriv' R f xdx ((ydy.1,zdz.1),(ydy.2,zdz.2)) := byR:Typeinst✝⁶:RealScalar RX:Typeinst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace R XY:Typeinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace R YZ:Typeinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace R Zg:X → Yf:X → Zhg:Differentiable R ghf:Differentiable R f⊢ (fwdFDeriv' R fun x => (g x, f x)) = fun xdx =>   let ydy := fwdFDeriv' R g xdx;   let zdz := fwdFDeriv' R f xdx;   ((ydy.1, zdz.1), ydy.2, zdz.2) unfold fwdFDeriv'R:Typeinst✝⁶:RealScalar RX:Typeinst✝⁵:NormedAddCommGroup Xinst✝⁴:NormedSpace R XY:Typeinst✝³:NormedAddCommGroup Yinst✝²:NormedSpace R YZ:Typeinst✝¹:NormedAddCommGroup Zinst✝:NormedSpace R Zg:X → Yf:X → Zhg:Differentiable R ghf:Differentiable R f⊢ (fun xdx => ((fun x => (g x, f x)) xdx.1, (∂ (x:=xdx.1), (g x, f x)) xdx.2)) = fun xdx =>   let ydy := (g xdx.1, (∂ g xdx.1) xdx.2);   let zdz := (f xdx.1, (∂ f xdx.1) xdx.2);   ((ydy.1, zdz.1), ydy.2, zdz.2); fun_transAll goals completed! 🐙
```

```Lean
@[fun_trans] theorem Prod.fst.arg_self.fwdFDeriv'_rule : fwdFDeriv' R (fun (xy : X×Y) => xy.1) = fun xydxy => (xydxy.1.1,xydxy.2.1) := byR:Typeinst✝⁴:RealScalar RX:Typeinst✝³:NormedAddCommGroup Xinst✝²:NormedSpace R XY:Typeinst✝¹:NormedAddCommGroup Yinst✝:NormedSpace R Y⊢ (fwdFDeriv' R fun xy => xy.1) = fun xydxy => (xydxy.1.1, xydxy.2.1) unfold fwdFDeriv'R:Typeinst✝⁴:RealScalar RX:Typeinst✝³:NormedAddCommGroup Xinst✝²:NormedSpace R XY:Typeinst✝¹:NormedAddCommGroup Yinst✝:NormedSpace R Y⊢ (fun xdx => ((fun xy => xy.1) xdx.1, (∂ (xy:=xdx.1), xy.1) xdx.2)) = fun xydxy => (xydxy.1.1, xydxy.2.1); fun_transAll goals completed! 🐙
```

```Lean
@[fun_trans] theorem Prod.snd.arg_self.fwdFDeriv'_rule : fwdFDeriv' R (fun (xy : X×Y) => xy.2) = fun xydxy => (xydxy.1.2,xydxy.2.2) := byR:Typeinst✝⁴:RealScalar RX:Typeinst✝³:NormedAddCommGroup Xinst✝²:NormedSpace R XY:Typeinst✝¹:NormedAddCommGroup Yinst✝:NormedSpace R Y⊢ (fwdFDeriv' R fun xy => xy.2) = fun xydxy => (xydxy.1.2, xydxy.2.2) unfold fwdFDeriv'R:Typeinst✝⁴:RealScalar RX:Typeinst✝³:NormedAddCommGroup Xinst✝²:NormedSpace R XY:Typeinst✝¹:NormedAddCommGroup Yinst✝:NormedSpace R Y⊢ (fun xdx => ((fun xy => xy.2) xdx.1, (∂ (xy:=xdx.1), xy.2) xdx.2)) = fun xydxy => (xydxy.1.2, xydxy.2.2); fun_transAll goals completed! 🐙
```

--------------------------------

### Parametrize function application

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Function-Transformation

Demonstrates how to parametrize the apply function by a variable w for differentiation.

```Lean
fun w => apply (fun x => w * x + w) (1 + w) : R → R
```

```Lean
#check fun w : R => apply (fun x : R => w * x + w) (1 + w) 
```

--------------------------------

### Differentiate functions of multiple arguments

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Symbolic-Differentiation

Demonstrates calculating derivatives for a function f: ℝ → ℝ → ℝ with respect to the first, second, or both arguments.

```lean
variable (f : ℝ → ℝ → ℝ) (x₀ y₀ : ℝ)  -- first argument `∂ (x:=x₀), f x y₀ : ℝ`#check ∂ (x:=x₀), (f x y₀) `∂ (x:=x₀), f x y₀ : ℝ`#check ∂ (f · y₀) x₀ -- second agument `∂ (y:=y₀), f x₀ y : ℝ`#check ∂ (y:=y₀), (f x₀ y) `∂ (x:=y₀), f x₀ x : ℝ`#check ∂ (f x₀ ·) y₀ -- both arguments `∂ (x:=(x₀, y₀)),   match x with   | (x, y) => f x y : ℝ × ℝ →L[ℝ] ℝ`#check ∂ ((x,y):=(x₀,y₀)), f x y
```

--------------------------------

### Flexible avgPool Implementation

Source: https://lecopivo.github.io/scientific-computing-lean/Working-with-Arrays/Tensor-Operations

A robust implementation of a 1D average pooling function that uses an implicit proof obligation to infer the output dimension.

```Lean
def avgPool (x : Float^[n]) {m} (h : m = n/2 := by infer_var) : Float^[m] := ⊞ (i : Fin m) => let i1 : Fin n := ⟨2*i.1, byn:ℕx:Float^[n]m:ℕh:autoParam (m = n / 2) _auto✝i:Fin m⊢ 2 * ↑i < n omegaAll goals completed! 🐙⟩ let i2 : Fin n := ⟨2*i.1+1, byn:ℕx:Float^[n]m:ℕh:autoParam (m = n / 2) _auto✝i:Fin mi1:Fin n := ⟨2 * ↑i, ⋯⟩⊢ 2 * ↑i + 1 < n omegaAll goals completed! 🐙⟩ 0.5 * (x[i1] + x[i2]) 
```

--------------------------------

### Create and Access Matrix

Source: https://lecopivo.github.io/scientific-computing-lean/Working-with-Arrays/Basic-Operations

Creates a matrix and accesses elements using both multi-index and tuple notation.

```Lean
def A := ⊞[1.0, 2.0; 3.0, 4.0] 
```

```Lean
#eval A[0,1] 
```

```Lean
#eval A[(1,0)] 
```

--------------------------------

### Simulate harmonic oscillator

Source: https://lecopivo.github.io/scientific-computing-lean/Examples/Harmonic-Oscillator

Runs the solver in an IO loop to simulate the oscillator and print a simple visualization.

```Lean
def sim : IO Unit := do let substeps := 1 let m := 1.0 let k := 10.0 let Δt := 0.1 let x₀ := 1.0 let p₀ := 0.0 let mut t := 0 let mut (x,p) := (x₀, p₀) for _ in [0:50] do (x, p) := solver m k substeps t (t+Δt) (x, p) t += Δt      -- poor man's visualization     for (j : Nat) in [0:20] do if j.toFloat < 10*(x+1.0) then IO.print "o" IO.println ""
```

```Lean
#eval sim
```

--------------------------------

### Modular vs Natural Number Arithmetic in Fin

Source: https://lecopivo.github.io/scientific-computing-lean/Working-with-Arrays/Tensor-Operations

Demonstrates the difference between modular arithmetic on Fin types and standard natural number arithmetic.

```Lean
def i : Fin 10 := 6 ```2`#eval 2*i 
```

```Lean
``12`#eval 2*i.1 
```

--------------------------------

### Inspect heterogeneous operators

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Typeclasses-as-Interfaces-and-Function-Overloading

Shows how standard operators like + and ++ map to underlying typeclass methods.

```lean
set_option pp.notation false in `HAdd.hAdd 2 3 : Nat`#check 2 + 3 
```

```lean
#eval 2 + 3 
```

```lean
set_option pp.notation false in `HAppend.hAppend (List.cons 1 (List.cons 2 (List.cons 3 List.nil)))   (List.cons 4 (List.cons 5 (List.cons 6 List.nil))) : List Nat`#check [1, 2, 3] ++ [4, 5, 6] 
```

```lean
#eval [1, 2, 3] ++ [4, 5, 6] 
```

--------------------------------

### Summary of derivative notations

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Symbolic-Differentiation

Various syntax patterns for scalar and vector-valued differentiation.

```Lean
#check ∂ f
#check ∂ x, f x
#check ∂ (x:=x₀), f x
#check ∂ f
#check ∂ u, g u
#check ∂ (u:=u₀), g u
#check ∂ (u:=u₀;du₀), g u
```

--------------------------------

### Mutable Matrix Initialization

Source: https://lecopivo.github.io/scientific-computing-lean/Working-with-Arrays/Basic-Operations

Initializes a mutable matrix with zeros and populates it using nested loops.

```Lean
def outerProduct {n m : Nat} (x : Float^[n]) (y : Float^[m]) := Id.run do let mut A : Float^[n,m] := 0 for i in fullRange (Fin n) do for j in fullRange (Fin m) do A[i,j] := x[i]*y[j] return A
```

--------------------------------

### Discovering Typeclass Instances with #synth

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Typeclasses-as-Interfaces-and-Function-Overloading

Use the #synth command to identify the specific instance of a typeclass being applied to a type.

```lean
#synth Neg Int
```

```lean
Int.instNegInt
```

--------------------------------

### Chain Rule for Forward Mode

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Automatic-Differentiation

Demonstration of the chain rule for the forward mode derivative using standard and uncurried notation.

```lean
example : (∂> (f ∘ g) x dx) = let (y,dy) := (∂> g x dx) (∂> f y dy) := byf:ℝ → ℝg:ℝ → ℝx:ℝdx:ℝhf:Differentiable ℝ fhg:Differentiable ℝ g⊢ ∂> (f ∘ g) x dx =   match ∂> g x dx with   | (y, dy) => ∂> f y dy fun_trans[Function.comp_def]All goals completed! 🐙
```

```lean
example : ↿(∂> (f ∘ g)) = ↿(∂> f) ∘ ↿(∂> g) := byf:ℝ → ℝg:ℝ → ℝx:ℝdx:ℝhf:Differentiable ℝ fhg:Differentiable ℝ g⊢ ↿(∂> f ∘ g) = ↿(∂> f) ∘ ↿(∂> g) fun_trans[Function.comp_def,Function.HasUncurry.uncurry]All goals completed! 🐙
```

--------------------------------

### Compute derivative of x^n using fun_trans

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Symbolic-Differentiation

Demonstrates computing the derivative of x^n at a point using the fun_trans tactic.

```Lean
#check (fderiv ℝ (fun (x : ℝ) => x^n) x 1) rewrite_by fun_trans
```

```text
↑n * x ^ (n - 1) : ℝ
```

--------------------------------

### Affine Rule for Forward Differentiation

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Function-Transformation

A Lean theorem proof demonstrating the affine rule for forward differentiation.

```Lean
theorem fwdFDeriv'.affine_rule (f : X → Y) (hf : IsAffineMap R f) (hf' : Continuous f) : fwdFDeriv' R f = fun xdx => (f xdx.1, f xdx.2 - f 0) := by
  unfold fwdFDeriv'
  funext (x,dx)
  let g := (fun x => f x - f 0)
  have hf'' : IsContinuousLinearMap R g := by
    constructor
    linear
    cont
    apply hf.1
  have h : f = fun x => g x + f 0 := by
    simp (config:={zetaDelta:=true})
  rw[h]
  fun_trans
  sorry
```

--------------------------------

### Evaluate Mathlib Uncurry

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Typeclasses-as-Interfaces-and-Function-Overloading

Testing the built-in mathlib uncurry notation.

```lean
#eval (↿fun a b c d : Nat => a + b + c + d) (1,2,3,4) 
```

--------------------------------

### Compare fun_trans and autodiff Tactics

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Automatic-Differentiation

Comparison of code generation between fun_trans and autodiff, where autodiff preserves let bindings for efficiency.

```lean
#check (∂ (x : ℝ), let y := x*x; y*x) rewrite_by unfold derivf:ℝ → ℝg:ℝ → ℝx:ℝdx:ℝhf:Differentiable ℝ fhg:Differentiable ℝ g| fun x => (∂ (x:=x), let y := x * x; y * x) 1; fun_transf:ℝ → ℝg:ℝ → ℝx:ℝdx:ℝhf:Differentiable ℝ fhg:Differentiable ℝ g| fun x => x * x + (x + x) * x
```

```lean
#check (∂ (x : ℝ), let y := x*x; y*x) rewrite_by autodifff:ℝ → ℝg:ℝ → ℝx:ℝdx:ℝhf:Differentiable ℝ fhg:Differentiable ℝ g| fun x => let y := x * x; let dy := x + x; let dz := y + dy * x; dz
```

--------------------------------

### Curry Function Implementation

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Typeclasses-as-Interfaces-and-Function-Overloading

Implementation of a curry function for product types using typeclasses.

```Lean
#eval (Curry.curry fun ((a,b,c,d) : ℕ×ℕ×ℕ×ℕ) => a + b + c + d) 1 2 3 4
```

--------------------------------

### Automated Theorem Generation

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Symbolic-Differentiation

Use def_fun_prop and def_fun_trans macros to automatically generate required theorems.

```lean
def_fun_prop : Differentiable ℝ foo by
unfold foo
⊢ Differentiable ℝ fun x => x ^ 2 + x;
fun_prop
All goals completed! 🐙

def_fun_trans : fderiv ℝ foo by
unfold foo
| ∂ x, (x ^ 2 + x);
fun_trans
| fun x => fun x_1 =>L[ℝ] 2 * x_1 * x + x_1
```

--------------------------------

### Wrap solver for execution

Source: https://lecopivo.github.io/scientific-computing-lean/Examples/Harmonic-Oscillator

Wraps the generated solver into a function that can be called with specific parameters.

```Lean
fun m k substep t₀ t x =>   match x with   | (x, p) =>     ApproxSolution.val (solver m k) substep t₀ t       (x, p) : Float → Float → ℕ × Unit → Float → Float → Float × Float → Float × Float
```

```Lean
#check fun m k substep t₀ t (x,p) => solver m k substep t₀ t (x,p)
```

--------------------------------

### Implement Sum for Lists

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Typeclasses-as-Interfaces-and-Function-Overloading

Inductive step for the Sum typeclass to handle lists.

```lean
instance [Sum A] : Sum (List A) where sum l := l.foldl (fun acc a => acc + sum a) 0 
```

--------------------------------

### Construct an element of a quotient type

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Working-with-Quotients

Uses Quot.mk to create an instance of the quotient type from a representative.

```Lean
Quot.mk equiv (1, 2) : Quot equiv
```

```Lean
#check Quot.mk equiv (1, 2) 
```

--------------------------------

### Evaluate Uncurry

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Typeclasses-as-Interfaces-and-Function-Overloading

Testing the custom uncurry implementation.

```lean
#eval uncurry (fun a b c d : Nat => a + b + c + d) (1,2,3,4) 
```

--------------------------------

### Evaluate overloaded size function

Source: https://lecopivo.github.io/scientific-computing-lean/Miscellaneous/Typeclasses-as-Interfaces-and-Function-Overloading

Demonstrates the usage of the overloaded size function across different types.

```lean
#eval Size.size [1, 2, 3] 
```

```lean
#eval Size.size "hello" 
```

```lean
#eval Size.size () 
```

--------------------------------

### Differentiate a Sum of Functions in SciLean

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Symbolic-Differentiation

Demonstrates the linearity of the gradient operator for the sum of two differentiable functions in an abstract vector space.

```Lean
open SciLean variable {𝕜 : Type} [RCLike 𝕜] {X : Type} [NormedAddCommGroup X] [AdjointSpace 𝕜 X] [CompleteSpace X] {Y : Type} [NormedAddCommGroup Y] [AdjointSpace 𝕜 Y] [CompleteSpace Y] set_default_scalar 𝕜 example (f g : X → Y) (hf : Differentiable 𝕜 f) (hg : Differentiable 𝕜 g) : (∇ x, (f x + g x)) = (∇ f) + (∇ g) := byx₀✝²:ℝhx₀✝²:x₀✝² ≠ 0x₀✝¹:ℝhx₀✝¹:x₀✝¹ ≠ 0x₀✝:ℝhx₀✝:x₀✝ ≠ 0x₀:ℝ × ℝhx₀:x₀ ≠ 0ε:ℝhε:0 < ε𝕜:Typeinst✝⁶:RCLike 𝕜X:Typeinst✝⁵:NormedAddCommGroup Xinst✝⁴:AdjointSpace 𝕜 Xinst✝³:CompleteSpace XY:Typeinst✝²:NormedAddCommGroup Yinst✝¹:AdjointSpace 𝕜 Yinst✝:CompleteSpace Yf:X → Yg:X → Yhf:Differentiable 𝕜 fhg:Differentiable 𝕜 g⊢ ∇ x, (f x + g x) = ∇ f + ∇ g ext xh.hx₀✝²:ℝhx₀✝²:x₀✝² ≠ 0x₀✝¹:ℝhx₀✝¹:x₀✝¹ ≠ 0x₀✝:ℝhx₀✝:x₀✝ ≠ 0x₀:ℝ × ℝhx₀:x₀ ≠ 0ε:ℝhε:0 < ε𝕜:Typeinst✝⁶:RCLike 𝕜X:Typeinst✝⁵:NormedAddCommGroup Xinst✝⁴:AdjointSpace 𝕜 Xinst✝³:CompleteSpace XY:Typeinst✝²:NormedAddCommGroup Yinst✝¹:AdjointSpace 𝕜 Yinst✝:CompleteSpace Yf:X → Yg:X → Yhf:Differentiable 𝕜 fhg:Differentiable 𝕜 gx:Xx✝:Y⊢ ∇ (x:=x;x✝), (f x + g x) = (∇ f + ∇ g) x x✝; autodiffx₀✝²:ℝhx₀✝²:x₀✝² ≠ 0x₀✝¹:ℝhx₀✝¹:x₀✝¹ ≠ 0x₀✝:ℝhx₀✝:x₀✝ ≠ 0x₀:ℝ × ℝhx₀:x₀ ≠ 0ε:ℝhε:0 < ε𝕜:Typeinst✝⁶:RCLike 𝕜X:Typeinst✝⁵:NormedAddCommGroup Xinst✝⁴:AdjointSpace 𝕜 Xinst✝³:CompleteSpace XY:Typeinst✝²:NormedAddCommGroup Yinst✝¹:AdjointSpace 𝕜 Yinst✝:CompleteSpace Yf:X → Yg:X → Yhf:Differentiable 𝕜 fhg:Differentiable 𝕜 gx:Xx✝:Y⊢ let ydf := <∂ f x; let ydg := <∂ g x; ydf.2 x✝ + ydg.2 x✝ = (<∂ f x).2 x✝ + (<∂ g x).2 x✝; rflAll goals completed! 🐙
```

--------------------------------

### Create and Access DataArray

Source: https://lecopivo.github.io/scientific-computing-lean/Working-with-Arrays/Basic-Operations

Creates a DataArray and accesses its elements using bracket notation.

```Lean
def u := ⊞[1.0, 2.0, 3.0] 
```

```Lean
#eval u[0] 
```

```Lean
#eval u[1] 
```

```Lean
#eval u[2] 
```

--------------------------------

### Differentiate functions of tuples

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Symbolic-Differentiation

Shows how to compute derivatives for a function g: ℝ×ℝ → ℝ with respect to specific coordinates or vectors.

```lean
variable (g : ℝ×ℝ → ℝ) (x₀ y₀ : ℝ) `(∂ (xy:=(x₀, y₀)), g xy) (1, 0) : ℝ`#check ∂ (xy:=(x₀,y₀);(1,0)), g xy `(∂ g (x₀, y₀)) (1, 0) : ℝ`#check ∂ g (x₀,y₀) (1,0) `∂ (x:=x₀), g (x, y₀) : ℝ`#check ∂ (x:=x₀), g (x,y₀)
```

--------------------------------

### Prove Wave Equation Solution

Source: https://lecopivo.github.io/scientific-computing-lean/Differentiation/Symbolic-Differentiation

Proof that a sine function satisfies the wave equation.

```Lean
open SciLean Scalar def WaveEquation (u : ℝ → ℝ → ℝ) := ∀ x t, (∂ (∂ (u · x)) t) = (∂ (∂ (u t ·)) x) example : WaveEquation (fun t x => sin (x - t)) := by⊢ WaveEquation fun t x => sin (x - t) unfold WaveEquation deriv⊢ ∀ (x t : ℝ),   (∂ (x_1:=t), (∂ (x_2:=x_1), (fun t x => sin (x - t)) x_2 x) 1) 1 =     (∂ (x:=x), (∂ (x:=x), (fun t x => sin (x - t)) t x) 1) 1 fun_transAll goals completed! 🐙 
```

--------------------------------

### VAdd Instance Definitions

Source: https://lecopivo.github.io/scientific-computing-lean/Working-with-Arrays/Tensor-Operations

Instances for the VAdd typeclass to support shifting indices across different types.

```Lean
instance (n : ℕ) : VAdd ℤ (Fin n) := ⟨fun j i => ⟨((Int.ofNat i.1 + j)%n).toNat, sorry_proof⟩⟩ instance (a b : ℤ) (n : ℕ) : VAdd (Set.Icc a b) (Fin n) := ⟨fun j i => j.1 +ᵥ i⟩ instance {I I' J J'} [VAdd J I] [VAdd J' I'] : VAdd (J×J') (I×I') := ⟨fun (j,j') (i,i') => (j+ᵥi, j'+ᵥi')⟩
```
Tokens:
Raw