OAI/Probability/SKGap/Localization/ScalarVariance.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.scalarVariance line 29
  2. lemma OAI.SKGapCutoff.scalarVariance_pos line 31
  3. lemma OAI.SKGapCutoff.scalarVariance_le_one line 34
  4. lemma OAI.SKGapCutoff.scalarVariance_eq line 38
  5. lemma OAI.SKGapCutoff.tanh_hasDerivAt line 45
  6. lemma OAI.SKGapCutoff.tanh_lipschitz line 53
  7. lemma OAI.SKGapCutoff.scalarVariance_lipschitz line 61
  8. lemma OAI.SKGapCutoff.tanh_linear_remainder line 72
  9. lemma OAI.SKGapCutoff.cosh_le_exp_abs line 89
  10. lemma OAI.SKGapCutoff.cosh_shift_le line 95
  11. lemma OAI.SKGapCutoff.sinh_abs_le line 107
  12. lemma OAI.SKGapCutoff.tanh_difference_eq line 118
  13. lemma OAI.SKGapCutoff.tanh_difference_variance_le line 123
  14. lemma OAI.SKGapCutoff.field_flip_general line 139
  15. lemma OAI.SKGapCutoff.halfDiff_as_flip line 145
  16. lemma OAI.SKGapCutoff.abs_spin_eq_one line 154
  17. lemma OAI.SKGapCutoff.abs_field_change line 157
  18. lemma OAI.SKGapCutoff.influence_error_le line 163
  19. lemma OAI.SKGapCutoff.influence_variance_le line 179
  20. lemma OAI.SKGapCutoff.siteVariance_sq_le_jumpWeight line 191
  21. lemma OAI.SKGapCutoff.influence_weighted_entry_le line 208
  22. lemma OAI.SKGapCutoff.influence_weighted_row_le line 227
  23. lemma OAI.SKGapCutoff.influence_error_quadratic_le line 236
  24. lemma OAI.SKGapCutoff.influence_quadratic_le line 271