OAI/Probability/StrongRayleigh/FiniteMarginalObservation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Problem336AdditiveD139.finite_field_sum_restrict line 15
  2. lemma OAI.Problem336AdditiveD139.integral_finiteMarginal line 24
  3. theorem OAI.Problem336AdditiveD139.finiteFieldMean_eq_tiltMean_finiteMarginal line 33
  4. def OAI.Problem336AdditiveD139.finiteObservationField line 76
  5. def OAI.Problem336AdditiveD139.finiteObservationDrift line 80
  6. theorem OAI.Problem336AdditiveD139.finiteObservationDrift_eq_finiteFieldMean line 86
  7. theorem OAI.Problem336AdditiveD139.finiteObservationDrift_mem_Icc line 95
  8. theorem OAI.Problem336AdditiveD139.measurable_finiteObservationDrift line 101
  9. theorem OAI.Problem336AdditiveD139.finiteObservationDrift_translate line 110
  10. theorem OAI.Problem336AdditiveD139.finiteObservationField_abs_sub_le line 118
  11. theorem OAI.Problem336AdditiveD139.finiteObservationDrift_response_of_finite_response line 128
  12. theorem OAI.Problem336AdditiveD139.finiteObservationDrift_eq_tiltMean_of_mem line 140
  13. theorem OAI.Problem336AdditiveD139.finiteFieldMean_zero_field line 152
  14. theorem OAI.Problem336AdditiveD139.finiteObservationDrift_zero_zero line 158