OAI/Probability/FreeIsing/Gaussian/NoiseSlope.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.ae_tendsto_zero_of_tail_tsum_ne_top line 12
  2. theorem OAI.Problem367.ae_tendsto_zero_of_summable_tail line 27
  3. theorem OAI.Problem367.ae_tendsto_zero_of_exp_tail line 35
  4. theorem OAI.Problem367.ae_all_tendsto_zero_of_exp_tail line 47
  5. theorem OAI.Problem367.subgaussian_abs_tail line 54
  6. theorem OAI.Problem367.ae_tendsto_div_succ_zero_of_subgaussian line 68
  7. theorem OAI.Problem367.hasSubgaussianMGF_of_hasLaw_gaussian line 92
  8. theorem OAI.Problem367.ae_brownian_div_succ_tendsto_zero line 103
  9. theorem OAI.Problem367.ae_brownian_div_nat_tendsto_zero line 112
  10. theorem OAI.Problem367.ae_all_brownian_div_nat_tendsto_zero line 119
  11. theorem OAI.Problem367.ae_brownian_signal_recovery line 124