OAI/Probability/StrongRayleigh/InnovationCorrection.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336AdditiveD139.InnovationCorrection.correction line 14
  2. theorem OAI.Problem336AdditiveD139.InnovationCorrection.integral_mem_unitInterval_scaled line 17
  3. theorem OAI.Problem336AdditiveD139.InnovationCorrection.abs_correction_le line 31
  4. theorem OAI.Problem336AdditiveD139.InnovationCorrection.correction_eq_integral line 42
  5. theorem OAI.Problem336AdditiveD139.InnovationCorrection.abs_sum_correction_le line 48
  6. def OAI.Problem336AdditiveD139.InnovationCorrection.innovation line 67
  7. theorem OAI.Problem336AdditiveD139.InnovationCorrection.innovation_sub_eq line 70
  8. theorem OAI.Problem336AdditiveD139.InnovationCorrection.sum_innovation_sub_eq line 80
  9. theorem OAI.Problem336AdditiveD139.InnovationCorrection.intervalIntegrable_of_measurable_unitInterval line 93
  10. theorem OAI.Problem336AdditiveD139.InnovationCorrection.measurable_intervalIntegral line 105
  11. theorem OAI.Problem336AdditiveD139.InnovationCorrection.measurable_correction line 114
  12. theorem OAI.Problem336AdditiveD139.InnovationCorrection.integrable_correction_pow line 119
  13. theorem OAI.Problem336AdditiveD139.InnovationCorrection.integrable_abs_correction_pow line 132
  14. theorem OAI.Problem336AdditiveD139.InnovationCorrection.measurable_sum_correction line 140
  15. theorem OAI.Problem336AdditiveD139.InnovationCorrection.integrable_sum_correction_pow line 148