OAI/Probability/GaussianInformation/Dyadic/GaussianImages.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RepeatedLocalization.finiteProduct_le line 19
  2. lemma OAI.RepeatedLocalization.standardGaussianPDF_le_one line 33
  3. lemma OAI.RepeatedLocalization.standardGaussian_le_volume line 44
  4. lemma OAI.RepeatedLocalization.iidGaussian_le_volume line 49
  5. lemma OAI.RepeatedLocalization.gaussian_square_map_le line 53
  6. lemma OAI.RepeatedLocalization.rectangularGaussian_eq line 65
  7. lemma OAI.RepeatedLocalization.rectangularGaussian_squareRoot_eq line 89
  8. lemma OAI.RepeatedLocalization.gaussian_rectangular_map_le line 105
  9. lemma OAI.RepeatedLocalization.gaussian_rectangular_box_le line 122
  10. lemma OAI.RepeatedLocalization.gaussian_multirow_box_le line 141
  11. lemma OAI.RepeatedLocalization.gaussian_multirow_box_le_extended line 161
  12. def OAI.RepeatedLocalization.rowMatrix line 181
  13. lemma OAI.RepeatedLocalization.rowMatrix_gram line 184