OAI/Probability/GaussianReplacement/StreamGeometry.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.NoiselessRegression.inverse_pow_dyadic_majorant line 19

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

2. lemma OAI.NoiselessRegression.dyadic_power_cancel line 54

   Also declared: OAI/Probability/GaussianRegression/InverseMoments.lean:58 (same declaration text).

3. theorem OAI.NoiselessRegression.inverse_moment_of_tube_bound line 66

   Also declared: OAI/Probability/GaussianRegression/InverseMoments.lean:70 (same declaration text).

4. theorem OAI.NoiselessRegression.exists_affine_tube_cover line 135

   Also declared: OAI/Probability/GaussianRegression/AffineTubes.lean:26 (same declaration text).

5. theorem OAI.NoiselessRegression.HasLocalMassBound.affine_tube line 167

   Also declared: OAI/Probability/GaussianRegression/AffineTubes.lean:58 (same declaration text).

6. lemma OAI.NoiselessRegression.tube_radius_factors line 197

   Also declared: OAI/Probability/GaussianRegression/AffineTubes.lean:88 (same declaration text).

7. theorem OAI.NoiselessRegression.HasLocalMassBound.affine_tube_pow line 204

   Also declared: OAI/Probability/GaussianRegression/AffineTubes.lean:95 (same declaration text).

8. theorem OAI.NoiselessRegression.HasLocalMassBound.affine_inverse_moment line 219

   Also declared: OAI/Probability/GaussianRegression/AffineTubes.lean:110 (same declaration text).

9. theorem OAI.NoiselessRegression.HasLocalMassBound.affine_null line 232

   Also declared: OAI/Probability/GaussianRegression/AffineTubes.lean:123 (same declaration text).