awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, Norm.norm (E := E) ((f : (a : ℝ) → E) b_1 : E) ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : (↑(Icc (x + R) (x + S)) : Type)
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
rw : |(↑y : ℝ)| ^ (-b) ≤ (1 / 2) ^ (-b) * |x| ^ (-b)
⊢ c * ‖|(↑y : ℝ)| ^ (-b)‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖

Tactic:
rw [mul_assoc, mul_le_mul_iff_right₀ hc, norm_of_nonneg (A _), norm_of_nonneg (A _)]

Premises used: mul_assoc, Real.norm_of_nonneg, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, Norm.norm (E := E) ((f : (a : ℝ) → E) b_1 : E) ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : (↑(Icc (x + R) (x + S)) : Type)
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
linarith : x ≤ max 0 (-2 * R) → -1 + (x - max 0 (-2 * R)) + (1 + max 0 (-2 * R) - x) = 0
⊢ max 0 (-2 * R) < x

Tactic:
linarith only [hx.1]

Premises used: And.left
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, Norm.norm (E := E) ((f : (a : ℝ) → E) b_1 : E) ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : (↑(Icc (x + R) (x + S)) : Type)
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
h : |(↑y : ℝ)| = (↑y : ℝ)
h₁ : |x| = x
⊢ |(↑y : ℝ)| ^ (-b) ≤ (1 / 2) ^ (-b) * |x| ^ (-b)

Tactic:
convert! claim x (by linarith only [hx.1]) y.1 y.2.1

Premises used: And.left, Subtype.val, Subtype.property
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, Norm.norm (E := E) ((f : (a : ℝ) → E) b_1 : E) ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : (↑(Icc (x + R) (x + S)) : Type)
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
h : 0 ≤ (↑y : ℝ)
⊢ |(↑y : ℝ)| = (↑y : ℝ)

Tactic:
apply abs_of_nonneg

Premises used: abs_of_nonneg
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, Norm.norm (E := E) ((f : (a : ℝ) → E) b_1 : E) ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : (↑(Icc (x + R) (x + S)) : Type)
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
linarith : (↑y : ℝ) < 0 → 0 - x + (-2 * R - x) + 2 * ((↑y : ℝ) - 0) + 2 * (x + R - (↑y : ℝ)) = 0
linarith₁ linarith₂ : (↑y : ℝ) < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ (↑y : ℝ)

Tactic:
linarith [y.2.1]

Premises used: And.left, Subtype.property
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, Norm.norm (E := E) ((f : (a : ℝ) → E) b_1 : E) ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : (↑(Icc (x + R) (x + S)) : Type)
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ |x| = x

Tactic:
abs_of_pos hx'.1

Premises used: And.left, abs_of_pos
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
c : ℝ
hc : c > 0
d : ℝ
hd : ∀ b_1 ≥ d, Norm.norm (E := E) ((f : (a : ℝ) → E) b_1 : E) ≤ c * ‖|b_1| ^ (-b)‖
x : ℝ
hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
hx' : 0 < x ∧ -2 * R < x
y : (↑(Icc (x + R) (x + S)) : Type)
A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
⊢ |x| = x

Tactic:
exact abs_of_pos hx'.1

Premises used: And.left, abs_of_pos
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
⊢ IsBigO (α := ℝ) (E := E) (F := ℝ) atTop ((⇑f : (a : ℝ) → E) ∘ Neg.neg) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg)

Tactic:
hf.comp_tendsto tendsto_neg_atTop_atBot

Premises used: Filter.tendsto_neg_atTop_atBot, Asymptotics.IsBigO.comp_tendsto
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h : Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ |x| ^ (-b)) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg)
⊢ IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)

Tactic:
convert! hf.comp_tendsto tendsto_neg_atTop_atBot using 1

Premises used: Filter.tendsto_neg_atTop_atBot, Asymptotics.IsBigO.comp_tendsto
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h : ∀ (x : ℝ), |x| ^ (-b) = ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) x
⊢ Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ |x| ^ (-b)) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg)

Tactic:
ext1 x
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x : ℝ
⊢ |x| ^ (-b) = ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) x

Tactic:
simp only [Function.comp_apply, abs_neg]

Premises used: abs_neg, Function.comp_apply
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
⊢ IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)

Tactic:
have h1 : (f.comp (ContinuousMap.mk _ continuous_neg)) =O[atTop] fun x : ℝ => |x| ^ (-b) := by
    convert! hf.comp_tendsto tendsto_neg_atTop_atBot using 1
    ext1 x; simp only [Function.comp_apply, abs_neg]
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h1 :
  IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
⊢ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg)

Tactic:
have h2 := (isBigO_norm_Icc_restrict_atTop hb h1 (-S) (-R)).comp_tendsto tendsto_neg_atBot_atTop
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h1 :
  IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
