OAI/Probability/SphericalField/Control/Independence.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SphericalPerceptron.indep_eventuallyMeasurable_left line 16
  2. lemma OAI.SphericalPerceptron.nullSigma_le_eventuallyMeasurable line 24
  3. def OAI.SphericalPerceptron.rawBrownianSigma line 31
  4. lemma OAI.SphericalPerceptron.rawBrownianSigma_le line 35
  5. lemma OAI.SphericalPerceptron.rawBrownianSigma_le_past_comap line 40
  6. lemma OAI.SphericalPerceptron.usualBrownianSigma_le_ae_raw line 48
  7. lemma OAI.SphericalPerceptron.brownian_future_indep_raw line 54
  8. lemma OAI.SphericalPerceptron.brownian_future_indep_usual_earlier line 62
  9. lemma OAI.SphericalPerceptron.indep_setIntegral_eq_mul_null line 71
  10. lemma OAI.SphericalPerceptron.indep_comap_of_ae_tendsto line 91
  11. lemma OAI.SphericalPerceptron.brownian_increment_indep_usual line 116
  12. def OAI.SphericalPerceptron.clipControl line 135
  13. lemma OAI.SphericalPerceptron.progressive_clipControl line 138
  14. lemma OAI.SphericalPerceptron.abs_clip_le line 143
  15. lemma OAI.SphericalPerceptron.clip_cost_gain line 147
  16. lemma OAI.SphericalPerceptron.clip_sq_le line 160
  17. lemma OAI.SphericalPerceptron.pathControlCost_clip_le line 165