English
A refinement of le_mul_withDensity showing the inequality for arbitrary measurable s against the density μ.withDensity(limRatioMeas hρ).
Русский
Уточнение неравенства le_mul_withDensity для произвольного измеримого s по плотности μ.withDensity(limRatioMeas hρ).
LaTeX
$$$\forall s\ MeasurableSet s,\ ρ s ≤ t · μ.withDensity (v.limRatioMeas hρ) s$ for appropriate t.$$
Lean4
/-- As an intermediate step to show that `μ.withDensity (v.limRatioMeas hρ) = ρ`, we show here
that `ρ ≤ t μ.withDensity (v.limRatioMeas hρ)` for any `t > 1`. -/
theorem le_mul_withDensity {s : Set α} (hs : MeasurableSet s) {t : ℝ≥0} (ht : 1 < t) :
ρ s ≤ t * μ.withDensity (v.limRatioMeas hρ) s := by
/- We cut `s` into the sets where `v.limRatioMeas hρ = 0`, where `v.limRatioMeas hρ = ∞`, and
where `v.limRatioMeas hρ ∈ [t^n, t^(n+1))` for `n : ℤ`. The first and second have measure `0`.
For the latter, since `v.limRatioMeas hρ` fluctuates by at most `t` on this slice, we can use
`measure_le_mul_of_subset_limRatioMeas_lt` and `mul_measure_le_of_subset_lt_limRatioMeas` to
show that the two measures are comparable up to `t`. -/
have t_ne_zero' : t ≠ 0 := (zero_lt_one.trans ht).ne'
have t_ne_zero : (t : ℝ≥0∞) ≠ 0 := by simpa only [ENNReal.coe_eq_zero, Ne] using t_ne_zero'
let ν := μ.withDensity (v.limRatioMeas hρ)
let f := v.limRatioMeas hρ
have f_meas : Measurable f := v.limRatioMeas_measurable hρ
have A : ρ (s ∩ f ⁻¹' {0}) ≤ (t • ν) (s ∩ f ⁻¹' {0}) :=
by
refine le_trans (measure_mono inter_subset_right) (le_trans (le_of_eq ?_) (zero_le _))
exact v.measure_limRatioMeas_zero hρ
have B : ρ (s ∩ f ⁻¹' {∞}) ≤ (t • ν) (s ∩ f ⁻¹' {∞}) :=
by
apply le_trans (le_of_eq _) (zero_le _)
apply hρ
rw [← nonpos_iff_eq_zero]
exact (measure_mono inter_subset_right).trans (v.measure_limRatioMeas_top hρ).le
have C :
∀ n : ℤ,
ρ (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) ≤
(t • ν) (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) :=
by
intro n
let I := Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))
have M : MeasurableSet (s ∩ f ⁻¹' I) := hs.inter (f_meas measurableSet_Ico)
simp only [ν, I, M, withDensity_apply, coe_nnreal_smul_apply]
calc
ρ (s ∩ f ⁻¹' I) ≤ (t : ℝ≥0∞) ^ (n + 1) * μ (s ∩ f ⁻¹' I) :=
by
rw [← ENNReal.coe_zpow t_ne_zero']
apply v.measure_le_mul_of_subset_limRatioMeas_lt hρ
intro x hx
apply hx.2.2.trans_le (le_of_eq _)
rw [ENNReal.coe_zpow t_ne_zero']
_ = ∫⁻ _ in s ∩ f ⁻¹' I, (t : ℝ≥0∞) ^ (n + 1) ∂μ := by
simp only [lintegral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter]
_ ≤ ∫⁻ x in s ∩ f ⁻¹' I, t * f x ∂μ :=
by
apply lintegral_mono_ae ((ae_restrict_iff' M).2 (Eventually.of_forall fun x hx => ?_))
rw [add_comm, ENNReal.zpow_add t_ne_zero ENNReal.coe_ne_top, zpow_one]
exact mul_le_mul_left' hx.2.1 _
_ = t * ∫⁻ x in s ∩ f ⁻¹' I, f x ∂μ := lintegral_const_mul _ f_meas
calc
ρ s = ρ (s ∩ f ⁻¹' {0}) + ρ (s ∩ f ⁻¹' {∞}) + ∑' n : ℤ, ρ (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) :=
measure_eq_measure_preimage_add_measure_tsum_Ico_zpow ρ f_meas hs ht
_ ≤
(t • ν) (s ∩ f ⁻¹' {0}) + (t • ν) (s ∩ f ⁻¹' {∞}) +
∑' n : ℤ, (t • ν) (s ∩ f ⁻¹' Ico ((t : ℝ≥0∞) ^ n) ((t : ℝ≥0∞) ^ (n + 1))) :=
(add_le_add (add_le_add A B) (ENNReal.tsum_le_tsum C))
_ = (t • ν) s := (measure_eq_measure_preimage_add_measure_tsum_Ico_zpow (t • ν) f_meas hs ht).symm