h2 :
  IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg)
h : ∀ (x : ℝ), ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) x = |x| ^ (-b)
⊢ Eq (α := ℝ → ℝ) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ (-b)

Tactic:
ext1 x
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h1 :
  IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
h2 :
  IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg)
x : ℝ
⊢ ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) x = |x| ^ (-b)

Tactic:
simp only [Function.comp_apply, abs_neg]

Premises used: abs_neg, Function.comp_apply
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h1 :
  IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
h2 :
  IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg)
⊢ Eq (α := ℝ → ℝ) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ (-b)

Tactic:
have : (fun x : ℝ => |x| ^ (-b)) ∘ Neg.neg = fun x : ℝ => |x| ^ (-b) := by
    ext1 x; simp only [Function.comp_apply, abs_neg]
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h1 :
  IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
h2 :
  IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg)
this : Eq (α := ℝ → ℝ) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ (-b)
⊢ IsBigO (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    fun (x : ℝ) ↦ |x| ^ (-b)

Tactic:
rw [this] at h2
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h1 :
  IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
h2 :
  IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg)
this : Eq (α := ℝ → ℝ) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ (-b)
h2₁ :
  IsBigO (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    fun (x : ℝ) ↦ |x| ^ (-b)
⊢ Eq (α := ℝ → ℝ) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ (-b)

Tactic:
rw [this] at h2
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h1 :
  IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
h2 :
  IsBigO (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    fun (x : ℝ) ↦ |x| ^ (-b)
this : Eq (α := ℝ → ℝ) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ (-b)
⊢ IsBigO (E := ℝ) (F := ℝ) atBot (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) fun (x : ℝ) ↦
    |x| ^ (-b)

Tactic:
(isBigO_of_le _ fun x => ?_).trans h2

Premises used: Asymptotics.IsBigO.trans, Asymptotics.isBigO_of_le
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h1 :
  IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
h2 :
  IsBigO (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    fun (x : ℝ) ↦ |x| ^ (-b)
this : Eq (α := ℝ → ℝ) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ (-b)
refine :
  ∀ (x : ℝ),
    ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤
      Norm.norm (E := ℝ)
        (((fun (x : ℝ) ↦
              ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
                  (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
            Neg.neg)
          x)
⊢ IsBigO (E := ℝ) (F := ℝ) atBot (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) fun (x : ℝ) ↦
    |x| ^ (-b)

Tactic:
refine (isBigO_of_le _ fun x => ?_).trans h2

Premises used: Asymptotics.IsBigO.trans, Asymptotics.isBigO_of_le
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h1 :
  IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
h2 :
  IsBigO (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    fun (x : ℝ) ↦ |x| ^ (-b)
this : Eq (α := ℝ → ℝ) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ (-b)
x : ℝ
rw :
  ∀ (x_1 : (↑(Icc (x + R) (x + S)) : Type)),
    Norm.norm (E := E)
        ((ContinuousMap.restrict (Icc (x + R) (x + S)) f : (a : (↑(Icc (x + R) (x + S)) : Type)) → E) x_1 : E) ≤
      ‖ContinuousMap.restrict (Icc (-x + -S) (-x + -R))
          (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤
    Norm.norm (E := ℝ)
      (((fun (x : ℝ) ↦
            ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
                (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
          Neg.neg)
        x)

Tactic:
rw [norm_norm, Function.comp_apply, norm_norm, ContinuousMap.norm_le _ (norm_nonneg _)]

Premises used: ContinuousMap.norm_le, norm_norm, Function.comp_apply, norm_nonneg
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h1 :
  IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
h2 :
  IsBigO (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    fun (x : ℝ) ↦ |x| ^ (-b)
this : Eq (α := ℝ → ℝ) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ (-b)
x_1 x : ℝ
hx : x ∈ Icc (x_1 + R) (x_1 + S)
rw :
  Norm.norm (E := E) ((f : (a : ℝ) → E) x : E) ≤
    ‖ContinuousMap.restrict (Icc (-x_1 + -S) (-x_1 + -R))
        (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖
⊢ Norm.norm (E := E)
      ((ContinuousMap.restrict (Icc (x_1 + R) (x_1 + S)) f : (a : (↑(Icc (x_1 + R) (x_1 + S)) : Type)) → E)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (x_1 + R) (x_1 + S)) x hx) :
        E) ≤
    ‖ContinuousMap.restrict (Icc (-x_1 + -S) (-x_1 + -R))
        (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖

Tactic:
rw [ContinuousMap.restrict_apply_mk]

Premises used: ContinuousMap.restrict_apply_mk
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h1 :
  IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
h2 :
  IsBigO (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    fun (x : ℝ) ↦ |x| ^ (-b)
this : Eq (α := ℝ → ℝ) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ (-b)
x_1 x : ℝ
hx : x ∈ Icc (x_1 + R) (x_1 + S)
⊢ Norm.norm (E := E) ((f : (a : ℝ) → E) x : E) ≤
    ‖ContinuousMap.restrict (Icc (-x_1 + -S) (-x_1 + -R))
        (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖

Tactic:
(le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨-x, ?_⟩)

Premises used: ContinuousMap.norm_coe_le_norm, LE.le.trans, le_of_eq
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h1 :
  IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
h2 :
  IsBigO (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    fun (x : ℝ) ↦ |x| ^ (-b)
this : Eq (α := ℝ → ℝ) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ (-b)
x_1 x : ℝ
hx : x ∈ Icc (x_1 + R) (x_1 + S)
refine_1 :
  Norm.norm (E := E) ((f : (a : ℝ) → E) x : E) =
    Norm.norm (E := E)
      ((ContinuousMap.restrict (Icc (-x_1 + -S) (-x_1 + -R))
              (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) :
            (a : (↑(Icc (-x_1 + -S) (-x_1 + -R)) : Type)) → E)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (-x_1 + -S) (-x_1 + -R)) (-x) ⋯) :
        E)
refine_2 : -x ∈ Icc (-x_1 + -S) (-x_1 + -R)
⊢ Norm.norm (E := E) ((f : (a : ℝ) → E) x : E) ≤
    ‖ContinuousMap.restrict (Icc (-x_1 + -S) (-x_1 + -R))
        (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖

Tactic:
refine (le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨-x, ?_⟩)

Premises used: ContinuousMap.norm_coe_le_norm, LE.le.trans, le_of_eq
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h1 :
  IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
h2 :
  IsBigO (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    fun (x : ℝ) ↦ |x| ^ (-b)
this : Eq (α := ℝ → ℝ) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ (-b)
x_1 x : ℝ
hx : x ∈ Icc (x_1 + R) (x_1 + S)
refine_1 :
  Norm.norm (E := E) ((f : (a : ℝ) → E) x : E) =
    Norm.norm (E := E) ((f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) } : (a : ℝ) → E) (-x) : E)
refine_1₁ :
  Norm.norm (E := E) ((f : (a : ℝ) → E) x : E) =
    Norm.norm (E := E)
      ((f : (a : ℝ) → E) (({ toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ } : (a : ℝ) → ℝ) (-x) : ℝ) : E)
refine_1₂ :
  ‖f.toFun x‖ = ‖f.toFun (({ toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) } : (a : ℝ) → ℝ) (-x))‖
refine_1₃ : ‖f.toFun x‖ = ‖f.toFun (- -x)‖
refine_1₄ refine_1₅ : ‖f.toFun x‖ = ‖f.toFun x‖
⊢ Norm.norm (E := E) ((f : (a : ℝ) → E) x : E) =
    Norm.norm (E := E)
      ((ContinuousMap.restrict (Icc (-x_1 + -S) (-x_1 + -R))
              (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) :
            (a : (↑(Icc (-x_1 + -S) (-x_1 + -R)) : Type)) → E)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (-x_1 + -S) (-x_1 + -R)) (-x) ⋯) :
        E)

Tactic:
rw [ContinuousMap.restrict_apply_mk, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
      ContinuousMap.coe_mk, neg_neg]

Premises used: neg_neg, ContinuousMap.comp_apply, ContinuousMap.coe_mk, ContinuousMap.restrict_apply_mk
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h1 :
  IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
h2 :
  IsBigO (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    fun (x : ℝ) ↦ |x| ^ (-b)
this : Eq (α := ℝ → ℝ) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ (-b)
x_1 x : ℝ
hx : x ∈ Icc (x_1 + R) (x_1 + S)
linarith : -x < -x_1 + -S → -x - (-x_1 + -S) + (x - (x_1 + S)) = 0
⊢ -x_1 + -S ≤ -x

Tactic:
linarith [hx.2]

Premises used: And.right
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
h1 :
  IsBigO (E := E) (F := ℝ) atTop
    (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) }) : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
h2 :
  IsBigO (E := ℝ) (F := ℝ) atBot
    ((fun (x : ℝ) ↦
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
            (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := ⋯ : C(ℝ, ℝ) })‖) ∘
      Neg.neg)
    fun (x : ℝ) ↦ |x| ^ (-b)
this : Eq (α := ℝ → ℝ) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ (-b)
x_1 x : ℝ
hx : x ∈ Icc (x_1 + R) (x_1 + S)
linarith : -x_1 + -R < -x → -x_1 + -R - -x + (x_1 + R - x) = 0
⊢ -x ≤ -x_1 + -R

Tactic:
linarith [hx.1]

Premises used: And.left