OAI/Probability/FreeIsing/Ising/ContinuousResponseAlgebra.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.IsingObservationFactor.continuousPosterior_variance_pos line 16
  2. theorem OAI.Problem367.IsingObservationFactor.firstWeight_mul_continuousRootCovariance line 21
  3. theorem OAI.Problem367.IsingObservationFactor.continuousRootCovariance_div_variance line 31
  4. theorem OAI.Problem367.IsingObservationFactor.continuousRootCovariance_square_tsum line 39
  5. theorem OAI.Problem367.IsingObservationFactor.secondWeight_mul_continuousRootCovariance_square_tsum line 46
  6. theorem OAI.Problem367.IsingObservationFactor.continuousRootCovariance_square_tsum_le_response line 55
  7. theorem OAI.Problem367.IsingObservationFactor.abs_continuousPosterior_mul_response_square_tsum_le line 66
  8. theorem OAI.Problem367.IsingObservationFactor.firstWeight_mul_stopped_continuousRootCovariance line 76
  9. theorem OAI.Problem367.IsingObservationFactor.firstWeight_stopped_mul_continuousRootCovariance_of_le line 84
  10. theorem OAI.Problem367.IsingObservationFactor.firstWeight_stopped_pullback_mul_continuousRootCovariance_of_le line 92
  11. theorem OAI.Problem367.IsingObservationFactor.firstWeight_stopped_copy_mul_continuousRootCovariance_of_le line 102