α : Type u_2
β : Type u_1
ι : Type ?u.15743
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ Set.indicator {x | ↑n ≤ ↑‖f x‖₊} f x = 0
α : Type u_2
β : Type u_1
ι : Type ?u.15743
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
x : α
⊢ Tendsto (fun M => Set.indicator {x | ↑M ≤ ↑‖f x‖₊} f x) atTop (𝓝 0)
refine' tendsto_atTop_of_eventually_const (i₀ := Nat.ceil (‖f x‖₊ : ℝ) + 1) fun n hn => _
case h
α : Type u_2
β : Type u_1
ι : Type ?u.15743
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ ¬x ∈ {x | ↑n ≤ ↑‖f x‖₊}
α : Type u_2
β : Type u_1
ι : Type ?u.15743
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ Set.indicator {x | ↑n ≤ ↑‖f x‖₊} f x = 0
rw [Set.indicator_of_not_mem]
case h
α : Type u_2
β : Type u_1
ι : Type ?u.15743
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ ↑‖f x‖₊ < ↑n
case h
α : Type u_2
β : Type u_1
ι : Type ?u.15743
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ ¬x ∈ {x | ↑n ≤ ↑‖f x‖₊}
simp only [not_le, Set.mem_setOf_eq]
case h
α : Type u_2
β : Type u_1
ι : Type ?u.15743
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ ↑⌈↑‖f x‖₊⌉₊ < ↑n
case h
α : Type u_2
β : Type u_1
ι : Type ?u.15743
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ ↑‖f x‖₊ < ↑n
refine' lt_of_le_of_lt (Nat.le_ceil _) _
case h
α : Type u_2
β : Type u_1
ι : Type ?u.15743
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ ↑⌈↑‖f x‖₊⌉₊ + 1 ≤ ↑n
case h
α : Type u_2
β : Type u_1
ι : Type ?u.15743
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ ↑⌈↑‖f x‖₊⌉₊ < ↑n
refine' lt_of_lt_of_le (lt_add_one _) _
no goals
case h
α : Type u_2
β : Type u_1
ι : Type ?u.15743
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈↑‖f x‖₊⌉₊ + 1
⊢ ↑⌈↑‖f x‖₊⌉₊ + 1 ≤ ↑n
norm_cast