OAI/Probability/StrongRayleigh/WeightedLocalInnovation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem336AdditiveD139.WeightedLocalInnovation.signal line 18
  2. def OAI.Problem336AdditiveD139.WeightedLocalInnovation.drift line 21
  3. def OAI.Problem336AdditiveD139.WeightedLocalInnovation.correction line 25
  4. theorem OAI.Problem336AdditiveD139.WeightedLocalInnovation.posterior_sum line 29
  5. theorem OAI.Problem336AdditiveD139.WeightedLocalInnovation.correction_eq line 55
  6. theorem OAI.Problem336AdditiveD139.WeightedLocalInnovation.measurable_drift line 68
  7. theorem OAI.Problem336AdditiveD139.WeightedLocalInnovation.abs_drift_le line 75
  8. theorem OAI.Problem336AdditiveD139.WeightedLocalInnovation.intervalIntegrable_drift_coordinates line 85
  9. theorem OAI.Problem336AdditiveD139.WeightedLocalInnovation.correction_condExp_zero line 95
  10. def OAI.Problem336AdditiveD139.WeightedLocalInnovation.amplitude line 119
  11. def OAI.Problem336AdditiveD139.WeightedLocalInnovation.variance line 121
  12. def OAI.Problem336AdditiveD139.WeightedLocalInnovation.errorConstant line 124
  13. theorem OAI.Problem336AdditiveD139.WeightedLocalInnovation.amplitude_nonneg line 128
  14. theorem OAI.Problem336AdditiveD139.WeightedLocalInnovation.errorConstant_nonneg line 131
  15. theorem OAI.Problem336AdditiveD139.WeightedLocalInnovation.corrected_gaussian_characteristic_error line 135
  16. def OAI.Problem336AdditiveD139.WeightedLocalInnovation.noiseIncrement line 176
  17. def OAI.Problem336AdditiveD139.WeightedLocalInnovation.innovationIncrement line 180
  18. theorem OAI.Problem336AdditiveD139.WeightedLocalInnovation.innovationIncrement_eq line 186
  19. theorem OAI.Problem336AdditiveD139.WeightedLocalInnovation.innovation_characteristic_error line 198