OAI/Probability/GaussianInformation/Inverse/Orthogonal.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AllScaleInverseVolume.Suborthonormal line 13
  2. lemma OAI.AllScaleInverseVolume.Suborthonormal.inner_eq line 16
  3. lemma OAI.AllScaleInverseVolume.Suborthonormal.norm_le line 23
  4. lemma OAI.AllScaleInverseVolume.orthogonal_sum_norm_sq line 27
  5. lemma OAI.AllScaleInverseVolume.suborthonormal_synth_contraction line 37
  6. def OAI.AllScaleInverseVolume.orthoResidual line 47
  7. lemma OAI.AllScaleInverseVolume.suborthonormal_coeff_norm line 50
  8. lemma OAI.AllScaleInverseVolume.orthoResidual_inner line 54
  9. lemma OAI.AllScaleInverseVolume.orthoResidual_norm_sq line 62
  10. lemma OAI.AllScaleInverseVolume.orthoResidual_norm_antitone line 77
  11. lemma OAI.AllScaleInverseVolume.suborthonormal_bessel line 86
  12. lemma OAI.AllScaleInverseVolume.gramSchmidtNormed_suborthonormal line 92
  13. lemma OAI.AllScaleInverseVolume.Suborthonormal.cut line 103