OAI/Probability/GaussianInformation/Kernel/ScaledReference.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KernelPotential.Scale.normalized_restriction line 14
2. lemma OAI.KernelPotential.Scale.dyadic_log_identity line 30
3. lemma OAI.KernelPotential.Scale.chosen_scale_log line 38
4. lemma OAI.KernelPotential.Scale.radius_mono line 61
5. lemma OAI.KernelPotential.Scale.reference_J_lower line 66