OAI/Probability/GaussianRegression/GaussianKernel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Gaussian coordinate domination and replica kernel bounds.

  1. lemma OAI.NoiselessRegression.orthonormal_gaussian_map line 23
  2. lemma OAI.NoiselessRegression.gaussianReal_le_volume line 48
  3. lemma OAI.NoiselessRegression.measure_pi_mono line 65
  4. lemma OAI.NoiselessRegression.pi_gaussianReal_le_volume line 78
  5. lemma OAI.NoiselessRegression.gaussian_pairings_le line 81
  6. lemma OAI.NoiselessRegression.measure_pi_smul line 120
  7. lemma OAI.NoiselessRegression.gaussian_rows_pairings_le line 131
  8. lemma OAI.NoiselessRegression.lintegral_fin_prod line 148
  9. lemma OAI.NoiselessRegression.lintegral_pow_pi line 159
  10. lemma OAI.NoiselessRegression.lintegral_product_differences line 165
  11. lemma OAI.NoiselessRegression.gaussian_rows_kernel_bound line 184
  12. lemma OAI.NoiselessRegression.gaussian_replica_kernel_bound line 209