Scientific Computing in Lean
📖
🖨
Introduction
Introduction
Why Lean for Scientific Computing?
Working with Arrays
Basic Operations
Reshaping Arrays
Exercises
Tensor Operations
Transformations and Reductions
Convolution and Operations on Indices
Pooling and Difficulties with Dependent Types
Simple Neural Network
Optimizing Array Expressions
Loop Fusion
Optimizing Array Indexing
🚧 Differentiation
Symbolic Differentiation
Notation
Examples
Gradient
Derivative Rules
Differentiating Division, Log, Sqrt, ...
Abstract Vector Spaces
Automatic Differentiation
Forward Mode
Reverse Mode
Derivatives of Neural Network Layers
Derivative Rules
Basic Rules
Rules with Conditions
Higher Order Functions
Recursive Functions
Custom Structures
Polymorphics Functions
Differentiating Array Expressions
Imperative and Monadic Code
Control flow
Differentiable Monad
Forward Derivative Monad
Reverse Derivative Monad
Variational Calculus
🚧 Function Transformation
User Defined Function Transformation
Lambda Theorems
Function Theorems
Free Variable Theorems
Morphism Theorems
Advanced Function Theorems
Expression Compiler
Compiling from Lean to Expressions
Miscellaneous
Typeclasses as Interfaces and Function Overloading
Function overloading
Typeclasses as Interfaces
Working with Quotients
Unordered Pair
Symbolic Expressions
Examples
Harmonic Oscillator
Introduction
Introduction
Why Lean for Scientific Computing?
The Role of Dependent Types?
Benefits of Interactivity