α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ δ
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ TendstoInMeasure μ f atTop g
refine' fun ε hε => ENNReal.tendsto_atTop_zero.mpr fun δ hδ => _
case pos
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
hδi : δ = ⊤
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ δ

case neg
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
hδi : ¬δ = ⊤
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ δ
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ δ
by_cases hδi : δ = ∞
case neg.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : ↑δ > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
case neg
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
hδi : ¬δ = ⊤
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ δ
lift δ to ℝ≥0 using hδi
case neg.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
case neg.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : ↑δ > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
rw [gt_iff_lt, ENNReal.coe_pos, ← NNReal.coe_pos] at hδ
case neg.intro.intro.intro.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ENNReal.ofReal ↑δ
hunif : TendstoUniformlyOn (fun n => f n) g atTop (tᶜ)
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
case neg.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
obtain ⟨t, _, ht, hunif⟩ := tendstoUniformlyOn_of_ae_tendsto' hf hg hfg hδ
case neg.intro.intro.intro.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : TendstoUniformlyOn (fun n => f n) g atTop (tᶜ)
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
case neg.intro.intro.intro.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ENNReal.ofReal ↑δ
hunif : TendstoUniformlyOn (fun n => f n) g atTop (tᶜ)
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
rw [ENNReal.ofReal_coe_nnreal] at ht
case neg.intro.intro.intro.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
case neg.intro.intro.intro.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : TendstoUniformlyOn (fun n => f n) g atTop (tᶜ)
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
rw [Metric.tendstoUniformlyOn_iff] at hunif
case neg.intro.intro.intro.intro.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
case neg.intro.intro.intro.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
obtain ⟨N, hN⟩ := eventually_atTop.1 (hunif ε hε)
case neg.intro.intro.intro.intro.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
⊢ ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
case neg.intro.intro.intro.intro.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
refine' ⟨N, fun n hn => _⟩
case neg.intro.intro.intro.intro.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
this : {x | ε ≤ dist (f n x) (g x)} ⊆ t
⊢ ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ

case this
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
⊢ {x | ε ≤ dist (f n x) (g x)} ⊆ t
case neg.intro.intro.intro.intro.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
⊢ ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ
suffices : { x : α | ε ≤ dist (f n x) (g x) } ⊆ t
case this
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
⊢ {x | ε ≤ dist (f n x) (g x)} ⊆ t
case neg.intro.intro.intro.intro.intro
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
this : {x | ε ≤ dist (f n x) (g x)} ⊆ t
⊢ ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ ↑δ

case this
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
⊢ {x | ε ≤ dist (f n x) (g x)} ⊆ t
exact (measure_mono this).trans ht
case this
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
⊢ tᶜ ⊆ {x | ε ≤ dist (f n x) (g x)}ᶜ
case this
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
⊢ {x | ε ≤ dist (f n x) (g x)} ⊆ t
rw [← Set.compl_subset_compl]
case this
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
x : α
hx : x ∈ tᶜ
⊢ x ∈ {x | ε ≤ dist (f n x) (g x)}ᶜ
case this
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
⊢ tᶜ ⊆ {x | ε ≤ dist (f n x) (g x)}ᶜ
intro x hx
case this
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
x : α
hx : x ∈ tᶜ
⊢ dist (g x) (f n x) < ε
case this
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
x : α
hx : x ∈ tᶜ
⊢ x ∈ {x | ε ≤ dist (f n x) (g x)}ᶜ
rw [Set.mem_compl_iff, Set.nmem_setOf_iff, dist_comm, not_le]
no goals
case this
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < ↑δ
t : Set α
left✝ : MeasurableSet t
ht : ↑↑μ t ≤ ↑δ
hunif : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ℕ) in atTop, ∀ (x : α), x ∈ tᶜ → dist (g x) (f n x) < ε
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x : α), x ∈ tᶜ → dist (g x) (f b x) < ε
n : ℕ
hn : n ≥ N
x : α
hx : x ∈ tᶜ
⊢ dist (g x) (f n x) < ε
exact hN n hn x hx
no goals
case pos
α : Type u_1
ι : Type ?u.3660
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
hδi : δ = ⊤
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → ↑↑μ {x | ε ≤ dist (f n x) (g x)} ≤ δ
simp only [hδi, imp_true_iff, le_top, exists_const]