Theorem: tsum_indicator (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
⊢ ∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x) = ∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n
Tactic:
have l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * indicator (Ico a b) 1 (↑n / x) = 0 := by
  simp [mem_Ico_iff_div hx] ; tauto
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x) = ∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x) = ∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n
Tactic:
rw [tsum_eq_sum l1]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∑ b_1 ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f b_1 * (Ico a b).indicator 1 (↑b_1 / x) =
    ∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∑ b_1 ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f b_1 * (Ico a b).indicator 1 (↑b_1 / x) =
    ∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n
Tactic:
apply Finset.sum_congr rfl
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∀ x_1 ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f x_1 * (Ico a b).indicator 1 (↑x_1 / x) = f x_1

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∀ x_1 ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f x_1 * (Ico a b).indicator 1 (↑x_1 / x) = f x_1
Tactic:
simp only [mem_Ico_iff_div hx]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∀ (x_1 : ℕ), ↑x_1 / x ∈ Ico a b → f x_1 * (Ico a b).indicator 1 (↑x_1 / x) = f x_1

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∀ (x_1 : ℕ), ↑x_1 / x ∈ Ico a b → f x_1 * (Ico a b).indicator 1 (↑x_1 / x) = f x_1
Tactic:
intro n hn
State after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
n : ℕ
hn : ↑n / x ∈ Ico a b
⊢ f n * (Ico a b).indicator 1 (↑n / x) = f n

State before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
n : ℕ
hn : ↑n / x ∈ Ico a b
⊢ f n * (Ico a b).indicator 1 (↑n / x) = f n
Tactic:
simp [hn]
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
⊢ ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
Tactic:
simp [mem_Ico_iff_div hx]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
⊢ ∀ (n : ℕ), (a ≤ ↑n / x → b ≤ ↑n / x) → f n = 0 ∨ (a ≤ ↑n / x → b ≤ ↑n / x)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
⊢ ∀ (n : ℕ), (a ≤ ↑n / x → b ≤ ↑n / x) → f n = 0 ∨ (a ≤ ↑n / x → b ≤ ↑n / x)
Tactic:
tauto
State after:
no goals