OAI/Probability/GaussianInformation/Kernel/Mixtures.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KernelPotential.Coercivity.log_ratio_lower line 13
2. lemma OAI.KernelPotential.Coercivity.log_ratio_mul line 25
3. lemma OAI.KernelPotential.Coercivity.perspective_sum_le line 32
4. lemma OAI.KernelPotential.Coercivity.mixture_probability line 69
5. lemma OAI.KernelPotential.Coercivity.mixture_density line 79
6. lemma OAI.KernelPotential.Coercivity.density_bounded line 95
7. lemma OAI.KernelPotential.Coercivity.J_mixture line 104
8. lemma OAI.KernelPotential.Coercivity.finite_convexity line 120
9. theorem OAI.KernelPotential.kernel_coercivity line 185

   Distinct definitions of this name: ComparatorChallenges/GaussianInformation.lean:200 (same statement text; different proof or body). Qualify references as OAI.KernelPotential.kernel_coercivity@path.