OAI/Probability/GaussianInformation/Kernel/Main.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KernelPotential.FiniteMessage.component_le_sphere line 17
2. lemma OAI.KernelPotential.FiniteMessage.component_masses_sum line 21
3. lemma OAI.KernelPotential.FiniteMessage.averagePhi_energy line 26
4. lemma OAI.KernelPotential.FiniteMessage.entropy_charge line 28
5. lemma OAI.KernelPotential.FiniteMessage.actual_row_drift_bound line 52
6. lemma OAI.KernelPotential.numeric_drift_charge line 80
7. theorem OAI.KernelPotential.actual_row_drift line 97

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