OAI/Probability/FreeIsing/Gaussian/FiniteSignalInformation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.finiteSignalField line 12
  2. theorem OAI.Problem367.finiteSignalField_le line 15
  3. theorem OAI.Problem367.finiteSignalField_singleton line 19
  4. theorem OAI.Problem367.finiteSignalField_insert line 23
  5. theorem OAI.Problem367.indep_finiteSignalField_of_not_mem line 28
  6. theorem OAI.Problem367.condExp_spin_sup_eq_binaryFusion line 36
  7. theorem OAI.Problem367.abs_condExp_spin_sup_lt_one line 68
  8. theorem OAI.Problem367.abs_condExp_spin_finiteSignalField_lt_one line 82
  9. def OAI.Problem367.spinInformation line 104
  10. theorem OAI.Problem367.spinInformation_sup_le_add line 108
  11. theorem OAI.Problem367.spinInformation_sup_le_sub_loss line 139
  12. theorem OAI.Problem367.spinInformation_finiteSignalField_union_le line 187
  13. theorem OAI.Problem367.spinInformation_finiteSignalField_le_sum line 208
  14. theorem OAI.Problem367.spinInformation_finiteSignalField_le_sum_sub_loss line 227