-- Mathlib/Analysis/Fourier/PoissonSummation.lean
theorem isBigO_norm_Icc_restrict_atTop {f : C(ℝ, E)} {b : ℝ} (hb : 0 < b)
    (hf : f =O[atTop] fun x : ℝ => |x| ^ (-b)) (R S : ℝ) :
    (fun x : ℝ => ‖f.restrict (Icc (x + R) (x + S))‖) =O[atTop] fun x : ℝ => |x| ^ (-b)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), 0 ⊔ -2 * R < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + 0 ⊔ -2 * R ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
⊢ ↑y ≥ d

Tactic:
linarith [hx.1, y.2.1]

Result:
no goals

Proof state:
case h.e'_4.h.e'_6.h.e'_5
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), 0 ⊔ -2 * R < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + 0 ⊔ -2 * R ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ |x| = x

Tactic:
exact abs_of_pos hx'.1

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), 0 ⊔ -2 * R < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + 0 ⊔ -2 * R ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
⊢ 0 ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)

Tactic:
obtain ⟨hx1, hx2⟩ := hx

Result:
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)

Proof state:
case intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), 0 ⊔ -2 * R < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
hc' : IsBigOWith c atTop ⇑f fun x => |x| ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atTop] fun x => |x| ^ (-b)

Tactic:
simp only [IsBigO, IsBigOWith, eventually_atTop] at hc' ⊢

Result:
case intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), 0 ⊔ -2 * R < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
hc' : ∃ a, ∀ b_1 ≥ a, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
⊢ ∃ c a, ∀ b_1 ≥ a, ‖‖ContinuousMap.restrict (Icc (b_1 + R) (b_1 + S)) f‖‖ ≤ c * ‖|b_1| ^ (-b)‖

Proof state:
case h.e'_3.h.e'_5
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), 0 ⊔ -2 * R < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + 0 ⊔ -2 * R ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ |↑y| = ↑y

Tactic:
apply abs_of_nonneg

Result:
case h.e'_3.h.e'_5.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), 0 ⊔ -2 * R < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + 0 ⊔ -2 * R ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ 0 ≤ ↑y

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), 0 ⊔ -2 * R < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + 0 ⊔ -2 * R ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : ↑(Icc (x + R) (x + S))
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ 0 ⊔ -2 * R < x

Tactic:
linarith only [hx.1]

Result:
no goals

Proof state:
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)

Tactic:
rw [← mul_rpow] <;> try positivity

Result:
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ y ^ (-b) ≤ (1 / 2 * x) ^ (-b)

Proof state:
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), 0 ⊔ -2 * R < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + 0 ⊔ -2 * R ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖

Tactic:
rw [norm_norm, ContinuousMap.norm_le _ (by positivity)]

Result:
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), 0 ⊔ -2 * R < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + 0 ⊔ -2 * R ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
⊢ ∀ (x_1 : ↑(Icc (x + R) (x + S))),
    ‖(ContinuousMap.restrict (Icc (x + R) (x + S)) f) x_1‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atTop] fun x => |x| ^ (-b)

Tactic:
have claim : ∀ x : ℝ, max 0 (-2 * R) < x → ∀ y : ℝ, x + R ≤ y →
    y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b) := fun x hx y hy ↦ by
  rw [max_lt_iff] at hx
  obtain ⟨hx1, hx2⟩ := hx
  rw [← mul_rpow] <;> try positivity
  apply rpow_le_rpow_of_nonpos <;> linarith

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), 0 ⊔ -2 * R < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
⊢ (fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atTop] fun x => |x| ^ (-b)

Proof state:
case intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ y ^ (-b) ≤ (1 / 2 * x) ^ (-b)

Tactic:
apply rpow_le_rpow_of_nonpos <;> linarith

Result:
no goals

Proof state:
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), 0 ⊔ -2 * R < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : x ≥ (1 + 0 ⊔ -2 * R) ⊔ (d - R)
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖

Tactic:
rw [ge_iff_le, max_le_iff] at hx

Result:
case intro.intro.intro
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atTop] fun x => |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), 0 ⊔ -2 * R < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + 0 ⊔ -2 * R ≤ x ∧ d - R ≤ x
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