OAI/Probability/StrongRayleigh/FiniteEndpointPosterior.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem336AdditiveD139.finiteFieldWeight_congr_on line 20
  2. lemma OAI.Problem336AdditiveD139.finiteFieldMean_congr_on line 29
  3. def OAI.Problem336AdditiveD139.endpointObservationField line 35
  4. def OAI.Problem336AdditiveD139.finiteEndpointMean line 39
  5. lemma OAI.Problem336AdditiveD139.measurable_endpointObservationField line 44
  6. lemma OAI.Problem336AdditiveD139.measurable_finiteEndpointMean line 55
  7. lemma OAI.Problem336AdditiveD139.finiteEndpointMean_restrict line 60
  8. theorem OAI.Problem336AdditiveD139.finiteBinary_condExp_of_field_densities line 69
  9. lemma OAI.Problem336AdditiveD139.endpoint_pi_dirac_zero line 107
  10. lemma OAI.Problem336AdditiveD139.gaussianEndpoint_shift_map line 122
  11. theorem OAI.Problem336AdditiveD139.finiteBinary_condExp_independentGaussian line 140
  12. lemma OAI.Problem336AdditiveD139.endpointObservationField_sum line 186
  13. lemma OAI.Problem336AdditiveD139.finiteEndpointMean_eq_tiltMean line 206
  14. theorem OAI.Problem336AdditiveD139.finiteEndpointMean_condExp line 217
  15. theorem OAI.Problem336AdditiveD139.finiteObservationDrift_condExp line 262