OAI/Probability/SKFluctuations/EventuallyNatPos.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Eventually Nat Pos.

  1. theorem OAI.SKFluctuations.eventually_nat_pos line 19
  2. theorem OAI.SKFluctuations.eventually_const_mul_rpow_le line 23
  3. theorem OAI.SKFluctuations.eventually_rpow_le_const_mul_rpow line 32
  4. theorem OAI.SKFluctuations.tendsto_nat_rpow_zero line 39
  5. theorem OAI.SKFluctuations.tendsto_const_div_nat_rpow line 48
  6. theorem OAI.SKFluctuations.augmentedSD_monomial_bounds line 59
  7. theorem OAI.SKFluctuations.augmentedSD_scale_of_window line 105
  8. theorem OAI.SKFluctuations.nat_rpow_sq line 128
  9. theorem OAI.SKFluctuations.augmentedSD_sq line 131
  10. theorem OAI.SKFluctuations.freeEnergySD_sq line 135
  11. theorem OAI.SKFluctuations.freeEnergySD_nonneg line 139
  12. theorem OAI.SKFluctuations.freeEnergySD_le_augmentedSD line 141
  13. theorem OAI.SKFluctuations.freeEnergySD_scale_of_window line 146
  14. theorem OAI.SKFluctuations.freeEnergyVariance_scale_of_window line 174
  15. theorem OAI.SKFluctuations.freeEnergy_smallball_tendsto_of_window line 195
  16. theorem OAI.SKFluctuations.freeEnergy_largetail_tendsto_of_window line 228
  17. theorem OAI.SKFluctuations.measurableSet_fluctuationEvent line 254
  18. theorem OAI.SKFluctuations.fluctuationEvent_tendsto_of_window line 259
  19. theorem OAI.SKFluctuations.main_of_positiveLaplaceWindow line 294
  20. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_standardGaussianPDF line 310
  21. theorem OAI.SKFluctuations.GaussianCalculus.integrable_standardGaussian_iff line 321
  22. theorem OAI.SKFluctuations.GaussianCalculus.standardGaussian_stein line 330
  23. theorem OAI.SKFluctuations.GaussianCalculus.standardGaussianVector_stein line 356
  24. def OAI.SKFluctuations.GaussianCalculus.ExpNormBounded line 390
  25. theorem OAI.SKFluctuations.GaussianCalculus.affine_norm_exp_bound line 393
  26. theorem OAI.SKFluctuations.GaussianCalculus.affine_coord_exp_bound line 404
  27. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.affine_integrable line 420
  28. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.affine_coord_integrable line 430
  29. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.exp_lipschitz line 445
  30. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.bdd_mul line 458
  31. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_gaussian_vector_affine line 474
  32. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_gaussian_vector_affine_heat line 509
  33. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_gaussian_vector_variance line 545
  34. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.continuous_gaussian_affine line 568
  35. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.continuous_gaussian_variance line 593
  36. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivWithinAt_gaussian_vector_variance_zero line 600
  37. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivWithinAt_gaussian_vector_variance line 635