OAI/Probability/InvariantIsing/Core/KernelExponentialBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exponential endpoint bounds compose additively over Markov kernels. The proof includes integrability, so no undefined Bochner integral is used in the recursive Gaussian moment estimates.

  1. theorem OAI.InvariantIsing.kernel_exp_bound_comp line 14