OAI/Probability/GaussianInformation/Kernel/Scaling.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KernelPotential.Geometry.truncated_inverseMoment line 12
2. lemma OAI.KernelPotential.Geometry.exists_good_dyadic_scale line 71
3. def OAI.KernelPotential.Scale.radius line 139
4. lemma OAI.KernelPotential.Scale.radius_pos line 140
5. lemma OAI.KernelPotential.Scale.closed_cap line 142
6. lemma OAI.KernelPotential.Scale.norm_half_tail line 154
7. lemma OAI.KernelPotential.Scale.exists_J_scale line 179