OAI/Analysis/Conductivity/Fourier/AnalyticDerivativeBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ScalarConductivity.analyticAt_of_factorial_bound line 12
2. lemma OAI.ScalarConductivity.RadialMeanOn.linearIsometry line 121
3. lemma OAI.ScalarConductivity.RadialMeanOn.iterated line 129
4. lemma OAI.ScalarConductivity.RadialMeanOn.iterated_bound line 143
5. lemma OAI.ScalarConductivity.RadialMeanOn.factorial_bound line 172
6. lemma OAI.ScalarConductivity.RadialMeanOn.analyticAt line 209