OAI/Analysis/HardSphere/Geometry/GeneratorScalar.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.heatScalar_eq_exp line 24
  2. def OAI.HardSphere.generatorScalar line 31
  3. lemma OAI.HardSphere.generatorScalar_bounds line 33
  4. lemma OAI.HardSphere.generatorScalar_range_error line 51
  5. def OAI.HardSphere.generatorOperator line 90
  6. lemma OAI.HardSphere.generatorScalar_continuous line 93
  7. lemma OAI.HardSphere.generatorOperator_eq line 97
  8. lemma OAI.HardSphere.generatorOperator_norm_le line 111
  9. lemma OAI.HardSphere.one_sub_positive_contraction_norm_le line 119
  10. lemma OAI.HardSphere.generatorOperator_range_error line 131
  11. lemma OAI.HardSphere.generatorOperator_tendsto line 147
  12. lemma OAI.HardSphere.heat_difference_resolvent_tendsto line 168