α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ ∀ (x : ℕ → ι), Tendsto x atTop l → Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Tendsto (fun n => ∫⁻ (a : α), F n a ∂μ) l (𝓝 (∫⁻ (a : α), f a ∂μ))
rw [tendsto_iff_seq_tendsto]
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
⊢ Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ ∀ (x : ℕ → ι), Tendsto x atTop l → Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
intro x xl
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
⊢ Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
⊢ Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
have hxl := by
  rw [tendsto_atTop'] at xl
  exact xl
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
h : {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x} ∈ l
⊢ Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
⊢ Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
have h := inter_mem hF_meas h_bound
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
h :
  ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
h : {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x} ∈ l
⊢ Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
replace h := hxl _ h
case intro
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
h :
  ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
rcases h with ⟨k, h⟩
case intro
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ Tendsto (fun n => ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) (n + k)) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
case intro
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ Tendsto ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
rw [← tendsto_add_atTop_iff_nat k]
case intro.refine'_1
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ α → ℝ≥0∞

case intro.refine'_2
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ ∀ (n : ℕ), Measurable fun a => F (x (n + k)) a

case intro.refine'_3
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ ∀ (n : ℕ), (fun a => F (x (n + k)) a) ≤ᵐ[μ] ?intro.refine'_1

case intro.refine'_4
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ (∫⁻ (a : α), ?intro.refine'_1 a ∂μ) ≠ ⊤

case intro.refine'_5
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F (x (n + k)) a) atTop (𝓝 (f a))
case intro
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ Tendsto (fun n => ((fun n => ∫⁻ (a : α), F n a ∂μ) ∘ x) (n + k)) atTop (𝓝 (∫⁻ (a : α), f a ∂μ))
refine' tendsto_lintegral_of_dominated_convergence _ _ _ _ _
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl✝ : Tendsto x atTop l
xl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
⊢ ?m.1003992
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
⊢ ?m.1003992
rw [tendsto_atTop'] at xl
no goals
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl✝ : Tendsto x atTop l
xl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
⊢ ?m.1003992
exact xl
no goals
case intro.refine'_1
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ α → ℝ≥0∞
exact bound
case intro.refine'_2
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
n✝ : ℕ
⊢ Measurable fun a => F (x (n✝ + k)) a
case intro.refine'_2
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ ∀ (n : ℕ), Measurable fun a => F (x (n + k)) a
intro
case intro.refine'_2
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
n✝ : ℕ
⊢ n✝ + k ≥ k
case intro.refine'_2
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
n✝ : ℕ
⊢ Measurable fun a => F (x (n✝ + k)) a
refine' (h _ _).1
no goals
case intro.refine'_2
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
n✝ : ℕ
⊢ n✝ + k ≥ k
exact Nat.le_add_left _ _
case intro.refine'_3
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
n✝ : ℕ
⊢ (fun a => F (x (n✝ + k)) a) ≤ᵐ[μ] bound
case intro.refine'_3
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ ∀ (n : ℕ), (fun a => F (x (n + k)) a) ≤ᵐ[μ] bound
intro
case intro.refine'_3
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
n✝ : ℕ
⊢ n✝ + k ≥ k
case intro.refine'_3
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
n✝ : ℕ
⊢ (fun a => F (x (n✝ + k)) a) ≤ᵐ[μ] bound
refine' (h _ _).2
no goals
case intro.refine'_3
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
n✝ : ℕ
⊢ n✝ + k ≥ k
exact Nat.le_add_left _ _
no goals
case intro.refine'_4
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
assumption
case intro.refine'_5
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim✝ : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
a : α
h_lim : Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Tendsto (fun n => F (x (n + k)) a) atTop (𝓝 (f a))
case intro.refine'_5
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F (x (n + k)) a) atTop (𝓝 (f a))
refine' h_lim.mono fun a h_lim => _
case intro.refine'_5.hg
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim✝ : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
a : α
h_lim : Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Tendsto (fun n => F n a) ?intro.refine'_5.y (𝓝 (f a))

case intro.refine'_5.hf
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim✝ : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
a : α
h_lim : Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Tendsto (fun n => x (n + k)) atTop ?intro.refine'_5.y

case intro.refine'_5.y
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim✝ : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
a : α
h_lim : Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Filter ι
case intro.refine'_5
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim✝ : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
a : α
h_lim : Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Tendsto (fun n => F (x (n + k)) a) atTop (𝓝 (f a))
apply @Tendsto.comp _ _ _ (fun n => x (n + k)) fun n => F n a
case intro.refine'_5.hf
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim✝ : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
a : α
h_lim : Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Tendsto x atTop l
case intro.refine'_5.hf
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim✝ : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
a : α
h_lim : Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Tendsto (fun n => x (n + k)) atTop l
rw [tendsto_add_atTop_iff_nat]
no goals
case intro.refine'_5.hf
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim✝ : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
a : α
h_lim : Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Tendsto x atTop l
assumption
no goals
case intro.refine'_5.hg
α : Type u_2
β : Type ?u.1003459
γ : Type ?u.1003462
δ : Type ?u.1003465
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
l : Filter ι
inst✝ : IsCountablyGenerated l
F : ι → α → ℝ≥0∞
f bound : α → ℝ≥0∞
hF_meas : ∀ᶠ (n : ι) in l, Measurable (F n)
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, F n a ≤ bound a
h_fin : (∫⁻ (a : α), bound a ∂μ) ≠ ⊤
h_lim✝ : ∀ᵐ (a : α) ∂μ, Tendsto (fun n => F n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ (s : Set ι), s ∈ l → ∃ a, ∀ (b : ℕ), b ≥ a → x b ∈ s
k : ℕ
h : ∀ (b : ℕ), b ≥ k → x b ∈ {x | (fun n => Measurable (F n)) x} ∩ {x | (fun n => ∀ᵐ (a : α) ∂μ, F n a ≤ bound a) x}
a : α
h_lim : Tendsto (fun n => F n a) l (𝓝 (f a))
⊢ Tendsto (fun n => F n a) ?intro.refine'_5.y (𝓝 (f a))
assumption