Scientific Computing in Lean

🖨

Differentiating Array Expressions

Talk about the problem of differentiating w.r.t. an array. Mention sparse update problem and structure sharing.

Talk about SciLean.revFDerivProj and SciLean.revFDerivProjUpdate.