English
If ht holds, then X belongs to L^p with respect to the tilted measure μ.tilted(t X·) for every p≥0.
Русский
При условии ht, X ∈ L^p по отношению к смещённой мере μ_tilted(tX·) для каждого p≥0.
LaTeX
$$$\\text{If } ht, \\quad X \\in L^p(\\mu_{tX}) \\text{ for all } p \\ge 0$$$
Lean4
theorem memLp_tilted_mul (ht : t ∈ interior (integrableExpSet X μ)) (p : ℝ≥0) : MemLp X p (μ.tilted (t * X ·)) :=
by
have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet ht
by_cases hp : p = 0
· simpa [hp] using hX.aestronglyMeasurable.mono_ac (tilted_absolutelyContinuous _ _)
refine ⟨hX.aestronglyMeasurable.mono_ac (tilted_absolutelyContinuous _ _), ?_⟩
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top]
rotate_left
· simp [hp]
· simp
simp_rw [ENNReal.coe_toReal, ← ofReal_norm_eq_enorm, norm_eq_abs,
ENNReal.ofReal_rpow_of_nonneg (x := |X _|) (p := p) (abs_nonneg (X _)) p.2]
refine Integrable.lintegral_lt_top ?_
simp_rw [integrable_tilted_iff (interior_subset (s := integrableExpSet X μ) ht), smul_eq_mul, mul_comm]
exact integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet ht p.2
