ι : Type ?u.1838723
𝕜 : Type ?u.1838726
E : Type u_1
F : Type ?u.1838732
A : Type ?u.1838735
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g✝ φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : NormedSpace.Dual ℝ E
⊢ ↑g (∫ (y : ℝ) in a..b, f' y) = ↑g (f b - f a)
ι : Type ?u.1838723
𝕜 : Type ?u.1838726
E : Type u_1
F : Type ?u.1838732
A : Type ?u.1838735
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
⊢ (∫ (y : ℝ) in a..b, f' y) = f b - f a
refine' (NormedSpace.eq_iff_forall_dual_eq ℝ).2 fun g => _
ι : Type ?u.1838723
𝕜 : Type ?u.1838726
E : Type u_1
F : Type ?u.1838732
A : Type ?u.1838735
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g✝ φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : NormedSpace.Dual ℝ E
⊢ (∫ (x : ℝ) in a..b, ↑g (f' x)) = ↑g (f b) - ↑g (f a)
ι : Type ?u.1838723
𝕜 : Type ?u.1838726
E : Type u_1
F : Type ?u.1838732
A : Type ?u.1838735
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g✝ φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : NormedSpace.Dual ℝ E
⊢ ↑g (∫ (y : ℝ) in a..b, f' y) = ↑g (f b - f a)
rw [← g.intervalIntegral_comp_comm f'int, g.map_sub]
no goals
ι : Type ?u.1838723
𝕜 : Type ?u.1838726
E : Type u_1
F : Type ?u.1838732
A : Type ?u.1838735
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g✝ φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivWithinAt f (f' x) (Ioi x) x
f'int : IntervalIntegrable f' volume a b
g : NormedSpace.Dual ℝ E
⊢ (∫ (x : ℝ) in a..b, ↑g (f' x)) = ↑g (f b) - ↑g (f a)
exact integral_eq_sub_of_hasDeriv_right_of_le_real hab (g.continuous.comp_continuousOn hcont)
  (fun x hx => g.hasFDerivAt.comp_hasDerivWithinAt x (hderiv x hx))
  (g.integrable_comp ((intervalIntegrable_iff_integrable_Icc_of_le hab).1 f'int))