case zero
α : Type u_1
ι : Type ?u.17265
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k : ℕ
hn : seqTendstoAeSeq hfg Nat.zero ≤ k
⊢ ↑↑μ {x | 2⁻¹ ^ Nat.zero ≤ dist (f k x) (g x)} ≤ 2⁻¹ ^ Nat.zero

case succ
α : Type u_1
ι : Type ?u.17265
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k n✝ : ℕ
hn : seqTendstoAeSeq hfg (Nat.succ n✝) ≤ k
⊢ ↑↑μ {x | 2⁻¹ ^ Nat.succ n✝ ≤ dist (f k x) (g x)} ≤ 2⁻¹ ^ Nat.succ n✝
α : Type u_1
ι : Type ?u.17265
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
n k : ℕ
hn : seqTendstoAeSeq hfg n ≤ k
⊢ ↑↑μ {x | 2⁻¹ ^ n ≤ dist (f k x) (g x)} ≤ 2⁻¹ ^ n
cases n
no goals
case zero
α : Type u_1
ι : Type ?u.17265
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k : ℕ
hn : seqTendstoAeSeq hfg Nat.zero ≤ k
⊢ ↑↑μ {x | 2⁻¹ ^ Nat.zero ≤ dist (f k x) (g x)} ≤ 2⁻¹ ^ Nat.zero
exact Classical.choose_spec (exists_nat_measure_lt_two_inv hfg 0) k hn
no goals
case succ
α : Type u_1
ι : Type ?u.17265
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : MetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
k n✝ : ℕ
hn : seqTendstoAeSeq hfg (Nat.succ n✝) ≤ k
⊢ ↑↑μ {x | 2⁻¹ ^ Nat.succ n✝ ≤ dist (f k x) (g x)} ≤ 2⁻¹ ^ Nat.succ n✝
exact Classical.choose_spec
  (exists_nat_measure_lt_two_inv hfg _) _ (le_trans (le_max_left _ _) hn)