VolterraDifferentiation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The moving-endpoint part of differentiation of a Volterra integral.

theorem OAI.ForcedComputation.hasDerivAt_shrinking_integral line 18
Source documentation
Joint continuity is enough for the derivative of an integral over a shrinking interval, even when its integrand depends on the moving endpoint.
```
theorem hasDerivAt_shrinking_integral (f : ℝ → ℝ → F)
    (hf : Continuous (Function.uncurry f)) (a : ℝ) :
    HasDerivAt (fun t => ∫ s in a..t, f t s) (f a a) a := by
…
```

theorem OAI.ForcedComputation.hasDerivAt_volterra_of_fixed line 46

Source documentation

Leibniz' rule after the fixed-endpoint derivative has been justified by dominated differentiation.

theorem hasDerivAt_volterra_of_fixed (f : ℝ → ℝ → F)
    (hf : Continuous (Function.uncurry f)) (a t : ℝ) (d : F)
    (hd : HasDerivAt (fun u => ∫ s in a..t, f u s) d t) :
    HasDerivAt (fun u => ∫ s in a..u, f u s) (d + f t t) t := by
…