OAI/Probability/LatticePassage/ExponentialEnergy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CompanionFPP.exponential_square_difference line 9
2. lemma OAI.CompanionFPP.exponential_square_difference_split line 22
3. theorem OAI.CompanionFPP.exponential_resampling_energy_split line 37
4. theorem OAI.CompanionFPP.finite_exponential_forward_energy line 70
5. theorem OAI.CompanionFPP.finite_exponential_resampling_energy line 116