OAI/Probability/GaussianReplacement/StreamBlock.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NoiselessRegression.Learner.run_congr_labels line 15

   Also declared: OAI/Probability/GaussianRegression/Rotational.lean:57 (same declaration text).

2. lemma OAI.NoiselessRegression.Learner.estimate_congr_labels line 29

   Also declared: OAI/Probability/GaussianRegression/Rotational.lean:71 (same declaration text).

3. lemma OAI.NoiselessRegression.Learner.angularSuccess_nullMeasurable line 34

   Also declared: OAI/Probability/GaussianRegression/Rotational.lean:76 (same declaration text).

4. lemma OAI.NoiselessRegression.Learner.linear_success_bound line 44

   Also declared: OAI/Probability/GaussianRegression/Rotational.lean:86 (same declaration text).

5. lemma OAI.NoiselessRegression.blockValue_le_one_no_borel line 96