OAI/Probability/SKGap/Localization/CoordinateLipschitz.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.CoordinateLipschitz line 20
  2. lemma OAI.SKGapCutoff.CoordinateLipschitz.lipschitz line 23
  3. lemma OAI.SKGapCutoff.memLp_gaussian_pi_id line 35
  4. lemma OAI.SKGapCutoff.memLp_gaussian_pi_of_lipschitz line 42
  5. lemma OAI.SKGapCutoff.memLp_gaussian_real_of_lipschitz line 53
  6. lemma OAI.SKGapCutoff.gaussian_lipschitz_variance line 65
  7. lemma OAI.SKGapCutoff.coordinateLipschitz_cons_real line 90
  8. lemma OAI.SKGapCutoff.coordinateLipschitz_integral_cons line 97
  9. lemma OAI.SKGapCutoff.integral_gaussian_fin_succ line 117
  10. lemma OAI.SKGapCutoff.gaussian_coordinate_variance_fin line 136
  11. lemma OAI.SKGapCutoff.gaussian_coordinate_variance line 175
  12. lemma OAI.SKGapCutoff.abs_upperCoefficient_le_one line 191
  13. lemma OAI.SKGapCutoff.energy_sampled_diff_le line 198
  14. lemma OAI.SKGapCutoff.log_partition_sampled_le line 208
  15. lemma OAI.SKGapCutoff.coordinateLipschitz_log_partition line 226
  16. lemma OAI.SKGapCutoff.memLp_log_partition line 236
  17. lemma OAI.SKGapCutoff.variance_log_partition_le line 240
  18. lemma OAI.SKGapCutoff.integral_sq_cauchy line 252
  19. lemma OAI.SKGapCutoff.second_moment_lower_probability line 279
  20. lemma OAI.SKGapCutoff.partition_half_mean_probability line 309
  21. lemma OAI.SKGapCutoff.mean_ge_of_upper_event line 341
  22. lemma OAI.SKGapCutoff.integral_log_partition_le_log_mean line 368
  23. lemma OAI.SKGapCutoff.integral_log_partition_ge_log_mean line 393
  24. lemma OAI.SKGapCutoff.square_integral_shift line 418
  25. lemma OAI.SKGapCutoff.second_moment_log_partition_centered_le line 429