OAI/Probability/GaussianRegression/Support.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Finite-volume enclosures for Gaussian matrix observations.

  1. def OAI.NoiselessRegression.coordinateNorm line 22
  2. lemma OAI.NoiselessRegression.continuous_coordinateNorm line 24
  3. lemma OAI.NoiselessRegression.coordinateNorm_sq line 29
  4. lemma OAI.NoiselessRegression.coordinateNorm_smul line 33
  5. def OAI.NoiselessRegression.coordinateBall line 37
  6. lemma OAI.NoiselessRegression.measurableSet_coordinateBall line 40
  7. lemma OAI.NoiselessRegression.coordinateBall_smul line 44
  8. lemma OAI.NoiselessRegression.volume_coordinateBall_smul line 58
  9. lemma OAI.NoiselessRegression.gaussianPDF_le_exp line 64
  10. lemma OAI.NoiselessRegression.lintegral_quarterGaussian_le line 74
  11. lemma OAI.NoiselessRegression.gaussian_density_pair_bound line 92
  12. lemma OAI.NoiselessRegression.measurable_coordinateVolume line 120
  13. lemma OAI.NoiselessRegression.gaussian_expected_coordinate_volume line 132
  14. lemma OAI.NoiselessRegression.stdGaussian_inner_map line 179
  15. lemma OAI.NoiselessRegression.rows_inner_map line 194
  16. lemma OAI.NoiselessRegression.rows_expected_coordinate_volume line 204
  17. def OAI.NoiselessRegression.rowOperator line 222
  18. lemma OAI.NoiselessRegression.rowOperator_apply line 227
  19. def OAI.NoiselessRegression.netProjectionSupport line 232
  20. lemma OAI.NoiselessRegression.measurableSet_netProjectionSupport line 236
  21. lemma OAI.NoiselessRegression.netProjectionSupport_volume line 242
  22. lemma OAI.NoiselessRegression.opNorm_le_twice_net line 270
  23. theorem OAI.NoiselessRegression.exists_projection_support line 296