OAI/Probability/FreeIsing/Gaussian/ComponentSignalAttenuation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.ComponentSignalAttenuation.posteriorMean line 16
  2. theorem OAI.Problem367.ComponentSignalAttenuation.measurable_posteriorMean line 23
  3. theorem OAI.Problem367.ComponentSignalAttenuation.posteriorMean_abs_le_one line 28
  4. theorem OAI.Problem367.ComponentSignalAttenuation.posteriorMean_flip_ae line 36
  5. def OAI.Problem367.ComponentSignalAttenuation.posteriorLaw line 70
  6. theorem OAI.Problem367.ComponentSignalAttenuation.posteriorLaw_probability line 74
  7. theorem OAI.Problem367.ComponentSignalAttenuation.posteriorLaw_abs_le_one line 81
  8. theorem OAI.Problem367.ComponentSignalAttenuation.posteriorLaw_neg_invariant line 87
  9. theorem OAI.Problem367.ComponentSignalAttenuation.posteriorLaw_information_lower line 98
  10. def OAI.Problem367.ComponentSignalAttenuation.lossCoefficient line 111
  11. theorem OAI.Problem367.ComponentSignalAttenuation.lossCoefficient_pos line 113
  12. theorem OAI.Problem367.ComponentSignalAttenuation.lossCoefficient_le_half line 117
  13. theorem OAI.Problem367.ComponentSignalAttenuation.integral_tilted_posteriorLaw_attenuation_le line 120