OAI/Probability/GaussianInformation/Inverse/GreedyOrder.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AllScaleInverseVolume.Greedy line 15
  2. lemma OAI.AllScaleInverseVolume.swap_preserves_lower_bound line 18
  3. lemma OAI.AllScaleInverseVolume.exists_greedy_permutation line 27
  4. def OAI.AllScaleInverseVolume.prefixResidual line 72
  5. def OAI.AllScaleInverseVolume.prefixAxes line 74
  6. lemma OAI.AllScaleInverseVolume.prefixAxes_suborthonormal line 77
  7. lemma OAI.AllScaleInverseVolume.gramSchmidtNormed_term line 81
  8. lemma OAI.AllScaleInverseVolume.prefixResidual_self line 89
  9. lemma OAI.AllScaleInverseVolume.prefixResidual_eq line 96
  10. lemma OAI.AllScaleInverseVolume.prefixResidual_prefix_congr line 109
  11. lemma OAI.AllScaleInverseVolume.prefixAxes_prefix_congr line 120
  12. lemma OAI.AllScaleInverseVolume.measurable_gramSchmidtNormed line 128
  13. lemma OAI.AllScaleInverseVolume.measurable_prefixAxes line 132
  14. lemma OAI.AllScaleInverseVolume.measurable_prefixResidual line 138
  15. def OAI.AllScaleInverseVolume.residualScore line 147
  16. lemma OAI.AllScaleInverseVolume.exists_greedy_gram_order line 150
  17. lemma OAI.AllScaleInverseVolume.greedy_lengths_antitone line 156
  18. lemma OAI.AllScaleInverseVolume.measurableSet_greedy line 166