[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝¹ : MetricSpace β
μ : Measure α
n : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝ : Preorder ι
x : α
⊢ x ∈ notConvergentSeq f g n j ↔ ∃ k x_1, 1 / (↑n + 1) < dist (f k x) (g x)
[PROOFSTEP]
simp_rw [notConvergentSeq, Set.mem_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝¹ : MetricSpace β
μ : Measure α
n : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝ : Preorder ι
x : α
⊢ (∃ i i_1, x ∈ {x | 1 / (↑n + 1) < dist (f i x) (g x)}) ↔ ∃ k x_1, 1 / (↑n + 1) < dist (f k x) (g x)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
⊢ ↑↑μ (s ∩ ⋂ (j : ι), notConvergentSeq f g n j) = 0
[PROOFSTEP]
simp_rw [Metric.tendsto_atTop, ae_iff] at hfg 
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : ↑↑μ {a | ¬(a ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ι), n ≥ N → dist (f n a) (g a) < ε)} = 0
⊢ ↑↑μ (s ∩ ⋂ (j : ι), notConvergentSeq f g n j) = 0
[PROOFSTEP]
rw [← nonpos_iff_eq_zero, ← hfg]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : ↑↑μ {a | ¬(a ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ι), n ≥ N → dist (f n a) (g a) < ε)} = 0
⊢ ↑↑μ (s ∩ ⋂ (j : ι), notConvergentSeq f g n j) ≤
    ↑↑μ {a | ¬(a ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ι), n ≥ N → dist (f n a) (g a) < ε)}
[PROOFSTEP]
refine' measure_mono fun x => _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : ↑↑μ {a | ¬(a ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ι), n ≥ N → dist (f n a) (g a) < ε)} = 0
x : α
⊢ x ∈ s ∩ ⋂ (j : ι), notConvergentSeq f g n j →
    x ∈ {a | ¬(a ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ι), n ≥ N → dist (f n a) (g a) < ε)}
[PROOFSTEP]
simp only [Set.mem_inter_iff, Set.mem_iInter, ge_iff_le, mem_notConvergentSeq_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : ↑↑μ {a | ¬(a ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ι), n ≥ N → dist (f n a) (g a) < ε)} = 0
x : α
⊢ (x ∈ s ∧ ∀ (i : ι), ∃ k x_1, 1 / (↑n + 1) < dist (f k x) (g x)) →
    x ∈ {a | ¬(a ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ι), N ≤ n → dist (f n a) (g a) < ε)}
[PROOFSTEP]
push_neg
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : ↑↑μ {a | ¬(a ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ι), n ≥ N → dist (f n a) (g a) < ε)} = 0
x : α
⊢ (x ∈ s ∧ ∀ (i : ι), ∃ k x_1, 1 / (↑n + 1) < dist (f k x) (g x)) →
    x ∈ {a | a ∈ s ∧ ∃ ε, ε > 0 ∧ ∀ (N : ι), ∃ n, N ≤ n ∧ ε ≤ dist (f n a) (g a)}
