OAI/Probability/GaussianInformation/Kernel/ProjectionMoments.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KernelPotential.Projection.Support.gaussianRows line 20
2. def OAI.KernelPotential.Projection.Support.projectVector line 23
3. lemma OAI.KernelPotential.Projection.Support.continuous_projectVector line 26
4. lemma OAI.KernelPotential.Projection.Support.projectVector_sub line 31
5. lemma OAI.KernelPotential.Projection.Support.projectVector_rowMatrix line 36
6. lemma OAI.KernelPotential.Projection.Support.boxScale_cancel line 44
7. lemma OAI.KernelPotential.Projection.Support.fixedReplica_moment_le line 53
8. def OAI.KernelPotential.Projection.Support.smoothedProjection line 107
9. lemma OAI.KernelPotential.Projection.Support.measurable_projection_kernel line 112
10. lemma OAI.KernelPotential.Projection.Support.measurable_smoothedProjection line 121
11. lemma OAI.KernelPotential.Projection.Support.measurable_replicated line 126
12. lemma OAI.KernelPotential.Projection.Support.measurable_replica_kernel line 133
13. lemma OAI.KernelPotential.Projection.Support.smoothedProjection_moment_le line 139
14. lemma OAI.KernelPotential.Projection.measurable_zero_kernel line 181