OAI/Probability/GaussianInformation/Kernel/ReplicaMoments.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

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