f : StieltjesFunction
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ Tendsto (fun x => ↑↑(StieltjesFunction.measure f) (Iic x)) atTop (𝓝 (ofReal (u - l)))
f : StieltjesFunction
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ ↑↑(StieltjesFunction.measure f) univ = ofReal (u - l)
refine' tendsto_nhds_unique (tendsto_measure_Iic_atTop _) _
f : StieltjesFunction
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ Tendsto (fun x => ofReal (↑f x - l)) atTop (𝓝 (ofReal (u - l)))
f : StieltjesFunction
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ Tendsto (fun x => ↑↑(StieltjesFunction.measure f) (Iic x)) atTop (𝓝 (ofReal (u - l)))
simp_rw [measure_Iic f hfl]
no goals
f : StieltjesFunction
l u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
⊢ Tendsto (fun x => ofReal (↑f x - l)) atTop (𝓝 (ofReal (u - l)))
exact ENNReal.tendsto_ofReal (Tendsto.sub_const hfu _)