gcongr
case neg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf0 : f 0 = 0
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
ggg : ℕ → ℝ := fun i => if i = 0 then 1 else gg x ↑i
l0 : x ≠ 0
l1 : ∀ (i : ℕ), 0 ≤ ggg i
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ x⁻¹ * hh (1 / (2 * π)) (↑j / x) ≤ x⁻¹ * hh (1 / (2 * π)) (↑i / x)
case neg.h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf0 : f 0 = 0
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
ggg : ℕ → ℝ := fun i => if i = 0 then 1 else gg x ↑i
l0 : x ≠ 0
l1 : ∀ (i : ℕ), 0 ≤ ggg i
i j : ℕ
hij : i ≤ j
hi : ¬i = 0
hj : ¬j = 0
⊢ hh (1 / (2 * π)) (↑j / x) ≤ hh (1 / (2 * π)) (↑i / x)