OAI/Probability/SKValue/GroundState/BlockCoeff.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValueG.hamCoeff_distance line 11
  2. def OAI.SKValueG.blockCoeff line 42
  3. lemma OAI.SKValueG.weighted_square_div_le line 47
  4. lemma OAI.SKValueG.blockCoeff_distance_le line 56
  5. lemma OAI.SKValueG.finiteMaximum_append_sum line 69
  6. lemma OAI.SKValueG.expected_max_block line 85
  7. lemma OAI.SKValueG.expectedMaximum_zero line 111
  8. lemma OAI.SKValueG.expectedMaximum_superadditive line 117
  9. lemma OAI.SKValueG.integrable_exp_linearProcess line 125
  10. lemma OAI.SKValueG.integral_exp_linearProcess line 130
  11. lemma OAI.SKValueG.integral_logPartition_upper line 139
  12. lemma OAI.SKValueG.upper_triangle_count_bound line 165
  13. lemma OAI.SKValueG.hamCoeff_variance_bound line 189
  14. lemma OAI.SKValueG.expectedMaximum_upper line 210
  15. theorem OAI.SKValueG.groundStateSequence_tendsto line 237