OAI/Probability/GaussianRegression/InverseMoments.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Inverse moments from polynomial tube bounds.

  1. lemma OAI.NoiselessRegression.inverse_pow_dyadic_majorant line 23

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

  2. lemma OAI.NoiselessRegression.dyadic_power_cancel line 58

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

  3. theorem OAI.NoiselessRegression.inverse_moment_of_tube_bound line 70

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