OAI/Probability/StrongRayleigh/AsymptoticReadout.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336AdditiveD139.binaryReadout line 14
  2. def OAI.Problem336AdditiveD139.asymptoticReadout line 18
  3. theorem OAI.Problem336AdditiveD139.measurable_binaryReadout line 21
  4. theorem OAI.Problem336AdditiveD139.binaryReadout_eq_of_tendsto line 30
  5. theorem OAI.Problem336AdditiveD139.measurable_asymptoticReadout line 51
  6. theorem OAI.Problem336AdditiveD139.asymptoticReadout_eq_of_tendsto line 58
  7. theorem OAI.Problem336AdditiveD139.asymptoticReadout_leftTranslate line 64
  8. theorem OAI.Problem336AdditiveD139.asymptoticReadout_ae_eq line 69
  9. theorem OAI.Problem336AdditiveD139.map_asymptoticReadout_of_reference line 76
  10. theorem OAI.Problem336AdditiveD139.hasEquivariantIIDFactor_of_asymptotic_observations line 91