OAI/Probability/GaussianRegression/Stream.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Sequential routing and continuation mass propagation.

  1. lemma OAI.NoiselessRegression.measurable_select line 25
  2. lemma OAI.NoiselessRegression.lintegral_pi_cons line 31
  3. def OAI.NoiselessRegression.streamRoute line 46
  4. lemma OAI.NoiselessRegression.measurable_streamRoute line 52
  5. def OAI.NoiselessRegression.continuation line 68
  6. lemma OAI.NoiselessRegression.measurable_continuation line 73
  7. lemma OAI.NoiselessRegression.continuation_le_one line 84
  8. lemma OAI.NoiselessRegression.continuation_unroll line 95
  9. def OAI.NoiselessRegression.streamFactor line 121
  10. lemma OAI.NoiselessRegression.streamFactor_ne_top line 125
  11. lemma OAI.NoiselessRegression.one_le_streamFactor line 129
  12. lemma OAI.NoiselessRegression.PolynomialMass.mono line 135
  13. lemma OAI.NoiselessRegression.continuation_mass_bound line 139
  14. lemma OAI.NoiselessRegression.fin_tail_snoc line 194
  15. lemma OAI.NoiselessRegression.streamRoute_snoc line 201
  16. lemma OAI.NoiselessRegression.lintegral_pi_prefix line 214