OAI/Probability/SKGap/Localization/PreparationGrowth.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKGapCutoff.refreshRoughDefect_nonneg line 154
  2. lemma OAI.SKGapCutoff.refreshRough_vector_propagation line 165
  3. lemma OAI.SKGapCutoff.refreshField_flip line 196
  4. lemma OAI.SKGapCutoff.refreshField_abs_change line 201
  5. lemma OAI.SKGapCutoff.refreshInfluence_error_le line 207
  6. lemma OAI.SKGapCutoff.refreshInfluence_variance_le line 225
  7. lemma OAI.SKGapCutoff.refreshVariance_sq_le_jumpWeight line 236
  8. lemma OAI.SKGapCutoff.matrix_row_sq_le line 256
  9. lemma OAI.SKGapCutoff.refreshInfluence_weighted_entry_le line 265
  10. lemma OAI.SKGapCutoff.refreshInfluence_weighted_row_le line 284
  11. lemma OAI.SKGapCutoff.refreshInfluence_error_quadratic_le line 293
  12. lemma OAI.SKGapCutoff.refreshInfluence_quadratic_le line 333
  13. lemma OAI.SKGapCutoff.refreshRough_of_field_opNorm line 367
  14. lemma OAI.SKGapCutoff.refreshGradient_of_field_opNorm line 392
  15. lemma OAI.SKGapCutoff.refreshSemigroup_mono line 405
  16. lemma OAI.SKGapCutoff.refreshSemigroup_add line 412
  17. lemma OAI.SKGapCutoff.refreshJumpEnergy_le_gradient line 420
  18. lemma OAI.SKGapCutoff.exp_growth_integral line 431
  19. lemma OAI.SKGapCutoff.refreshVariance_from_gradient line 442
  20. lemma OAI.SKGapCutoff.gibbsVariance_moments line 476
  21. lemma OAI.SKGapCutoff.gibbsVariance_gradient_le line 490
  22. lemma OAI.SKGapCutoff.refreshGibbs_poincare_from_gradient line 503
  23. def OAI.SKGapCutoff.preparationGrowth line 524
  24. lemma OAI.SKGapCutoff.preparationGrowth_pos line 527
  25. lemma OAI.SKGapCutoff.refreshGradient_field_bound line 530
  26. theorem OAI.SKGapCutoff.preparation_poincare_field line 546