Theorem: WI_summable (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
⊢ Summable fun n => f n * g (↑n / x)
Tactic:
obtain ⟨M, hM⟩ := hg.bddAbove.mono subset_closure
State after:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ Summable fun n => f n * g (↑n / x)

State before:
case intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ Summable fun n => f n * g (↑n / x)
Tactic:
apply summable_of_finite_support
State after:
case intro.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ (Function.support fun n => f n * g (↑n / x)).Finite

State before:
case intro.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ (Function.support fun n => f n * g (↑n / x)).Finite
Tactic:
simp only [Function.support_mul]
State after:
case intro.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ ((Function.support fun x => f x) ∩ Function.support fun x_1 => g (↑x_1 / x)).Finite

State before:
case intro.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ ((Function.support fun x => f x) ∩ Function.support fun x_1 => g (↑x_1 / x)).Finite
Tactic:
apply Finite.inter_of_right
State after:
case intro.h.hs
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ (Function.support fun x_1 => g (↑x_1 / x)).Finite

State before:
case intro.h.hs
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ (Function.support fun x_1 => g (↑x_1 / x)).Finite
Tactic:
rw [finite_iff_bddAbove]
State after:
case intro.h.hs
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ BddAbove (Function.support fun x_1 => g (↑x_1 / x))

State before:
case intro.h.hs
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ BddAbove (Function.support fun x_1 => g (↑x_1 / x))
Tactic:
exact ⟨Nat.ceil (M * x), fun i hi => by simpa using Nat.ceil_mono ((div_le_iff hx).mp (hM hi))⟩
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
i : ℕ
hi : i ∈ Function.support fun x_1 => g (↑x_1 / x)
⊢ i ≤ ⌈M * x⌉₊
Tactic:
simpa using Nat.ceil_mono ((div_le_iff hx).mp (hM hi))
State after:
no goals