ι : Type ?u.18353564
𝕜 : Type ?u.18353567
E : Type u_1
F : Type ?u.18353573
A : Type ?u.18353576
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
aux : (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) (Icc a b)
ι : Type ?u.18353564
𝕜 : Type ?u.18353567
E : Type u_1
F : Type ?u.18353573
A : Type ?u.18353576
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) (Icc a b)
have aux : (fun x => ∫ t in Icc a x, f t ∂μ) = fun x => ∫ t in Ioc a x, f t ∂μ := by
  ext x
  exact integral_Icc_eq_integral_Ioc
ι : Type ?u.18353564
𝕜 : Type ?u.18353567
E : Type u_1
F : Type ?u.18353573
A : Type ?u.18353576
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
aux : (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
ι : Type ?u.18353564
𝕜 : Type ?u.18353567
E : Type u_1
F : Type ?u.18353573
A : Type ?u.18353576
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
aux : (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) (Icc a b)
rw [aux]
no goals
ι : Type ?u.18353564
𝕜 : Type ?u.18353567
E : Type u_1
F : Type ?u.18353573
A : Type ?u.18353576
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
aux : (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ
⊢ ContinuousOn (fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ) (Icc a b)
exact continuousOn_primitive h_int
case h
ι : Type ?u.18353564
𝕜 : Type ?u.18353567
E : Type u_1
F : Type ?u.18353573
A : Type ?u.18353576
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
x : ℝ
⊢ (∫ (t : ℝ) in Icc a x, f t ∂μ) = ∫ (t : ℝ) in Ioc a x, f t ∂μ
ι : Type ?u.18353564
𝕜 : Type ?u.18353567
E : Type u_1
F : Type ?u.18353573
A : Type ?u.18353576
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
⊢ (fun x => ∫ (t : ℝ) in Icc a x, f t ∂μ) = fun x => ∫ (t : ℝ) in Ioc a x, f t ∂μ
ext x
no goals
case h
ι : Type ?u.18353564
𝕜 : Type ?u.18353567
E : Type u_1
F : Type ?u.18353573
A : Type ?u.18353576
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : IntegrableOn f (Icc a b)
x : ℝ
⊢ (∫ (t : ℝ) in Icc a x, f t ∂μ) = ∫ (t : ℝ) in Ioc a x, f t ∂μ
exact integral_Icc_eq_integral_Ioc