OAI/Analysis/HardSphere/Comparison/LaplaceIntegrand.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.semigroup_increment_bound line 18
  2. lemma OAI.HardSphere.semigroup_continuousOn line 40
  3. lemma OAI.HardSphere.semigroup_clamped_continuous line 56
  4. def OAI.HardSphere.laplaceIntegrand line 64
  5. lemma OAI.HardSphere.laplaceIntegrand_continuous line 67
  6. lemma OAI.HardSphere.laplaceIntegrand_integrable line 75
  7. def OAI.HardSphere.semigroupLaplace line 86
  8. lemma OAI.HardSphere.integral_Ioi_add line 89
  9. lemma OAI.HardSphere.semigroupLaplace_norm_le line 100
  10. lemma OAI.HardSphere.semigroupLaplace_shift line 115
  11. lemma OAI.HardSphere.semigroupLaplace_project line 142
  12. lemma OAI.HardSphere.semigroupLaplace_difference_tendsto line 149
  13. lemma OAI.HardSphere.semigroupLaplace_norm_sub_le line 181
  14. lemma OAI.HardSphere.laplaceIntegrand_eq_complex line 231
  15. lemma OAI.HardSphere.semigroupLaplace_difference_tendsto_complex line 235