OAI/Analysis/HardSphere/Geometry/ExpWeightedMultiplier.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.expWeightedMultiplier line 32
  2. lemma OAI.HardSphere.expWeightedMultiplier_apply line 36
  3. lemma OAI.HardSphere.expWeightedMultiplier_real line 41
  4. lemma OAI.HardSphere.expWeightedMultiplier_norm_sq line 45
  5. lemma OAI.HardSphere.expWeightedMultiplier_partial_sq line 51
  6. lemma OAI.HardSphere.expWeightedMultiplier_gradient line 66
  7. lemma OAI.HardSphere.SmoothMultiplier.error_integrable line 76
  8. lemma OAI.HardSphere.SmoothMultiplier.error_integral line 86
  9. lemma OAI.HardSphere.SmoothMultiplier.weighted_norm_integral line 91
  10. lemma OAI.HardSphere.expWeightedMultiplier_mass line 98
  11. lemma OAI.HardSphere.smoothWeightedCount_exp_integrable line 106
  12. lemma OAI.HardSphere.expWeightedMultiplier_defect line 125
  13. lemma OAI.HardSphere.weighted_count_penalty line 145
  14. lemma OAI.HardSphere.exp_neg_one_mul_exp_one line 170
  15. lemma OAI.HardSphere.exp_one_mul_exp_neg_one line 172
  16. lemma OAI.HardSphere.smoothWeightedCount_lower_for_penalty line 174
  17. lemma OAI.HardSphere.weightedSiteCount_le_smooth line 180
  18. lemma OAI.HardSphere.expWeightedMultiplier_weight_integrable line 186
  19. lemma OAI.HardSphere.expWeightedMultiplier_weight_lower line 193