OAI/Probability/SwitchChain/FixedBlockVariance.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem315.FixedBlockVariance.State line 15
  2. def OAI.Problem315.FixedBlockVariance.relabelPerm line 17
  3. def OAI.Problem315.FixedBlockVariance.move line 29
  4. def OAI.Problem315.FixedBlockVariance.key line 33
  5. theorem OAI.Problem315.FixedBlockVariance.key_move_eq line 36
  6. theorem OAI.Problem315.FixedBlockVariance.constant_of_move_invariant line 53
  7. def OAI.Problem315.FixedBlockVariance.rowSpace line 69
  8. theorem OAI.Problem315.FixedBlockVariance.rowSpace_invariant line 85
  9. theorem OAI.Problem315.FixedBlockVariance.local_energy_bound line 97
  10. theorem OAI.Problem315.FixedBlockVariance.centered_row_norm_bound line 121
  11. def OAI.Problem315.FixedBlockVariance.average line 130
  12. def OAI.Problem315.FixedBlockVariance.variance line 133
  13. theorem OAI.Problem315.FixedBlockVariance.sum_sub_average line 137
  14. theorem OAI.Problem315.FixedBlockVariance.average_sum line 146
  15. theorem OAI.Problem315.FixedBlockVariance.row_variance_bound line 151
  16. theorem OAI.Problem315.FixedBlockVariance.variance_sum_row_functions line 179