Commit 2023-12-07 21:29 5522fc37

feat: exponentially tilted measures (#7676) Define exponentially tilted measures. The exponential tilting of a measure μ on α by a function f : α → ℝ is the measure with density x ↦ exp (f x) / ∫ y, exp (f y) ∂μ with respect to μ.