OAI/Probability/SKGap/Localization/ScalarEmpirical.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.scalarEmpirical line 31
  2. def OAI.SKGap.scalarIntegrand line 33
  3. lemma OAI.SKGap.scalarA_empirical line 37
  4. lemma OAI.SKGap.empirical_scalar_cauchy line 44
  5. lemma OAI.SKGap.scalar_empirical_quadratic_envelope line 53
  6. lemma OAI.SKGap.scalar_empirical_parameter_bounds line 68
  7. theorem OAI.SKGap.scalar_integrand_envelope line 86
  8. theorem OAI.SKGap.scalar_integrand_tail line 100
  9. lemma OAI.SKGap.empirical_momentBall line 123
  10. def OAI.SKGap.scalarBox line 134
  11. lemma OAI.SKGap.isCompact_scalarBox line 137
  12. lemma OAI.SKGap.scalar_compact_nonpositive line 141
  13. theorem OAI.SKGap.scalar_uniform_tail line 161
  14. lemma OAI.SKGap.lintegral_split_le line 183
  15. theorem OAI.SKGap.scalar_unrestricted_rate line 190