Theorem: Filter.TendstoAtZero_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
⊢ Tendsto f (𝓝[>] 0) (𝓝 0)
Tactic:
apply Tendsto.comp (tendsto_nhds_of_eventually_eq ?_) tendsto_id
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' ha] 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:
replace hc := (mem_Ioo.mp hc).2
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 < 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 < a
⊢ f c = 0
Tactic:
have h : c ∉ Icc a b := fun h ↦ by linarith [mem_Icc.mp h]
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 < a
h : c ∉ Icc a b
⊢ 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 < a
h : c ∉ Icc a b
⊢ f c = 0
Tactic:
convert mt (Function.support_subset_iff.mp fSupp c) h
State after:
case a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c < a
h : c ∉ Icc a b
⊢ f c = 0 ↔ ¬f c ≠ 0

State before:
case a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c < a
h : c ∉ Icc a b
⊢ f c = 0 ↔ ¬f c ≠ 0
Tactic:
simp
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 < a
h : c ∈ Icc a b
⊢ False
Tactic:
linarith [mem_Icc.mp h]
State after:
no goals