OAI/Probability/SKGap/Posterior/GaussianChannel.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.channelReference line 13
  2. instance OAI.SKGap.channelReference_probability line 14
  3. def OAI.SKGap.gaussianChannelLikelihood line 18
  4. def OAI.SKGap.gaussianChannelDensity line 21
  5. def OAI.SKGap.gaussianChannelLaw line 24
  6. lemma OAI.SKGap.channel_linear_exp_integrable line 27
  7. lemma OAI.SKGap.channel_linear_exp_integral line 32
  8. lemma OAI.SKGap.gaussianChannelLikelihood_integrable line 42
  9. lemma OAI.SKGap.gaussianChannelLikelihood_integral line 51
  10. lemma OAI.SKGap.gaussianChannelDensity_pos line 63
  11. lemma OAI.SKGap.gaussianChannelDensity_continuous line 67
  12. lemma OAI.SKGap.gaussianChannelDensity_integrable line 72
  13. lemma OAI.SKGap.gaussianChannelDensity_integral line 76
  14. lemma OAI.SKGap.gaussianChannelLaw_probability line 82
  15. lemma OAI.SKGap.weight_field_shift line 90
  16. lemma OAI.SKGap.gaussianChannelDensity_partition line 95
  17. lemma OAI.SKGap.gaussianChannel_posterior_identity line 112
  18. lemma OAI.SKGap.gaussianChannel_mass_mean line 125