Theorem: Filter.BigO_zero_atZero_of_support_in_Icc (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
⊢ f =O[𝓝[>] 0] fun x => 0
Tactic:
refine Eventually.isBigO ?_
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖f x‖ ≤ 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖f x‖ ≤ 0
Tactic:
filter_upwards [Ioo_mem_nhdsWithin_Ioi' (by linarith : (0 : ℝ) < a)] with c hc
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioo 0 a
⊢ ‖f c‖ ≤ 0

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioo 0 a
⊢ ‖f c‖ ≤ 0
Tactic:
refine norm_le_zero_iff.mpr <| Function.support_subset_iff'.mp fSupp c ?_
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioo 0 a
⊢ c ∉ Icc a b

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioo 0 a
⊢ c ∉ Icc a b
Tactic:
exact fun h ↦ by linarith [mem_Icc.mp h, (mem_Ioo.mp hc).2]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
⊢ 0 < a
Tactic:
linarith
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioo 0 a
h : c ∈ Icc a b
⊢ False
Tactic:
linarith [mem_Icc.mp h, (mem_Ioo.mp hc).2]
State after:
no goals