OAI/Combinatorics/UniformKServer/LogPrimitive.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformKServer.LogPrimitive.primitive line 9
  2. def OAI.UniformKServer.LogPrimitive.Contract line 12
  3. def OAI.UniformKServer.LogPrimitive.J line 19
  4. def OAI.UniformKServer.LogPrimitive.w line 20
  5. theorem OAI.UniformKServer.LogPrimitive.log_recip_top line 22
  6. theorem OAI.UniformKServer.LogPrimitive.J_continuous line 25
  7. theorem OAI.UniformKServer.LogPrimitive.w_nonneg line 45
  8. theorem OAI.UniformKServer.LogPrimitive.J_derivative line 49
  9. theorem OAI.UniformKServer.LogPrimitive.w_integrable line 63
  10. theorem OAI.UniformKServer.LogPrimitive.integrand_integrable line 71
  11. theorem OAI.UniformKServer.LogPrimitive.slope_atBot line 97
  12. theorem OAI.UniformKServer.LogPrimitive.generic_contract line 113
  13. theorem OAI.UniformKServer.LogPrimitive.powlog_zero line 171
  14. theorem OAI.UniformKServer.LogPrimitive.log_recip_continuousAt line 176
  15. theorem OAI.UniformKServer.LogPrimitive.regular_lower line 182
  16. theorem OAI.UniformKServer.LogPrimitive.marked_lower line 191
  17. theorem OAI.UniformKServer.LogPrimitive.regular_contract line 202
  18. theorem OAI.UniformKServer.LogPrimitive.marked_contract line 221