OAI/Probability/Renewal/LocalInversion.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HoneycombLocal.localIntegrand line 11
  2. lemma OAI.HoneycombLocal.localIntegrand_eq line 15
  3. lemma OAI.HoneycombLocal.continuous_localIntegrand line 26
  4. lemma OAI.HoneycombLocal.norm_localIntegrand line 31
  5. lemma OAI.HoneycombLocal.scaled_inversion line 36
  6. def OAI.HoneycombLocal.gaussianIntegrand line 46
  7. lemma OAI.HoneycombLocal.continuous_gaussianIntegrand line 49
  8. lemma OAI.HoneycombLocal.gaussianIntegrand_re line 53
  9. lemma OAI.HoneycombLocal.gaussian_core_lower line 61
  10. lemma OAI.HoneycombLocal.local_core_error line 91
  11. lemma OAI.HoneycombLocal.fourier_tail_bound line 124
  12. lemma OAI.HoneycombLocal.local_lower_of_envelope line 150