α : Type u_1
ι : Type ?u.11195
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
n : ℕ
hfg : Tendsto (fun i => ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f i x) (g x)}) atTop (𝓝 0)
⊢ ∃ N, ∀ (m_1 : ℕ), m_1 ≥ N → ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n
α : Type u_1
ι : Type ?u.11195
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ ∃ N, ∀ (m_1 : ℕ), m_1 ≥ N → ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n
specialize hfg ((2⁻¹ : ℝ) ^ n) (by simp only [Real.rpow_nat_cast, inv_pos, zero_lt_two, pow_pos])
α : Type u_1
ι : Type ?u.11195
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
n : ℕ
hfg : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n_1 : ℕ), n_1 ≥ N → ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f n_1 x) (g x)} ≤ ε
⊢ ∃ N, ∀ (m_1 : ℕ), m_1 ≥ N → ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n
α : Type u_1
ι : Type ?u.11195
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
n : ℕ
hfg : Tendsto (fun i => ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f i x) (g x)}) atTop (𝓝 0)
⊢ ∃ N, ∀ (m_1 : ℕ), m_1 ≥ N → ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n
rw [ENNReal.tendsto_atTop_zero] at hfg
no goals
α : Type u_1
ι : Type ?u.11195
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
n : ℕ
hfg : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n_1 : ℕ), n_1 ≥ N → ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f n_1 x) (g x)} ≤ ε
⊢ ∃ N, ∀ (m_1 : ℕ), m_1 ≥ N → ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f m_1 x) (g x)} ≤ 2⁻¹ ^ n
exact hfg ((2 : ℝ≥0∞)⁻¹ ^ n) (pos_iff_ne_zero.mpr fun h_zero => by simpa using pow_eq_zero h_zero)
no goals
α : Type u_1
ι : Type ?u.11195
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n : ℕ
⊢ 0 < 2⁻¹ ^ n
simp only [Real.rpow_nat_cast, inv_pos, zero_lt_two, pow_pos]
no goals
α : Type u_1
ι : Type ?u.11195
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
n : ℕ
hfg : ∀ (ε : ℝ≥0∞), ε > 0 → ∃ N, ∀ (n_1 : ℕ), n_1 ≥ N → ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f n_1 x) (g x)} ≤ ε
h_zero : 2⁻¹ ^ n = 0
⊢ False
simpa using pow_eq_zero h_zero