OAI/InformationTheory/BooleanNoise/PerspectiveCalculus.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LeanBlast.CourtadeKumar.logCorrectedPerspective line 13
2. def OAI.LeanBlast.CourtadeKumar.logCorrectedPerspectiveDeriv line 16
3. def OAI.LeanBlast.CourtadeKumar.logCorrectedPerspectiveSecondDeriv line 19
4. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_const_quotient line 22
5. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_logCorrectedPerspective line 27
6. theorem OAI.LeanBlast.CourtadeKumar.hasDerivAt_logCorrectedPerspectiveDeriv line 43
7. theorem OAI.LeanBlast.CourtadeKumar.continuousOn_logCorrectedPerspectiveDeriv line 57
8. theorem OAI.LeanBlast.CourtadeKumar.concaveOn_logCorrectedPerspective line 72