α : Type u_2
E : Type u_3
F✝ : Type ?u.1019635
𝕜 : Type ?u.1019638
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
inst✝² : CompleteSpace F✝
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → E
x₀ : X
bound : α → ℝ
hF_meas : ∀ᶠ (x : X) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun x => F x a) x₀
⊢ ContinuousAt
    (fun x => if hf : Integrable fun a => F x a then ↑L1.integralCLM (Integrable.toL1 (fun a => F x a) hf) else 0) x₀
α : Type u_2
E : Type u_3
F✝ : Type ?u.1019635
𝕜 : Type ?u.1019638
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
inst✝² : CompleteSpace F✝
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → E
x₀ : X
bound : α → ℝ
hF_meas : ∀ᶠ (x : X) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun x => F x a) x₀
⊢ ContinuousAt (fun x => ∫ (a : α), F x a ∂μ) x₀
simp only [integral, L1.integral]
no goals
α : Type u_2
E : Type u_3
F✝ : Type ?u.1019635
𝕜 : Type ?u.1019638
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : SMulCommClass ℝ 𝕜 E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedSpace ℝ F✝
inst✝² : CompleteSpace F✝
f g : α → E
m : MeasurableSpace α
μ : Measure α
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
F : X → α → E
x₀ : X
bound : α → ℝ
hF_meas : ∀ᶠ (x : X) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a
bound_integrable : Integrable bound
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun x => F x a) x₀
⊢ ContinuousAt
    (fun x => if hf : Integrable fun a => F x a then ↑L1.integralCLM (Integrable.toL1 (fun a => F x a) hf) else 0) x₀
exact continuousAt_setToFun_of_dominated (dominatedFinMeasAdditive_weightedSMul μ)
  hF_meas h_bound bound_integrable h_cont