OAI/Probability/GaussianInformation/Inverse/GramVolume.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AllScaleInverseVolume.gram_linearCombination line 16
  2. def OAI.AllScaleInverseVolume.gramTriangular line 28
  3. lemma OAI.AllScaleInverseVolume.gramTriangular_expansion line 32
  4. lemma OAI.AllScaleInverseVolume.gramTriangular_det line 43
  5. lemma OAI.AllScaleInverseVolume.gram_gramSchmidt line 52
  6. lemma OAI.AllScaleInverseVolume.gram_det_eq_prod_gramSchmidt line 61
  7. lemma OAI.AllScaleInverseVolume.sqrt_gram_det_eq_prod_gramSchmidt line 75
  8. lemma OAI.AllScaleInverseVolume.gramSchmidt_real_def line 79
  9. lemma OAI.AllScaleInverseVolume.measurable_gramSchmidt line 85
  10. lemma OAI.AllScaleInverseVolume.gramSchmidt_prefix_congr line 95
  11. lemma OAI.AllScaleInverseVolume.gramSchmidt_residual_mem_span line 106
  12. lemma OAI.AllScaleInverseVolume.infDist_span_le_gramSchmidt line 115