OAI/Probability/GaussianInformation/Kernel/ConditionalCharge.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KernelPotential.NoisyDrift.reference_log_measurable line 18
2. lemma OAI.KernelPotential.NoisyDrift.reference_log_uniform_bound line 27
3. lemma OAI.KernelPotential.NoisyDrift.joint_Phi_identity line 39
4. lemma OAI.KernelPotential.NoisyDrift.referenceWeight_pos line 80
5. lemma OAI.KernelPotential.NoisyDrift.positive_noisy_comparison line 87