OAI/Probability/FreeIsing/Gaussian/BinarySignalDensity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.spin_measure_singleton_eq_mean line 17
  2. theorem OAI.Problem367.condDistrib_spin_singleton_of_calibration line 32
  3. theorem OAI.Problem367.condDistrib_signal_eq_withDensity_of_calibration line 50
  4. theorem OAI.Problem367.ae_abs_le_one_of_spin_calibration line 82
  5. theorem OAI.Problem367.calibrated_signal_product_likelihood line 96
  6. theorem OAI.Problem367.calibrated_condIndep_fusion_quadratic_loss line 123