OAI/Probability/SKGap/Localization/PhiBounds.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGap.Stein.phi_zero_diagonal line 13
  2. lemma OAI.SKGap.Stein.phi_zero_le_one line 16
  3. lemma OAI.SKGap.Stein.weight_le line 29
  4. lemma OAI.SKGap.Stein.continuous_integrand line 40
  5. lemma OAI.SKGap.Stein.phi_le_exp line 44
  6. lemma OAI.SKGap.Stein.abs_sinh_le_cosh line 57
  7. lemma OAI.SKGap.Stein.numerator_pos line 62
  8. lemma OAI.SKGap.Stein.abs_numeratorZ_le line 67
  9. lemma OAI.SKGap.Stein.phiZ_relative_bound line 83
  10. def OAI.SKGap.Stein.numeratorZZ line 93
  11. lemma OAI.SKGap.Stein.numeratorZ_hasDerivAt line 95
  12. lemma OAI.SKGap.Stein.numeratorZZ_nonneg line 107
  13. lemma OAI.SKGap.Stein.numeratorZZ_le line 111
  14. def OAI.SKGap.Stein.logSlope line 122
  15. def OAI.SKGap.Stein.logSlopeZ line 124
  16. lemma OAI.SKGap.Stein.logSlope_eq line 127
  17. lemma OAI.SKGap.Stein.logSlope_hasDerivAt line 132
  18. lemma OAI.SKGap.Stein.logSlopeZ_bound line 141
  19. lemma OAI.SKGap.Stein.logSlope_lipschitz line 153
  20. lemma OAI.SKGap.Stein.logSlope_diagonal line 160
  21. theorem OAI.SKGap.Stein.logSlope_near_diagonal line 164