OAI/Analysis/HardSphere/Bridges/WienerGaussian.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.Wiener.norm_tent_combination_le line 15
  2. lemma OAI.HardSphere.Wiener.dual_tent_sum_abs_le line 30
  3. lemma OAI.HardSphere.Wiener.dual_tent_sum_sq_le line 50
  4. lemma OAI.HardSphere.Wiener.amplitude_sq line 64
  5. lemma OAI.HardSphere.Wiener.dual_variance_summable line 69
  6. def OAI.HardSphere.Wiener.dualCoefficient line 77
  7. lemma OAI.HardSphere.Wiener.dual_partialPath_expansion line 81
  8. lemma OAI.HardSphere.Wiener.dual_partial_variance line 96
  9. lemma OAI.HardSphere.Wiener.dual_path_law line 102
  10. instance OAI.HardSphere.Wiener.wiener_isGaussian line 123
  11. theorem OAI.HardSphere.Wiener.wiener_exists_integrable_exp_sq line 130
  12. theorem OAI.HardSphere.Wiener.wiener_norm_gaussian_tail line 134