OAI/Probability/GaussianInformation/Kernel/GramVolume.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KernelPotential.Projection.Support.gram_linearCombination line 19
  2. def OAI.KernelPotential.Projection.Support.gramTriangular line 31
  3. lemma OAI.KernelPotential.Projection.Support.gramTriangular_expansion line 35
  4. lemma OAI.KernelPotential.Projection.Support.gramTriangular_det line 46
  5. lemma OAI.KernelPotential.Projection.Support.gram_gramSchmidt line 55
  6. lemma OAI.KernelPotential.Projection.Support.gram_det_eq_prod_gramSchmidt line 64
  7. lemma OAI.KernelPotential.Projection.Support.sqrt_gram_det_eq_prod_gramSchmidt line 78
  8. lemma OAI.KernelPotential.Projection.Support.gramSchmidt_real_def line 82
  9. lemma OAI.KernelPotential.Projection.Support.measurable_gramSchmidt line 88
  10. lemma OAI.KernelPotential.Projection.Support.gramSchmidt_prefix_congr line 98
  11. lemma OAI.KernelPotential.Projection.Support.gramSchmidt_residual_mem_span line 109
  12. lemma OAI.KernelPotential.Projection.Support.infDist_span_le_gramSchmidt line 118