OAI/Probability/GaussianRegression/Smoothing.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Projection smoothing, Gaussian noise, and bounds under weak limits.

  1. def OAI.NoiselessRegression.projectionSmoothing line 24
  2. lemma OAI.NoiselessRegression.measurable_projectionSmoothing line 28
  3. lemma OAI.NoiselessRegression.projectionSmoothing_pow line 34
  4. theorem OAI.NoiselessRegression.projectionSmoothing_moment line 50
  5. lemma OAI.NoiselessRegression.measure_pi_withDensity line 79
  6. lemma OAI.NoiselessRegression.pi_gaussian_map_scale line 105
  7. lemma OAI.NoiselessRegression.pi_gaussian_withDensity line 113
  8. lemma OAI.NoiselessRegression.lintegral_gaussian_shift_scale line 123
  9. lemma OAI.NoiselessRegression.withDensity_apply_le_moment line 149
  10. lemma OAI.NoiselessRegression.map_apply_open_le_of_tendsto line 171
  11. lemma OAI.NoiselessRegression.ennreal_rpow_iInf line 210
  12. lemma OAI.NoiselessRegression.measure_apply_le_of_isOpen line 214