SpectralDeficitDerivative.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Differentiating the overlap deficit away from atoms of the overlap law.

theorem OAI.InvariantIsing.hasDerivAt_deficit_of_nonatom line 17
Source documentation
At every non-atom of the path law, the derivative of D_p is minus the distribution function. This is the analytic step in rot:function-path.
```
theorem hasDerivAt_deficit_of_nonatom (p : OverlapPath) (r : ℝ)
    (hnonatom : pathMeasure {s | p s = r} = 0) :
    HasDerivAt (deficit p) (-pathMeasure.real {s | p s ≤ r}) r := by
…
```
Mentions: OAI.InvariantIsing.OverlapPath
theorem OAI.InvariantIsing.ae_hasDerivAt_deficit line 74