English
The measure of the half-open interval Ioc(a,b) equals f(b) - f(a) in ENNReal, i.e., μ_f(Ioc(a,b)) = ofReal(f(b) - f(a)).
Русский
Мера полупрерывного интервала Ioc(a,b) равна f(b) - f(a) в ENNReal: μ_f(Ioc(a,b)) = ofReal(f(b) - f(a)).
LaTeX
$$μ_f(Ioc(a,b)) = \operatorname{ofReal}(f(b) - f(a))$$
Lean4
@[simp]
theorem measure_singleton (a : ℝ) : f.measure { a } = ofReal (f a - leftLim f a) :=
by
obtain ⟨u, u_mono, u_lt_a, u_lim⟩ : ∃ u : ℕ → ℝ, StrictMono u ∧ (∀ n : ℕ, u n < a) ∧ Tendsto u atTop (𝓝 a) :=
exists_seq_strictMono_tendsto a
have A : { a } = ⋂ n, Ioc (u n) a :=
by
refine Subset.antisymm (fun x hx => by simp [mem_singleton_iff.1 hx, u_lt_a]) fun x hx => ?_
replace hx : ∀ (i : ℕ), u i < x ∧ x ≤ a := by simpa using hx
have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.le
simp [le_antisymm this (hx 0).2]
have L1 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure { a })) :=
by
rw [A]
refine tendsto_measure_iInter_atTop (fun n => nullMeasurableSet_Ioc) (fun m n hmn => ?_) ?_
· exact Ioc_subset_Ioc_left (u_mono.monotone hmn)
· exact ⟨0, by simpa only [measure_Ioc] using ENNReal.ofReal_ne_top⟩
have L2 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (ofReal (f a - leftLim f a))) :=
by
simp only [measure_Ioc]
have : Tendsto (fun n => f (u n)) atTop (𝓝 (leftLim f a)) :=
by
apply (f.mono.tendsto_leftLim a).comp
exact tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ u_lim (Eventually.of_forall fun n => u_lt_a n)
exact ENNReal.continuous_ofReal.continuousAt.tendsto.comp (tendsto_const_nhds.sub this)
exact tendsto_nhds_unique L1 L2
