OAI/NumberTheory/Ostmann/Construction/LogCellCalculus.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.realLogCellWeight line 10
2. def OAI.Ostmann.Construction.realLogCellDerivative line 13
3. lemma OAI.Ostmann.Construction.realLogCellWeight_hasDerivAt line 16
4. lemma OAI.Ostmann.Construction.realLogCellWeight_continuousOn line 28
5. lemma OAI.Ostmann.Construction.realLogCellDerivative_continuousOn line 33
6. lemma OAI.Ostmann.Construction.realLogCellWeight_endpoints line 46
7. lemma OAI.Ostmann.Construction.realLogCellWeight_integral line 55