OAI/Probability/LogConcave/Complexity/KernelAnalyticNormalizedBudget.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.kernelAnalyticNormalizedBudget line 13
  2. lemma OAI.LogConcaveSampling.kernelAnalyticNormalizedBudget_nonneg line 18
  3. lemma OAI.LogConcaveSampling.kernelAnalyticBudget_normalized line 23
  4. def OAI.LogConcaveSampling.velocityNormalizedBudget line 40
  5. lemma OAI.LogConcaveSampling.velocityNormalizedBudget_nonneg line 46
  6. theorem OAI.LogConcaveSampling.velocityRmsBudget_normalized line 53
  7. lemma OAI.LogConcaveSampling.square_root_two_budget line 96
  8. def OAI.LogConcaveSampling.centerStateQuadratureEnvelope line 104
  9. def OAI.LogConcaveSampling.centerInitialEnvelope line 106
  10. def OAI.LogConcaveSampling.centerStateEnvelope line 109
  11. def OAI.LogConcaveSampling.centerMeanEnvelope line 113
  12. lemma OAI.LogConcaveSampling.centerStateQuadratureEnvelope_nonneg line 117
  13. lemma OAI.LogConcaveSampling.centerInitialEnvelope_nonneg line 121
  14. lemma OAI.LogConcaveSampling.centerStateEnvelope_nonneg line 124
  15. lemma OAI.LogConcaveSampling.centerMeanEnvelope_nonneg line 128
  16. lemma OAI.LogConcaveSampling.centeringStateQuadratureBudget_normalized line 133
  17. lemma OAI.LogConcaveSampling.centeringInitialBudget_normalized line 144
  18. lemma OAI.LogConcaveSampling.centeringPicardBudget_normalized line 155
  19. lemma OAI.LogConcaveSampling.centeringMeanBudget_normalized line 172
  20. def OAI.LogConcaveSampling.dimensionLog line 207
  21. lemma OAI.LogConcaveSampling.dimensionLog_nonneg line 209
  22. lemma OAI.LogConcaveSampling.dimensionLog_isBigO_log line 214
  23. lemma OAI.LogConcaveSampling.dimensionLog_pow_isLittleO line 230
  24. theorem OAI.LogConcaveSampling.polylog_power_absorb line 237
  25. def OAI.LogConcaveSampling.LogPowerRate line 265
  26. lemma OAI.LogConcaveSampling.dimensionLog_one_le line 268
  27. lemma OAI.LogConcaveSampling.LogPowerRate.congr line 275
  28. lemma OAI.LogConcaveSampling.LogPowerRate.mono line 279
  29. lemma OAI.LogConcaveSampling.LogPowerRate.const line 290
  30. lemma OAI.LogConcaveSampling.LogPowerRate.power line 295
  31. lemma OAI.LogConcaveSampling.LogPowerRate.log line 299
  32. lemma OAI.LogConcaveSampling.LogPowerRate.mul line 303
  33. lemma OAI.LogConcaveSampling.LogPowerRate.pow line 313
  34. lemma OAI.LogConcaveSampling.LogPowerRate.const_mul line 321
  35. lemma OAI.LogConcaveSampling.LogPowerRate.mul_const line 325
  36. lemma OAI.LogConcaveSampling.LogPowerRate.add line 329
  37. lemma OAI.LogConcaveSampling.LogPowerRate.of_le_abs line 342
  38. lemma OAI.LogConcaveSampling.LogPowerRate.eventually_small line 347
  39. lemma OAI.LogConcaveSampling.LogPowerRate.abs line 375
  40. lemma OAI.LogConcaveSampling.LogPowerRate.div_const line 378
  41. lemma OAI.LogConcaveSampling.LogPowerRate.of_le line 382
  42. lemma OAI.LogConcaveSampling.LogPowerRate.inv_power line 389
  43. lemma OAI.LogConcaveSampling.LogPowerRate.log_nat line 395
  44. lemma OAI.LogConcaveSampling.LogPowerRate.log_power line 405
  45. lemma OAI.LogConcaveSampling.logMeshLength_le_scale line 411
  46. lemma OAI.LogConcaveSampling.logMeshLength_rate line 422
  47. lemma OAI.LogConcaveSampling.terminalQuadratureWeight_rate line 435