OAI/Probability/GaussianReplacement/StreamSphere.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NoiselessRegression.ae_fiber_aemeasurable line 30

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

2. lemma OAI.NoiselessRegression.prod_null_set_bound line 38

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

3. instance OAI.NoiselessRegression.sampleLaw_probability line 56

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

4. instance OAI.NoiselessRegression.uniformSphere_probability line 59

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