OAI/Probability/GaussianPropeller/FourReduction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.GaussianPropeller.Reduction.residual_inner_base line 38
  2. lemma OAI.GaussianPropeller.Reduction.residual_norm_sq line 43
  3. lemma OAI.GaussianPropeller.Reduction.residual_inner line 50
  4. lemma OAI.GaussianPropeller.Reduction.residual_coefficient_sum line 58
  5. lemma OAI.GaussianPropeller.Reduction.residual_sum line 68
  6. lemma OAI.GaussianPropeller.Reduction.residualCoefficient_smul line 76
  7. lemma OAI.GaussianPropeller.Reduction.residualVector_smul line 82
  8. lemma OAI.GaussianPropeller.Reduction.normalized_tuple_pair line 86
  9. lemma OAI.GaussianPropeller.Reduction.residual_self line 117
  10. lemma OAI.GaussianPropeller.Reduction.residual_sum_all line 123
  11. lemma OAI.GaussianPropeller.Reduction.residual_obtuse line 127
  12. lemma OAI.GaussianPropeller.Reduction.residual_obtuse_all line 136
  13. lemma OAI.GaussianPropeller.Reduction.residual_coefficients_three line 146
  14. lemma OAI.GaussianPropeller.Reduction.configuration_determinants line 160