α : Type u_2
E : Type u_1
F : Type ?u.1273109
𝕜 : Type ?u.1273112
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.1275803
inst✝⁴ : TopologicalSpace X
inst✝³ : FirstCountableTopology X
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
s : Set E
inst✝ : SeparableSpace ↑s
hfi : Integrable f
hfm : Measurable f
hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s
y₀ : E
h₀ : y₀ ∈ s
h₀i : Integrable fun x => y₀
hfi' : ∀ (n : ℕ), Integrable ↑(approxOn f hfm s y₀ h₀ n)
⊢ Tendsto (fun n => SimpleFunc.integral μ (approxOn f hfm s y₀ h₀ n)) atTop (𝓝 (∫ (x : α), f x ∂μ))
α : Type u_2
E : Type u_1
F : Type ?u.1273109
𝕜 : Type ?u.1273112
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.1275803
inst✝⁴ : TopologicalSpace X
inst✝³ : FirstCountableTopology X
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
s : Set E
inst✝ : SeparableSpace ↑s
hfi : Integrable f
hfm : Measurable f
hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s
y₀ : E
h₀ : y₀ ∈ s
h₀i : Integrable fun x => y₀
⊢ Tendsto (fun n => SimpleFunc.integral μ (approxOn f hfm s y₀ h₀ n)) atTop (𝓝 (∫ (x : α), f x ∂μ))
have hfi' := SimpleFunc.integrable_approxOn hfm hfi h₀ h₀i
α : Type u_2
E : Type u_1
F : Type ?u.1273109
𝕜 : Type ?u.1273112
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.1275803
inst✝⁴ : TopologicalSpace X
inst✝³ : FirstCountableTopology X
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
s : Set E
inst✝ : SeparableSpace ↑s
hfi : Integrable f
hfm : Measurable f
hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s
y₀ : E
h₀ : y₀ ∈ s
h₀i : Integrable fun x => y₀
hfi' : ∀ (n : ℕ), Integrable ↑(approxOn f hfm s y₀ h₀ n)
⊢ Tendsto
    (fun n =>
      if hf : Integrable fun x => ↑(approxOn f hfm s y₀ h₀ n) x then
        ↑L1.integralCLM (Integrable.toL1 (fun x => ↑(approxOn f hfm s y₀ h₀ n) x) hf)
      else 0)
    atTop (𝓝 (if hf : Integrable fun x => f x then ↑L1.integralCLM (Integrable.toL1 (fun x => f x) hf) else 0))
α : Type u_2
E : Type u_1
F : Type ?u.1273109
𝕜 : Type ?u.1273112
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.1275803
inst✝⁴ : TopologicalSpace X
inst✝³ : FirstCountableTopology X
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
s : Set E
inst✝ : SeparableSpace ↑s
hfi : Integrable f
hfm : Measurable f
hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s
y₀ : E
h₀ : y₀ ∈ s
h₀i : Integrable fun x => y₀
hfi' : ∀ (n : ℕ), Integrable ↑(approxOn f hfm s y₀ h₀ n)
⊢ Tendsto (fun n => SimpleFunc.integral μ (approxOn f hfm s y₀ h₀ n)) atTop (𝓝 (∫ (x : α), f x ∂μ))
simp only [SimpleFunc.integral_eq_integral _ (hfi' _), integral, L1.integral]
no goals
α : Type u_2
E : Type u_1
F : Type ?u.1273109
𝕜 : Type ?u.1273112
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.1275803
inst✝⁴ : TopologicalSpace X
inst✝³ : FirstCountableTopology X
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
s : Set E
inst✝ : SeparableSpace ↑s
hfi : Integrable f
hfm : Measurable f
hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s
y₀ : E
h₀ : y₀ ∈ s
h₀i : Integrable fun x => y₀
hfi' : ∀ (n : ℕ), Integrable ↑(approxOn f hfm s y₀ h₀ n)
⊢ Tendsto
    (fun n =>
      if hf : Integrable fun x => ↑(approxOn f hfm s y₀ h₀ n) x then
        ↑L1.integralCLM (Integrable.toL1 (fun x => ↑(approxOn f hfm s y₀ h₀ n) x) hf)
      else 0)
    atTop (𝓝 (if hf : Integrable fun x => f x then ↑L1.integralCLM (Integrable.toL1 (fun x => f x) hf) else 0))
exact tendsto_setToFun_approxOn_of_measurable (dominatedFinMeasAdditive_weightedSMul μ)
  hfi hfm hs h₀ h₀i