[PROOFSTEP]
rintro ⟨hmem, hx⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : ↑↑μ {a | ¬(a ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ι), n ≥ N → dist (f n a) (g a) < ε)} = 0
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k x_1, 1 / (↑n + 1) < dist (f k x) (g x)
⊢ x ∈ {a | a ∈ s ∧ ∃ ε, ε > 0 ∧ ∀ (N : ι), ∃ n, N ≤ n ∧ ε ≤ dist (f n a) (g a)}
[PROOFSTEP]
refine' ⟨hmem, 1 / (n + 1 : ℝ), Nat.one_div_pos_of_nat, fun N => _⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n : ℕ
hfg : ↑↑μ {a | ¬(a ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ι), n ≥ N → dist (f n a) (g a) < ε)} = 0
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k x_1, 1 / (↑n + 1) < dist (f k x) (g x)
N : ι
⊢ ∃ n_1, N ≤ n_1 ∧ 1 / (↑n + 1) ≤ dist (f n_1 x) (g x)
[PROOFSTEP]
obtain ⟨n, hn₁, hn₂⟩ := hx N
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝¹ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n✝ : ℕ
hfg : ↑↑μ {a | ¬(a ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ι), n ≥ N → dist (f n a) (g a) < ε)} = 0
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k x_1, 1 / (↑n✝ + 1) < dist (f k x) (g x)
N n : ι
hn₁ : N ≤ n
hn₂ : 1 / (↑n✝ + 1) < dist (f n x) (g x)
⊢ ∃ n, N ≤ n ∧ 1 / (↑n✝ + 1) ≤ dist (f n x) (g x)
[PROOFSTEP]
exact ⟨n, hn₁, hn₂.le⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
⊢ Tendsto (fun j => ↑↑μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
[PROOFSTEP]
cases' isEmpty_or_nonempty ι with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
⊢ Tendsto (fun j => ↑↑μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
[PROOFSTEP]
have : (fun j => μ (s ∩ notConvergentSeq f g n j)) = fun j => 0 := by simp only [eq_iff_true_of_subsingleton]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
⊢ (fun j => ↑↑μ (s ∩ notConvergentSeq f g n j)) = fun j => 0
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
this : (fun j => ↑↑μ (s ∩ notConvergentSeq f g n j)) = fun j => 0
⊢ Tendsto (fun j => ↑↑μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
[PROOFSTEP]
rw [this]
[GOAL]
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
this : (fun j => ↑↑μ (s ∩ notConvergentSeq f g n j)) = fun j => 0
⊢ Tendsto (fun j => 0) atTop (𝓝 0)
[PROOFSTEP]
exact tendsto_const_nhds
[GOAL]
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : Nonempty ι
⊢ Tendsto (fun j => ↑↑μ (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
[PROOFSTEP]
rw [← measure_inter_notConvergentSeq_eq_zero hfg n, Set.inter_iInter]
[GOAL]
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Countable ι
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
h : Nonempty ι
⊢ Tendsto (fun j => ↑↑μ (s ∩ notConvergentSeq f g n j)) atTop
    (𝓝 (↑↑μ (⋂ (i : ι), s ∩ notConvergentSeq (fun n x => f n x) (fun x => g x) n i)))
[PROOFSTEP]
refine'
  tendsto_measure_iInter (fun n => hsm.inter <| notConvergentSeq_measurableSet hf hg)
    (fun k l hkl => Set.inter_subset_inter_right _ <| notConvergentSeq_antitone hkl)
    ⟨h.some, (lt_of_le_of_lt (measure_mono <| Set.inter_subset_left _ _) (lt_top_iff_ne_top.2 hs)).ne⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
⊢ ∃ j, ↑↑μ (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)
[PROOFSTEP]
have ⟨N, hN⟩ :=
  (ENNReal.tendsto_atTop ENNReal.zero_ne_top).1 (measure_notConvergentSeq_tendsto_zero hf hg hsm hs hfg n)
    (ENNReal.ofReal (ε * 2⁻¹ ^ n))
    (by
      rw [gt_iff_lt, ENNReal.ofReal_pos]
      exact mul_pos hε (pow_pos (by norm_num) n))
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
⊢ ENNReal.ofReal (ε * 2⁻¹ ^ n) > 0
[PROOFSTEP]
rw [gt_iff_lt, ENNReal.ofReal_pos]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
⊢ 0 < ε * 2⁻¹ ^ n
[PROOFSTEP]
exact mul_pos hε (pow_pos (by norm_num) n)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
⊢ 0 < 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
N : ι
hN :
  ∀ (n_1 : ι),
    n_1 ≥ N →
      ↑↑μ (s ∩ notConvergentSeq (fun n => f n) g n n_1) ∈
        Icc (0 - ENNReal.ofReal (ε * 2⁻¹ ^ n)) (0 + ENNReal.ofReal (ε * 2⁻¹ ^ n))
⊢ ∃ j, ↑↑μ (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)
[PROOFSTEP]
rw [zero_add] at hN 
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
N : ι
hN :
  ∀ (n_1 : ι),
    n_1 ≥ N →
      ↑↑μ (s ∩ notConvergentSeq (fun n => f n) g n n_1) ∈
        Icc (0 - ENNReal.ofReal (ε * 2⁻¹ ^ n)) (ENNReal.ofReal (ε * 2⁻¹ ^ n))
⊢ ∃ j, ↑↑μ (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * 2⁻¹ ^ n)
[PROOFSTEP]
exact ⟨N, (hN N le_rfl).2⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ ↑↑μ (iUnionNotConvergentSeq hε hf hg hsm hs hfg) ≤ ENNReal.ofReal ε
[PROOFSTEP]
refine'
  le_trans (measure_iUnion_le _)
    (le_trans (ENNReal.tsum_le_tsum <| notConvergentSeqLTIndex_spec (half_pos hε) hf hg hsm hs hfg) _)
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ ∑' (a : ℕ), ENNReal.ofReal (ε / 2 * 2⁻¹ ^ a) ≤ ENNReal.ofReal ε
[PROOFSTEP]
simp_rw [ENNReal.ofReal_mul (half_pos hε).le]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ ∑' (a : ℕ), ENNReal.ofReal (ε / 2) * ENNReal.ofReal (2⁻¹ ^ a) ≤ ENNReal.ofReal ε
[PROOFSTEP]
rw [ENNReal.tsum_mul_left, ← ENNReal.ofReal_tsum_of_nonneg, inv_eq_one_div, tsum_geometric_two, ←
  ENNReal.ofReal_mul (half_pos hε).le, div_mul_cancel ε two_ne_zero]
[GOAL]
case hf_nonneg
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ ∀ (n : ℕ), 0 ≤ 2⁻¹ ^ n
[PROOFSTEP]
exact fun n => pow_nonneg (by norm_num) _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
n : ℕ
⊢ 0 ≤ 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
case hf
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ Summable fun i => 2⁻¹ ^ i
[PROOFSTEP]
rw [inv_eq_one_div]
[GOAL]
case hf
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ Summable fun i => (1 / 2) ^ i
[PROOFSTEP]
exact summable_geometric_two
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ iUnionNotConvergentSeq hε hf hg hsm hs hfg ⊆ s
[PROOFSTEP]
rw [iUnionNotConvergentSeq, ← Set.inter_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ s ∩ ⋃ (i : ℕ), notConvergentSeq (fun n => f n) g i (notConvergentSeqLTIndex (_ : 0 < ε / 2) hf hg hsm hs hfg i) ⊆ s
[PROOFSTEP]
exact Set.inter_subset_left _ _
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ TendstoUniformlyOn f g atTop (s \ iUnionNotConvergentSeq hε hf hg hsm hs hfg)
[PROOFSTEP]
rw [Metric.tendstoUniformlyOn_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ ∀ (ε_1 : ℝ),
    ε_1 > 0 →
      ∀ᶠ (n : ι) in atTop, ∀ (x : α), x ∈ s \ iUnionNotConvergentSeq hε hf hg hsm hs hfg → dist (g x) (f n x) < ε_1
[PROOFSTEP]
intro δ hδ
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
δ : ℝ
hδ : δ > 0
⊢ ∀ᶠ (n : ι) in atTop, ∀ (x : α), x ∈ s \ iUnionNotConvergentSeq hε hf hg hsm hs hfg → dist (g x) (f n x) < δ
[PROOFSTEP]
obtain ⟨N, hN⟩ := exists_nat_one_div_lt hδ
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
δ : ℝ
hδ : δ > 0
N : ℕ
hN : 1 / (↑N + 1) < δ
⊢ ∀ᶠ (n : ι) in atTop, ∀ (x : α), x ∈ s \ iUnionNotConvergentSeq hε hf hg hsm hs hfg → dist (g x) (f n x) < δ
[PROOFSTEP]
rw [eventually_atTop]
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
δ : ℝ
hδ : δ > 0
N : ℕ
hN : 1 / (↑N + 1) < δ
⊢ ∃ a, ∀ (b : ι), b ≥ a → ∀ (x : α), x ∈ s \ iUnionNotConvergentSeq hε hf hg hsm hs hfg → dist (g x) (f b x) < δ
[PROOFSTEP]
refine' ⟨Egorov.notConvergentSeqLTIndex (half_pos hε) hf hg hsm hs hfg N, fun n hn x hx => _⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
δ : ℝ
hδ : δ > 0
N : ℕ
hN : 1 / (↑N + 1) < δ
n : ι
hn : n ≥ notConvergentSeqLTIndex (_ : 0 < ε / 2) hf hg hsm hs hfg N
x : α
hx : x ∈ s \ iUnionNotConvergentSeq hε hf hg hsm hs hfg
⊢ dist (g x) (f n x) < δ
[PROOFSTEP]
simp only [Set.mem_diff, Egorov.iUnionNotConvergentSeq, not_exists, Set.mem_iUnion, Set.mem_inter_iff, not_and,
  exists_and_left] at hx 
[GOAL]
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
δ : ℝ
hδ : δ > 0
N : ℕ
hN : 1 / (↑N + 1) < δ
n : ι
hn : n ≥ notConvergentSeqLTIndex (_ : 0 < ε / 2) hf hg hsm hs hfg N
x : α
hx :
  x ∈ s ∧
    (x ∈ s →
      ∀ (x_1 : ℕ),
        ¬x ∈ notConvergentSeq (fun n => f n) g x_1 (notConvergentSeqLTIndex (_ : 0 < ε / 2) hf hg hsm hs hfg x_1))
⊢ dist (g x) (f n x) < δ
[PROOFSTEP]
obtain ⟨hxs, hx⟩ := hx
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
δ : ℝ
hδ : δ > 0
N : ℕ
hN : 1 / (↑N + 1) < δ
n : ι
hn : n ≥ notConvergentSeqLTIndex (_ : 0 < ε / 2) hf hg hsm hs hfg N
x : α
hxs : x ∈ s
hx :
  x ∈ s →
    ∀ (x_1 : ℕ),
      ¬x ∈ notConvergentSeq (fun n => f n) g x_1 (notConvergentSeqLTIndex (_ : 0 < ε / 2) hf hg hsm hs hfg x_1)
⊢ dist (g x) (f n x) < δ
[PROOFSTEP]
specialize hx hxs N
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
δ : ℝ
hδ : δ > 0
N : ℕ
hN : 1 / (↑N + 1) < δ
n : ι
hn : n ≥ notConvergentSeqLTIndex (_ : 0 < ε / 2) hf hg hsm hs hfg N
x : α
hxs : x ∈ s
hx : ¬x ∈ notConvergentSeq (fun n => f n) g N (notConvergentSeqLTIndex (_ : 0 < ε / 2) hf hg hsm hs hfg N)
⊢ dist (g x) (f n x) < δ
[PROOFSTEP]
rw [Egorov.mem_notConvergentSeq_iff] at hx 
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
δ : ℝ
hδ : δ > 0
N : ℕ
hN : 1 / (↑N + 1) < δ
n : ι
hn : n ≥ notConvergentSeqLTIndex (_ : 0 < ε / 2) hf hg hsm hs hfg N
x : α
hxs : x ∈ s
hx : ¬∃ k x_1, 1 / (↑N + 1) < dist (f k x) (g x)
⊢ dist (g x) (f n x) < δ
[PROOFSTEP]
push_neg at hx 
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
δ : ℝ
hδ : δ > 0
N : ℕ
hN : 1 / (↑N + 1) < δ
n : ι
hn : n ≥ notConvergentSeqLTIndex (_ : 0 < ε / 2) hf hg hsm hs hfg N
x : α
hxs : x ∈ s
hx : ∀ (k : ι), notConvergentSeqLTIndex (_ : 0 < ε / 2) hf hg hsm hs hfg N ≤ k → dist (f k x) (g x) ≤ 1 / (↑N + 1)
⊢ dist (g x) (f n x) < δ
[PROOFSTEP]
rw [dist_comm]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝³ : MetricSpace β
μ : Measure α
n✝ : ℕ
i j : ι
s : Set α
ε : ℝ
f : ι → α → β
g : α → β
inst✝² : SemilatticeSup ι
inst✝¹ : Nonempty ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hsm : MeasurableSet s
hs : ↑↑μ s ≠ ⊤
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n => f n x) atTop (𝓝 (g x))
δ : ℝ
hδ : δ > 0
N : ℕ
hN : 1 / (↑N + 1) < δ
n : ι
hn : n ≥ notConvergentSeqLTIndex (_ : 0 < ε / 2) hf hg hsm hs hfg N
x : α
hxs : x ∈ s
hx : ∀ (k : ι), notConvergentSeqLTIndex (_ : 0 < ε / 2) hf hg hsm hs hfg N ≤ k → dist (f k x) (g x) ≤ 1 / (↑N + 1)
⊢ dist (f n x) (g x) < δ
[PROOFSTEP]
exact lt_of_le_of_lt (hx n hn) hN
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁵ : MetricSpace β
μ : Measure α
inst✝⁴ : SemilatticeSup ι
inst✝³ : Nonempty ι
inst✝² : Countable ι
γ : Type u_4
inst✝¹ : TopologicalSpace γ
f : ι → α → β
g : α → β
s : Set α
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
⊢ ∃ t, MeasurableSet t ∧ ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ
[PROOFSTEP]
have ⟨t, _, ht, htendsto⟩ :=
  tendstoUniformlyOn_of_ae_tendsto hf hg MeasurableSet.univ (measure_ne_top μ Set.univ)
    (by filter_upwards [hfg] with _ htendsto _ using htendsto) hε
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁵ : MetricSpace β
μ : Measure α
inst✝⁴ : SemilatticeSup ι
inst✝³ : Nonempty ι
inst✝² : Countable ι
γ : Type u_4
inst✝¹ : TopologicalSpace γ
f : ι → α → β
g : α → β
s : Set α
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ → Tendsto (fun n => f n x) atTop (𝓝 (g x))
[PROOFSTEP]
filter_upwards [hfg] with _ htendsto _ using htendsto
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁵ : MetricSpace β
μ : Measure α
inst✝⁴ : SemilatticeSup ι
inst✝³ : Nonempty ι
inst✝² : Countable ι
γ : Type u_4
inst✝¹ : TopologicalSpace γ
f : ι → α → β
g : α → β
s : Set α
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
t : Set α
w✝ : t ⊆ univ
ht : MeasurableSet t
htendsto : ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn (fun n => f n) g atTop (univ \ t)
⊢ ∃ t, MeasurableSet t ∧ ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ
[PROOFSTEP]
refine' ⟨_, ht, _⟩
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁵ : MetricSpace β
μ : Measure α
inst✝⁴ : SemilatticeSup ι
inst✝³ : Nonempty ι
inst✝² : Countable ι
γ : Type u_4
inst✝¹ : TopologicalSpace γ
f : ι → α → β
g : α → β
s : Set α
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
t : Set α
w✝ : t ⊆ univ
ht : MeasurableSet t
htendsto : ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn (fun n => f n) g atTop (univ \ t)
⊢ ↑↑μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ
[PROOFSTEP]
rwa [Set.compl_eq_univ_diff]
