OAI/Probability/GaussianPropeller/PairBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GaussianPropeller.PairGeometry.orthonormal_triple_of_gram_pos line 39
2. lemma OAI.GaussianPropeller.Pair.triangle_inner_bound line 109
3. lemma OAI.GaussianPropeller.Pair.setIntegral_inner_le_triangle line 138
4. lemma OAI.GaussianPropeller.Pair.integral_inner_eq_inner_integral line 175
5. lemma OAI.GaussianPropeller.Pair.sqrt_gram_smul line 181
6. lemma OAI.GaussianPropeller.Pair.centroid_residual_pair line 190