Theorem: TendstoUniformlyOn.integral_tendsto
Proof state before:
case intro.intro
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ Tendsto (fun n => ∫ (x : X) in s, f n x) atTop (𝓝 (∫ (x : X) in s, g x))
Tactic:
apply tendsto_integral_of_dominated_convergence (F := f) (f := g) (fun _ ↦ b)
Proof state after:
case intro.intro.F_measurable
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ (n : ℕ), AEStronglyMeasurable (f n) (volume.restrict s)

case intro.intro.bound_integrable
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ Integrable (fun x => b) (volume.restrict s)

case intro.intro.h_bound
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ (n : ℕ), ∀ᵐ (a : X) ∂volume.restrict s, ‖f n a‖ ≤ b

case intro.intro.h_lim
E : Type
inst✝¹⁴ : NormedAddCommGroup E
inst✝¹³ : NormedSpace ℝ E
inst✝¹² : CompleteSpace E
inst✝¹¹ : SecondCountableTopology E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
X : Type
inst✝⁷ : MeasureSpace X
inst✝⁶ : MetricSpace X
inst✝⁵ : BorelSpace X
Y : Type
inst✝⁴ : MeasureSpace Y
inst✝³ : MetricSpace Y
inst✝² : BorelSpace Y
A : Type
inst✝¹ : TopologicalSpace A
f : ℕ → X → E
g : X → E
s : Set X
inst✝ : IsLocallyFiniteMeasure volume
u : TendstoUniformlyOn f g atTop s
fc : ∀ (n : ℕ), ContinuousOn (f n) s
sc : IsCompact s
b : ℝ
left✝ : 0 ≤ b
bh : ∀ (n : ℕ), ∀ x ∈ s, ‖f n x‖ ≤ b
⊢ ∀ᵐ (a : X) ∂volume.restrict s, Tendsto (fun n => f n a) atTop (𝓝 (g a))