f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ↑↑(StieltjesFunction.measure f) (Ico x x_1)) atTop (𝓝 (ofReal (l - leftLim (↑f) x)))
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ ↑↑(StieltjesFunction.measure f) (Ici x) = ofReal (l - leftLim (↑f) x)
refine' tendsto_nhds_unique (tendsto_measure_Ico_atTop _ _) _
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ofReal (leftLim (↑f) x_1 - leftLim (↑f) x)) atTop (𝓝 (ofReal (l - leftLim (↑f) x)))
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ↑↑(StieltjesFunction.measure f) (Ico x x_1)) atTop (𝓝 (ofReal (l - leftLim (↑f) x)))
simp_rw [measure_Ico]
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ Tendsto (fun x => leftLim (↑f) x) atTop (𝓝 l)
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ofReal (leftLim (↑f) x_1 - leftLim (↑f) x)) atTop (𝓝 (ofReal (l - leftLim (↑f) x)))
refine' ENNReal.tendsto_ofReal (Tendsto.sub_const _ _)
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
⊢ Tendsto (fun x => leftLim (↑f) x) atTop (𝓝 l)
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
⊢ Tendsto (fun x => leftLim (↑f) x) atTop (𝓝 l)
have h_le1 : ∀ x, f (x - 1) ≤ leftLim f x := fun x => Monotone.le_leftLim f.mono (sub_one_lt x)
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
⊢ Tendsto (fun x => leftLim (↑f) x) atTop (𝓝 l)
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
⊢ Tendsto (fun x => leftLim (↑f) x) atTop (𝓝 l)
have h_le2 : ∀ x, leftLim f x ≤ f x := fun x => Monotone.leftLim_le f.mono le_rfl
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
⊢ Tendsto (fun i => i - 1) atTop atTop
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
⊢ Tendsto (fun x => leftLim (↑f) x) atTop (𝓝 l)
refine' tendsto_of_tendsto_of_tendsto_of_le_of_le (hf.comp _) hf h_le1 h_le2
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a - 1
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
⊢ Tendsto (fun i => i - 1) atTop atTop
rw [tendsto_atTop_atTop]
no goals
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
⊢ ∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ a - 1
exact fun y => ⟨y + 1, fun z hyz => by rwa [le_sub_iff_add_le]⟩
no goals
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : ℝ
h_le1 : ∀ (x : ℝ), ↑f (x - 1) ≤ leftLim (↑f) x
h_le2 : ∀ (x : ℝ), leftLim (↑f) x ≤ ↑f x
y z : ℝ
hyz : y + 1 ≤ z
⊢ y ≤ z - 1
rwa [le_sub_iff_add_le]