Theorem: WI_sum_Iab_le (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b
Tactic:
have hb' : 0 < 2 / b := by positivity
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b
Tactic:
have hx : 0 < x := by linarith
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b
Tactic:
have hxb' : 2 < x * b := (div_lt_iff hb).mp hxb
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b
Tactic:
have l1 (i : ℕ) (hi : i ∉ Finset.range ⌈b * x⌉₊) : f i * indicator (Ico a b) 1 (i / x) = 0 := by
  simp at hi ⊢ ; right ; rintro - ; rw [le_div_iff hx] ; linarith
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b
Tactic:
have l2 (i : ℕ) (_ : i ∈ Finset.range ⌈b * x⌉₊) : f i * indicator (Ico a b) 1 (i / x) ≤ |f i| := by
  rw [abs_eq_self.mpr (hpos _)]
  convert_to _ ≤ f i * 1 ; ring
  apply mul_le_mul_of_nonneg_left ?_ (hpos _)
  by_cases hi : (i / x) ∈ (Ico a b) <;> simp [hi]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x ≤ C * 2 * b
Tactic:
rw [tsum_eq_sum l1, div_le_iff hx, mul_assoc, mul_assoc]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
⊢ ∑ b_1 ∈ Finset.range ⌈b * x⌉₊, f b_1 * (Ico a b).indicator 1 (↑b_1 / x) ≤ C * (2 * (b * x))

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
⊢ ∑ b_1 ∈ Finset.range ⌈b * x⌉₊, f b_1 * (Ico a b).indicator 1 (↑b_1 / x) ≤ C * (2 * (b * x))
Tactic:
apply Finset.sum_le_sum l2 |>.trans
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
⊢ ∑ i ∈ Finset.range ⌈b * x⌉₊, |f i| ≤ C * (2 * (b * x))

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
⊢ ∑ i ∈ Finset.range ⌈b * x⌉₊, |f i| ≤ C * (2 * (b * x))
Tactic:
have := hcheby ⌈b * x⌉₊
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this : cumsum (fun x => ‖(fun n => ↑(f n)) x‖) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
⊢ ∑ i ∈ Finset.range ⌈b * x⌉₊, |f i| ≤ C * (2 * (b * x))

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this : cumsum (fun x => ‖(fun n => ↑(f n)) x‖) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
⊢ ∑ i ∈ Finset.range ⌈b * x⌉₊, |f i| ≤ C * (2 * (b * x))
Tactic:
simp at this
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
⊢ ∑ i ∈ Finset.range ⌈b * x⌉₊, |f i| ≤ C * (2 * (b * x))

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
⊢ ∑ i ∈ Finset.range ⌈b * x⌉₊, |f i| ≤ C * (2 * (b * x))
Tactic:
apply this.trans
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
⊢ C * ↑⌈b * x⌉₊ ≤ C * (2 * (b * x))

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
⊢ C * ↑⌈b * x⌉₊ ≤ C * (2 * (b * x))
Tactic:
have : 0 ≤ C := by have := hcheby 1 ; simp only [cumsum, Finset.range_one, Complex.norm_eq_abs,
  abs_ofReal, Finset.sum_singleton, Nat.cast_one, mul_one] at this ; exact (abs_nonneg _).trans this
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this✝ : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
this : 0 ≤ C
⊢ C * ↑⌈b * x⌉₊ ≤ C * (2 * (b * x))

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this✝ : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
this : 0 ≤ C
⊢ C * ↑⌈b * x⌉₊ ≤ C * (2 * (b * x))
Tactic:
refine mul_le_mul_of_nonneg_left ?_ this
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this✝ : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
this : 0 ≤ C
⊢ ↑⌈b * x⌉₊ ≤ 2 * (b * x)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this✝ : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
this : 0 ≤ C
⊢ ↑⌈b * x⌉₊ ≤ 2 * (b * x)
Tactic:
apply (Nat.ceil_lt_add_one (by positivity)).le.trans
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this✝ : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
this : 0 ≤ C
⊢ b * x + 1 ≤ 2 * (b * x)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this✝ : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
this : 0 ≤ C
⊢ b * x + 1 ≤ 2 * (b * x)
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
⊢ 0 < 2 / b
Tactic:
positivity
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
⊢ 0 < x
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
i : ℕ
hi : i ∉ Finset.range ⌈b * x⌉₊
⊢ f i * (Ico a b).indicator 1 (↑i / x) = 0
Tactic:
simp at hi ⊢
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
i : ℕ
hi : b * x ≤ ↑i
⊢ f i = 0 ∨ (a ≤ ↑i / x → b ≤ ↑i / x)

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
i : ℕ
hi : b * x ≤ ↑i
⊢ f i = 0 ∨ (a ≤ ↑i / x → b ≤ ↑i / x)
Tactic:
right
State after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
i : ℕ
hi : b * x ≤ ↑i
⊢ a ≤ ↑i / x → b ≤ ↑i / x

State before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
i : ℕ
hi : b * x ≤ ↑i
⊢ a ≤ ↑i / x → b ≤ ↑i / x
Tactic:
rintro -
State after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
i : ℕ
hi : b * x ≤ ↑i
⊢ b ≤ ↑i / x

State before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
i : ℕ
hi : b * x ≤ ↑i
⊢ b ≤ ↑i / x
Tactic:
rw [le_div_iff hx]
State after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
i : ℕ
hi : b * x ≤ ↑i
⊢ b * x ≤ ↑i

State before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
i : ℕ
hi : b * x ≤ ↑i
⊢ b * x ≤ ↑i
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
i : ℕ
x✝ : i ∈ Finset.range ⌈b * x⌉₊
⊢ f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
Tactic:
rw [abs_eq_self.mpr (hpos _)]
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
i : ℕ
x✝ : i ∈ Finset.range ⌈b * x⌉₊
⊢ f i * (Ico a b).indicator 1 (↑i / x) ≤ f i

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
i : ℕ
x✝ : i ∈ Finset.range ⌈b * x⌉₊
⊢ f i * (Ico a b).indicator 1 (↑i / x) ≤ f i
Tactic:
convert_to _ ≤ f i * 1
State after:
case h.e'_4
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
i : ℕ
x✝ : i ∈ Finset.range ⌈b * x⌉₊
⊢ f i = f i * 1

case convert_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
i : ℕ
x✝ : i ∈ Finset.range ⌈b * x⌉₊
⊢ f i * (Ico a b).indicator 1 (↑i / x) ≤ f i * 1

State before:
case h.e'_4
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
i : ℕ
x✝ : i ∈ Finset.range ⌈b * x⌉₊
⊢ f i = f i * 1

case convert_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
i : ℕ
x✝ : i ∈ Finset.range ⌈b * x⌉₊
⊢ f i * (Ico a b).indicator 1 (↑i / x) ≤ f i * 1
Tactic:
ring
State after:
case convert_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
i : ℕ
x✝ : i ∈ Finset.range ⌈b * x⌉₊
⊢ f i * (Ico a b).indicator 1 (↑i / x) ≤ f i * 1

State before:
case convert_2
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
i : ℕ
x✝ : i ∈ Finset.range ⌈b * x⌉₊
⊢ f i * (Ico a b).indicator 1 (↑i / x) ≤ f i * 1
Tactic:
apply mul_le_mul_of_nonneg_left ?_ (hpos _)
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
i : ℕ
x✝ : i ∈ Finset.range ⌈b * x⌉₊
⊢ (Ico a b).indicator 1 (↑i / x) ≤ 1

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
i : ℕ
x✝ : i ∈ Finset.range ⌈b * x⌉₊
⊢ (Ico a b).indicator 1 (↑i / x) ≤ 1
Tactic:
by_cases hi : (i / x) ∈ (Ico a b) <;> simp [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 : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
⊢ 0 ≤ C
Tactic:
have := hcheby 1
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this✝ : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
this : cumsum (fun x => ‖(fun n => ↑(f n)) x‖) 1 ≤ C * ↑1
⊢ 0 ≤ C

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this✝ : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
this : cumsum (fun x => ‖(fun n => ↑(f n)) x‖) 1 ≤ C * ↑1
⊢ 0 ≤ C
Tactic:
simp only [cumsum, Finset.range_one, Complex.norm_eq_abs,
abs_ofReal, Finset.sum_singleton, Nat.cast_one, mul_one] at this
State after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this✝ : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
this : |f 0| ≤ C
⊢ 0 ≤ C

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this✝ : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
this : |f 0| ≤ C
⊢ 0 ≤ C
Tactic:
exact (abs_nonneg _).trans this
State after:
no goals

State before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
C : ℝ
hcheby : chebyWith C fun n => ↑(f n)
hb : 0 < b
hxb : 2 / b < x
hb' : 0 < 2 / b
hx : 0 < x
hxb' : 2 < x * b
l1 : ∀ i ∉ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) = 0
l2 : ∀ i ∈ Finset.range ⌈b * x⌉₊, f i * (Ico a b).indicator 1 (↑i / x) ≤ |f i|
this✝ : cumsum (fun x => |f x|) ⌈b * x⌉₊ ≤ C * ↑⌈b * x⌉₊
this : 0 ≤ C
⊢ 0 ≤ b * x
Tactic:
positivity
State after:
no goals