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
Miscellaneous
Typeclasses as Interfaces and Function Overloading
Function overloading
Where is the Overloaded Function Defined?
Finding the Definition Using
#synth
Alternative Method: Using
pp.all
Defining Functions "Inductively" on the Type
Example: Summing Nested Structures
Base Case: Natural Numbers
Inductive Step: Lists
Inductive Step: Products
Handling More Complex Cases
Working with Functions of Arbitrary Arity
Exercise
Polymorphism Over Types and Terms
Exercises
Typeclasses as Interfaces
Defining an Array-like Interface
Implementing the Interface
Extending the Interface to Other Types
Conclusion
Working with Quotients
Unordered Pair
Symbolic Expressions
Monoid Structure of
ExprMonoid
Example Usage