OAI/Probability/PosteriorReplicas/Regression/ReplicaNondegenerate.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PosteriorRegression.measurableSet_gramSchmidt_ne_zero line 18
2. theorem OAI.PosteriorRegression.ae_gramSchmidt_ne_zero line 27
3. theorem OAI.PosteriorRegression.ae_replica_linearIndependent line 63
4. lemma OAI.PosteriorRegression.sqrt_det_gram line 75
5. lemma OAI.PosteriorRegression.replicaWeight_eq_det line 81
6. theorem OAI.PosteriorRegression.gram_integral_bound line 87