OAI/Probability/GaussianRegression/AffineTubes.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Affine tube covers and inverse-distance bounds.

  1. theorem OAI.NoiselessRegression.exists_affine_tube_cover line 26

    Also declared: OAI/Probability/GaussianReplacement/StreamGeometry.lean:135 (same declaration text).

  2. theorem OAI.NoiselessRegression.HasLocalMassBound.affine_tube line 58

    Also declared: OAI/Probability/GaussianReplacement/StreamGeometry.lean:167 (same declaration text).

  3. lemma OAI.NoiselessRegression.tube_radius_factors line 88

    Also declared: OAI/Probability/GaussianReplacement/StreamGeometry.lean:197 (same declaration text).

  4. theorem OAI.NoiselessRegression.HasLocalMassBound.affine_tube_pow line 95

    Also declared: OAI/Probability/GaussianReplacement/StreamGeometry.lean:204 (same declaration text).

  5. theorem OAI.NoiselessRegression.HasLocalMassBound.affine_inverse_moment line 110

    Also declared: OAI/Probability/GaussianReplacement/StreamGeometry.lean:219 (same declaration text).

  6. theorem OAI.NoiselessRegression.HasLocalMassBound.affine_null line 123

    Also declared: OAI/Probability/GaussianReplacement/StreamGeometry.lean:232 (same declaration text).