OAI/Analysis/AncientFlat/Profile/ProfileFamilies.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FlatSimilarity.profileAf line 11
  2. def OAI.FlatSimilarity.profileBf line 12
  3. lemma OAI.FlatSimilarity.profile_smooth line 14
  4. def OAI.ProfileDecay.bump line 35
  5. def OAI.ProfileDecay.q line 37
  6. lemma OAI.ProfileDecay.q_pos line 38
  7. lemma OAI.ProfileDecay.q_smooth line 46
  8. lemma OAI.ProfileDecay.q_eq line 52
  9. def OAI.ProfileDecay.arg line 57
  10. def OAI.ProfileDecay.familyA line 58
  11. def OAI.ProfileDecay.familyB line 59
  12. lemma OAI.ProfileDecay.arg_smooth line 61
  13. lemma OAI.ProfileDecay.arg_nonneg line 63
  14. lemma OAI.ProfileDecay.families_smooth line 64
  15. lemma OAI.ProfileDecay.arg_even line 73
  16. lemma OAI.ProfileDecay.arg_zero line 74
  17. lemma OAI.ProfileDecay.families_decay line 75