OAI/Probability/SKGap/Localization/Magnetization.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGapCutoff.one_add_pow_le_exp line 10
  2. lemma OAI.SKGapCutoff.kernel_apply line 15
  3. lemma OAI.SKGapCutoff.generator_mul line 29
  4. def OAI.SKGapCutoff.magnetization line 39
  5. def OAI.SKGapCutoff.plusSpin line 41
  6. lemma OAI.SKGapCutoff.magnetization_plus line 43
  7. lemma OAI.SKGapCutoff.character_singleton line 46
  8. lemma OAI.SKGapCutoff.halfDiff_magnetization line 49
  9. lemma OAI.SKGapCutoff.generator_zero_magnetization line 54
  10. def OAI.SKGapCutoff.centeredMagnetizationSq line 60
  11. lemma OAI.SKGapCutoff.generator_zero_centeredMagnetizationSq line 63
  12. lemma OAI.SKGapCutoff.semigroup_zero_magnetization line 84
  13. lemma OAI.SKGapCutoff.semigroup_zero_centeredMagnetizationSq line 90
  14. lemma OAI.SKGapCutoff.pow_apply_of_eigenvector line 98
  15. lemma OAI.SKGapCutoff.attempt_pow_zero_magnetization line 105
  16. lemma OAI.SKGapCutoff.attempt_pow_zero_centeredMagnetizationSq line 113
  17. lemma OAI.SKGapCutoff.uniform_magnetization_second_moment line 122
  18. lemma OAI.SKGapCutoff.totalVariation_nonneg line 137
  19. lemma OAI.SKGapCutoff.totalVariation_le_one line 140
  20. lemma OAI.SKGapCutoff.event_difference_le_totalVariation line 151
  21. lemma OAI.SKGapCutoff.totalVariation_lower_from_quadratic_test line 165
  22. lemma OAI.SKGapCutoff.quadratic_centered_identity line 199
  23. lemma OAI.SKGapCutoff.continuous_zero_variance line 210
  24. lemma OAI.SKGapCutoff.discrete_zero_variance line 232
  25. lemma OAI.SKGapCutoff.continuous_zero_lower line 264
  26. lemma OAI.SKGapCutoff.exp_neg_inv_le_one_sub_inv line 295
  27. lemma OAI.SKGapCutoff.discrete_zero_lower line 309
  28. lemma OAI.SKGapCutoff.worstContinuous_nonneg line 353
  29. lemma OAI.SKGapCutoff.worstDiscrete_nonneg line 360
  30. lemma OAI.SKGapCutoff.worstContinuous_le_one line 367
  31. lemma OAI.SKGapCutoff.worstDiscrete_le_one line 374
  32. lemma OAI.SKGapCutoff.worstContinuous_zero_lower line 381
  33. lemma OAI.SKGapCutoff.worstDiscrete_zero_lower line 388
  34. lemma OAI.SKGapCutoff.worstContinuous_zero_upper line 396
  35. lemma OAI.SKGapCutoff.worstDiscrete_zero_upper line 410