English
Tilting by f and then by g is the same as tilting by f+g: (μ.tilted f).tilted g = μ.tilted (f+g) (when exp f is integrable).
Русский
Сначала тильтуем по f, затем по g; это равно тильтованию по f+g.
LaTeX
$$$$ (\\mu^{\\mathrm{tilted}} f)^{\\mathrm{tilted}} g = \\mu^{\\mathrm{tilted}}(f+g). $$$$
Lean4
theorem tilted_tilted (hf : Integrable (fun x ↦ exp (f x)) μ) (g : α → ℝ) : (μ.tilted f).tilted g = μ.tilted (f + g) :=
by
cases eq_zero_or_neZero μ with
| inl h => simp [h]
| inr h0 =>
ext1 s hs
rw [tilted_apply' _ _ hs, tilted_apply' _ _ hs, setLIntegral_tilted' f _ hs]
congr with x
rw [← ENNReal.ofReal_mul (by positivity), integral_exp_tilted f, Pi.add_apply, exp_add]
congr 1
simp only [Pi.add_apply]
have := (integral_exp_pos hf).ne'
simp [field]
