English
Consequence: the equality μ.withDensity(limRatioMeas hρ) = ρ holds on all measurable sets as a global equality of measures.
Русский
Следствие: равенство μ.withDensity(limRatioMeas hρ) = ρ действует на всех измеримых множествах как глобальное равенство мер.
LaTeX
$$$\mu.withDensity (v.limRatioMeas hρ) = ρ$$$
Lean4
theorem withDensity_limRatioMeas_eq : μ.withDensity (v.limRatioMeas hρ) = ρ :=
by
ext1 s hs
refine le_antisymm ?_ ?_
· have : Tendsto (fun t : ℝ≥0 => ((t : ℝ≥0∞) ^ 2 * ρ s : ℝ≥0∞)) (𝓝[>] 1) (𝓝 ((1 : ℝ≥0∞) ^ 2 * ρ s)) :=
by
refine ENNReal.Tendsto.mul ?_ ?_ tendsto_const_nhds ?_
· exact ENNReal.Tendsto.pow (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds)
· simp only [one_pow, true_or, Ne, not_false_iff, one_ne_zero]
· simp only [one_pow, Ne, or_true, ENNReal.one_ne_top, not_false_iff]
simp only [one_pow, one_mul] at this
refine ge_of_tendsto this ?_
filter_upwards [self_mem_nhdsWithin] with _ ht
exact v.withDensity_le_mul hρ hs ht
· have :
Tendsto (fun t : ℝ≥0 => (t : ℝ≥0∞) * μ.withDensity (v.limRatioMeas hρ) s) (𝓝[>] 1)
(𝓝 ((1 : ℝ≥0∞) * μ.withDensity (v.limRatioMeas hρ) s)) :=
by
refine ENNReal.Tendsto.mul_const (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds) ?_
simp only [true_or, Ne, not_false_iff, one_ne_zero]
simp only [one_mul] at this
refine ge_of_tendsto this ?_
filter_upwards [self_mem_nhdsWithin] with _ ht
exact v.le_mul_withDensity hρ hs ht
