English
Same as above: from integrability of exp(u X) and exp(v X) with u ≠ v, deduce X is AEMeasurable.
Русский
То же самое: из интегрируемости exp(u X) и exp(v X) при u ≠ v следует, что X измерима почти наверняка.
LaTeX
$$$\\text{AEMeasurable}(X,\\mu)$$$
Lean4
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then
`ω ↦ exp (t * |X| + v * X)` is integrable. -/
theorem integrable_exp_mul_abs_add (ht_int_pos : Integrable (fun ω ↦ exp ((v + t) * X ω)) μ)
(ht_int_neg : Integrable (fun ω ↦ exp ((v - t) * X ω)) μ) : Integrable (fun ω ↦ exp (t * |X ω| + v * X ω)) μ :=
by
have h_int_add : Integrable (fun a ↦ exp ((v + t) * X a) + exp ((v - t) * X a)) μ :=
ht_int_pos.add <| by simpa using ht_int_neg
refine Integrable.mono h_int_add ?_ (ae_of_all _ fun ω ↦ ?_)
· by_cases ht : t = 0
· simp only [ht, zero_mul, zero_add, add_zero] at ht_int_pos ⊢
exact ht_int_pos.1
have hX : AEMeasurable X μ := aemeasurable_of_integrable_exp_mul ?_ ht_int_pos ht_int_neg
· fun_prop
· rw [← sub_ne_zero]
simp [ht]
· simp only [norm_eq_abs, abs_exp]
conv_rhs =>
rw [abs_of_nonneg (by positivity)]
-- ⊢ exp (t * |X ω| + v * X ω) ≤ exp ((v + t) * X ω) + exp ((v - t) * X ω)
rcases le_total 0 (X ω) with h_nonneg | h_nonpos
· rw [abs_of_nonneg h_nonneg, ← add_mul, add_comm, le_add_iff_nonneg_right]
positivity
· rw [abs_of_nonpos h_nonpos, mul_neg, mul_comm, ← mul_neg, mul_comm, ← add_mul, add_comm, ← sub_eq_add_neg,
le_add_iff_nonneg_left]
positivity
