E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
⊢ Tendsto (fun i => ∫ (x : ℝ) in a..id i, f' x) atTop (𝓝 (m - f a))
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
⊢ (∫ (x : ℝ) in Ioi a, f' x) = m - f a
refine' tendsto_nhds_unique (intervalIntegral_tendsto_integral_Ioi a f'int tendsto_id) _
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
⊢ (fun k => f k - f a) =ᶠ[atTop] fun i => ∫ (x : ℝ) in a..id i, f' x
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
⊢ Tendsto (fun i => ∫ (x : ℝ) in a..id i, f' x) atTop (𝓝 (m - f a))
apply Tendsto.congr' _ (hf.sub_const _)
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ioi a
⊢ f x - f a = ∫ (x : ℝ) in a..id x, f' x
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
⊢ (fun k => f k - f a) =ᶠ[atTop] fun i => ∫ (x : ℝ) in a..id i, f' x
filter_upwards [Ioi_mem_atTop a] with x hx
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ f x - f a = ∫ (x : ℝ) in a..id x, f' x
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ioi a
⊢ f x - f a = ∫ (x : ℝ) in a..id x, f' x
have h'x : a ≤ id x := le_of_lt hx
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ (∫ (x : ℝ) in a..id x, f' x) = f x - f a
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ f x - f a = ∫ (x : ℝ) in a..id x, f' x
symm
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntervalIntegrable (fun y => f' y) volume a (id x)
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ (∫ (x : ℝ) in a..id x, f' x) = f x - f a
apply
  intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x (hcont.mono Icc_subset_Ici_self)
    fun y hy => hderiv y hy.1
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntegrableOn (fun y => f' y) (Ioc a (id x))
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntervalIntegrable (fun y => f' y) volume a (id x)
rw [intervalIntegrable_iff_integrable_Ioc_of_le h'x]
no goals
case h
E : Type u_1
f f' : ℝ → E
g g' : ℝ → ℝ
a b l : ℝ
m : E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hcont : ContinuousOn f (Ici a)
hderiv : ∀ (x : ℝ), x ∈ Ioi a → HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Ioi a)
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntegrableOn (fun y => f' y) (Ioc a (id x))
exact f'int.mono (fun y hy => hy.1) le_rfl