OAI/Probability/BenjaminiSchramm/SusceptibilityDerivative.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Percolation.BenjaminiSchramm.realSusceptibility line 15
2. theorem OAI.Percolation.BenjaminiSchramm.realSusceptibility_coe line 18
3. theorem OAI.Percolation.BenjaminiSchramm.summable_russoSlope line 22
4. theorem OAI.Percolation.BenjaminiSchramm.hasDerivAt_realSusceptibility line 30
5. theorem OAI.Percolation.BenjaminiSchramm.susceptibility_derivative_upper line 46
6. theorem OAI.Percolation.BenjaminiSchramm.hasDerivAt_realRootSusceptibility line 70
7. theorem OAI.Percolation.BenjaminiSchramm.rootSusceptibility_derivative_upper line 85