OAI/Probability/GaussianInformation/Kernel/GaussianImages.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

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