OAI/Probability/GaussianRegression/Rotational.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Fubini bounds and rotational lower bounds for sequential estimation.

  1. lemma OAI.NoiselessRegression.ae_fiber_aemeasurable line 23

    Also declared: OAI/Probability/GaussianReplacement/StreamSphere.lean:30 (same declaration text).

  2. lemma OAI.NoiselessRegression.prod_null_set_bound line 31

    Also declared: OAI/Probability/GaussianReplacement/StreamSphere.lean:38 (same declaration text).

  3. instance OAI.NoiselessRegression.sampleLaw_probability line 49

    Also declared: OAI/Probability/GaussianReplacement/StreamSphere.lean:56 (same declaration text).

  4. instance OAI.NoiselessRegression.uniformSphere_probability line 52

    Also declared: OAI/Probability/GaussianReplacement/StreamSphere.lean:59 (same declaration text).

  5. lemma OAI.NoiselessRegression.Learner.run_congr_labels line 57

    Also declared: OAI/Probability/GaussianReplacement/StreamBlock.lean:15 (same declaration text).

  6. lemma OAI.NoiselessRegression.Learner.estimate_congr_labels line 71

    Also declared: OAI/Probability/GaussianReplacement/StreamBlock.lean:29 (same declaration text).

  7. lemma OAI.NoiselessRegression.Learner.angularSuccess_nullMeasurable line 76

    Also declared: OAI/Probability/GaussianReplacement/StreamBlock.lean:34 (same declaration text).

  8. lemma OAI.NoiselessRegression.Learner.linear_success_bound line 86

    Also declared: OAI/Probability/GaussianReplacement/StreamBlock.lean:44 (same declaration text).