OAI/Probability/GaussianInformation/Kernel/MixedProjection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KernelPotential.Projection.fixed_center_replicas line 19
2. lemma OAI.KernelPotential.Projection.fixed_center_moment line 71
3. lemma OAI.KernelPotential.Projection.fresh_rows_kernel_le line 100
4. def OAI.KernelPotential.Projection.mixedCubeAverage line 110
5. lemma OAI.KernelPotential.Projection.auxiliary_average_le line 114
6. theorem OAI.KernelPotential.Projection.mixed_fixed_origin_moment line 136