OAI/Probability/SKGap/Brownian/PathBiasBase.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.ComplexMatrix.continuous_schwartzMatrix_comp line 13
  2. lemma OAI.SKGap.ComplexMatrix.continuous_truncatedK_comp line 30
  3. lemma OAI.SKGap.continuous_realTruncatedK_comp line 51
  4. lemma OAI.SKGap.continuousOn_expected_realTruncatedK line 72
  5. lemma OAI.SKGap.realTruncatedK_zero_diagonal line 91
  6. lemma OAI.SKGap.power_exponential_bound line 101
  7. lemma OAI.SKGap.exponential_tail_absorptions line 115
  8. def OAI.SKGap.loopErrorConstantOne line 161
  9. def OAI.SKGap.loopErrorConstantTwo line 164
  10. lemma OAI.SKGap.loopErrorConstants_nonneg line 167
  11. lemma OAI.SKGap.loop_error_one_absorption line 173
  12. lemma OAI.SKGap.loop_error_two_absorption line 187
  13. lemma OAI.SKGap.continuous_no_exit line 204
  14. lemma OAI.SKGap.weighted_abs_sum_le line 227
  15. lemma OAI.SKGap.loop_local_control line 236
  16. lemma OAI.SKGap.loop_global_control line 300
  17. lemma OAI.SKGap.exists_schwartz_inverse line 349
  18. lemma OAI.SKGap.schwartz_inverse_fourier_moments line 388
  19. lemma OAI.SKGap.schwartz_fourier_inverse line 392