OAI/Analysis/HardSphere/Cutoffs/Regularize.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ComplexRegularization.regularize line 14
  2. def OAI.ComplexRegularization.differential line 16
  3. lemma OAI.ComplexRegularization.smooth line 19
  4. lemma OAI.ComplexRegularization.zero line 27
  5. lemma OAI.ComplexRegularization.hasFDerivAt line 30
  6. lemma OAI.ComplexRegularization.sqroot_ge_norm line 44
  7. lemma OAI.ComplexRegularization.differential_apply_le line 47
  8. lemma OAI.ComplexRegularization.differential_le line 62
  9. lemma OAI.ComplexRegularization.fderiv_eq line 67
  10. lemma OAI.ComplexRegularization.tendsto_regularize line 70
  11. lemma OAI.ComplexRegularization.tendsto_differential line 78
  12. def OAI.HardSphere.regularization line 92
  13. def OAI.HardSphere.regularizationScale line 98
  14. lemma OAI.HardSphere.regularizationScale_pos line 100
  15. lemma OAI.HardSphere.tendsto_regularizationScale line 104
  16. lemma OAI.HardSphere.modulus_lipschitz line 107
  17. def OAI.HardSphere.modulusScalar line 113
  18. lemma OAI.HardSphere.coe_modulusScalar line 116
  19. lemma OAI.HardSphere.modulusCoefficient_meas line 120
  20. def OAI.HardSphere.modulusPartial line 133
  21. def OAI.HardSphere.modulusJet line 137
  22. lemma OAI.HardSphere.coe_modulusPartial line 140
  23. lemma OAI.HardSphere.tendsto_regularization_partial line 144
  24. lemma OAI.HardSphere.tendsto_regularization_scalar line 168
  25. lemma OAI.HardSphere.tendsto_regularization_jet line 188
  26. lemma OAI.HardSphere.modulusJet_mem_domain line 194
  27. lemma OAI.HardSphere.norm_modulusScalar line 200
  28. lemma OAI.HardSphere.energy_modulusJet_le line 208
  29. lemma OAI.HardSphere.bosonic_modulusScalar line 216
  30. lemma OAI.HardSphere.IsGroundVector.modulus line 229
  31. lemma OAI.HardSphere.IsGroundVector.energy_modulus line 236