OAI/Probability/GaussianInformation/Kernel/Reweighting.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KernelPotential.Reweight.rho line 12
2. lemma OAI.KernelPotential.Reweight.rho_ac line 15
3. lemma OAI.KernelPotential.Reweight.local_lower_J line 18
4. lemma OAI.KernelPotential.Reweight.rho_ball line 36
5. lemma OAI.KernelPotential.Reweight.rho_le line 55
6. lemma OAI.KernelPotential.Reweight.rho_bounded line 70
7. lemma OAI.KernelPotential.Reweight.rho_finite line 84
8. lemma OAI.KernelPotential.Reweight.rho_two_ball_bounds line 89
9. def OAI.KernelPotential.Reweight.centeredRho line 101
10. lemma OAI.KernelPotential.Reweight.centered_ball line 104
11. lemma OAI.KernelPotential.Reweight.centered_finite line 112
12. lemma OAI.KernelPotential.Reweight.centered_support line 118
13. lemma OAI.KernelPotential.Reweight.centered_mixed_moment line 127