OAI/Probability/GaussianInformation/Dyadic/ReplicaMoments.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RepeatedLocalization.gramSchmidt_castSucc line 19
2. def OAI.RepeatedLocalization.replicaPlane line 29
3. lemma OAI.RepeatedLocalization.replicaPlane_nonempty line 32
4. lemma OAI.RepeatedLocalization.replicaPlane_finrank_le line 36
5. lemma OAI.RepeatedLocalization.lastPlane_infDist_le line 42
6. def OAI.RepeatedLocalization.gramInverseProduct line 63
7. lemma OAI.RepeatedLocalization.gramInverseProduct_succ line 66
8. lemma OAI.RepeatedLocalization.measurable_gramInverseProduct line 73
9. lemma OAI.RepeatedLocalization.lintegral_gramInverseProduct_le line 79
10. lemma OAI.RepeatedLocalization.gramInverseProduct_eq_inverseVolume line 139
11. lemma OAI.RepeatedLocalization.lintegral_replicaInverse_le line 147