ι : Type ?u.18986205
𝕜 : Type ?u.18986208
E : Type u_1
F : Type ?u.18986214
A : Type ?u.18986217
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a✝ b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a : ℝ
⊢ ∀ (x : ℝ), ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) x
ι : Type ?u.18986205
𝕜 : Type ?u.18986208
E : Type u_1
F : Type ?u.18986214
A : Type ?u.18986217
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a✝ b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a : ℝ
⊢ Continuous fun b => ∫ (x : ℝ) in a..b, f x ∂μ
rw [continuous_iff_continuousAt]
ι : Type ?u.18986205
𝕜 : Type ?u.18986208
E : Type u_1
F : Type ?u.18986214
A : Type ?u.18986217
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a✝ b b₀✝ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ : ℝ
⊢ ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) b₀
ι : Type ?u.18986205
𝕜 : Type ?u.18986208
E : Type u_1
F : Type ?u.18986214
A : Type ?u.18986217
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a✝ b b₀ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a : ℝ
⊢ ∀ (x : ℝ), ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) x
intro b₀
case intro
ι : Type ?u.18986205
𝕜 : Type ?u.18986208
E : Type u_1
F : Type ?u.18986214
A : Type ?u.18986217
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a✝ b b₀✝ b₁✝ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ b₁ : ℝ
hb₁ : b₁ < b₀
⊢ ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) b₀
ι : Type ?u.18986205
𝕜 : Type ?u.18986208
E : Type u_1
F : Type ?u.18986214
A : Type ?u.18986217
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a✝ b b₀✝ b₁ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ : ℝ
⊢ ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) b₀
cases' exists_lt b₀ with b₁ hb₁
case intro.intro
ι : Type ?u.18986205
𝕜 : Type ?u.18986208
E : Type u_1
F : Type ?u.18986214
A : Type ?u.18986217
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a✝ b b₀✝ b₁✝ b₂✝ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ b₁ : ℝ
hb₁ : b₁ < b₀
b₂ : ℝ
hb₂ : b₀ < b₂
⊢ ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) b₀
case intro
ι : Type ?u.18986205
𝕜 : Type ?u.18986208
E : Type u_1
F : Type ?u.18986214
A : Type ?u.18986217
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a✝ b b₀✝ b₁✝ b₂ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ b₁ : ℝ
hb₁ : b₁ < b₀
⊢ ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) b₀
cases' exists_gt b₀ with b₂ hb₂
ι : Type ?u.18986205
𝕜 : Type ?u.18986208
E : Type u_1
F : Type ?u.18986214
A : Type ?u.18986217
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a✝ b b₀✝ b₁✝ b₂✝ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ b₁ : ℝ
hb₁ : b₁ < b₀
b₂ : ℝ
hb₂ : b₀ < b₂
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
case intro.intro
ι : Type ?u.18986205
𝕜 : Type ?u.18986208
E : Type u_1
F : Type ?u.18986214
A : Type ?u.18986217
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a✝ b b₀✝ b₁✝ b₂✝ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ b₁ : ℝ
hb₁ : b₁ < b₀
b₂ : ℝ
hb₂ : b₀ < b₂
⊢ ContinuousAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) b₀
apply ContinuousWithinAt.continuousAt _ (Icc_mem_nhds hb₁ hb₂)
no goals
ι : Type ?u.18986205
𝕜 : Type ?u.18986208
E : Type u_1
F : Type ?u.18986214
A : Type ?u.18986217
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
inst✝¹ : NormedSpace ℝ E
a✝ b b₀✝ b₁✝ b₂✝ : ℝ
μ : MeasureTheory.Measure ℝ
f g : ℝ → E
inst✝ : NoAtoms μ
h_int : ∀ (a b : ℝ), IntervalIntegrable f μ a b
a b₀ b₁ : ℝ
hb₁ : b₁ < b₀
b₂ : ℝ
hb₂ : b₀ < b₂
⊢ ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Icc b₁ b₂) b₀
exact continuousWithinAt_primitive (measure_singleton b₀) (h_int _ _)