OAI/Probability/GaussianRegression/Projection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Exact noiseless projection laws and completed-event bounds.

  1. def OAI.NoiselessRegression.matrixLabelReference line 23
  2. def OAI.NoiselessRegression.projectionLaw line 26
  3. def OAI.NoiselessRegression.gaussianCoupling line 30
  4. def OAI.NoiselessRegression.noisyObservation line 35
  5. lemma OAI.NoiselessRegression.measurable_noisyObservation line 39
  6. lemma OAI.NoiselessRegression.gaussianCoupling_map_noisyObservation_zero line 44
  7. lemma OAI.NoiselessRegression.gaussianCoupling_map_noisyObservation line 58
  8. lemma OAI.NoiselessRegression.matrixLabelReference_outerRegular line 82
  9. lemma OAI.NoiselessRegression.tendsto_noisyObservation line 88
  10. theorem OAI.NoiselessRegression.projectionLaw_set_bound line 98