OAI/Analysis/SymmetricDomains/TransverseCutoffs.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Release061.Wiener.vanishingFactor_real line 20
  2. def OAI.Release061.Wiener.vanishingReal line 26
  3. lemma OAI.Release061.Wiener.vanishingReal_eval line 28
  4. lemma OAI.Release061.Wiener.vanishingReal_nonneg line 40
  5. lemma OAI.Release061.Wiener.coeff_zero_real line 48
  6. def OAI.Release061.Wiener.realMean line 60
  7. lemma OAI.Release061.Wiener.coeff_zero_eq_realMean line 63
  8. lemma OAI.Release061.Wiener.localized_division line 68
  9. lemma OAI.Release061.Wiener.localized_radial_expansion line 81
  10. theorem OAI.Release061.Wiener.exists_transverse_cutoffs line 98