awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
h_sum : Summable (α := ℂ) fun (n : ℤ) ↦ 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ)
x : ℝ
F : C(UnitAddCircle, ℂ) :=
  {
    toFun :=
      Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯,
    continuous_toFun := ⋯ }
x_1 : ℤ
⊢ fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ) x_1 = 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑x_1 : ℝ)

Tactic:
exact Real.fourierCoeff_tsum_comp_add h_norm _

Premises used: Real.fourierCoeff_tsum_comp_add
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
h_sum : Summable (α := ℂ) fun (n : ℤ) ↦ 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ)
x : ℝ
F : C(UnitAddCircle, ℂ) :=
  {
    toFun :=
      Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯,
    continuous_toFun := ⋯ }
⊢ Summable (α := ℂ) (fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ))

Tactic:
have : Summable (fourierCoeff F) := by
    convert! h_sum
    exact Real.fourierCoeff_tsum_comp_add h_norm _
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
h_sum : Summable (α := ℂ) fun (n : ℤ) ↦ 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ)
x : ℝ
F : C(UnitAddCircle, ℂ) :=
  {
    toFun :=
      Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯,
    continuous_toFun := ⋯ }
this : Summable (α := ℂ) (fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ))
⊢ Eq (α := ℂ) ((F : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
    (∑' (b : ℤ),
        HSMul.hSMul (α := ℂ) (β := ℂ) (fourierCoeff (T := 1) (⇑F : (a : AddCircle 1) → ℂ) b)
          ((fourier b : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ) :
      ℂ)

Tactic:
(has_pointwise_sum_fourier_series_of_summable this x).tsum_eq.symm

Premises used: has_pointwise_sum_fourier_series_of_summable, QuotientAddGroup.mk, HasSum.tsum_eq, Eq.symm
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
h_sum : Summable (α := ℂ) fun (n : ℤ) ↦ 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ)
x : ℝ
F : C(UnitAddCircle, ℂ) :=
  {
    toFun :=
      Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯,
    continuous_toFun := ⋯ }
this : Summable (α := ℂ) (fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ))
h :
  Eq (α := ℂ) (∑' (n : ℤ), (f : (a : ℝ) → ℂ) (x + (↑n : ℝ)) : ℂ)
    ((F : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
h₁ :
  Eq (α := ℂ)
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ) (𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ))
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (∑' (b : ℤ),
      HSMul.hSMul (α := ℂ) (β := ℂ) (fourierCoeff (T := 1) (⇑F : (a : AddCircle 1) → ℂ) b)
        ((fourier b : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
⊢ Eq (α := ℂ) (∑' (n : ℤ), (f : (a : ℝ) → ℂ) (x + (↑n : ℝ)))
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ) (𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ))
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))

Tactic:
convert! (has_pointwise_sum_fourier_series_of_summable this x).tsum_eq.symm using 1

Premises used: has_pointwise_sum_fourier_series_of_summable, QuotientAddGroup.mk, HasSum.tsum_eq, Eq.symm
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
h_sum : Summable (α := ℂ) fun (n : ℤ) ↦ 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ)
x : ℝ
F : C(UnitAddCircle, ℂ) :=
  {
    toFun :=
      Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯,
    continuous_toFun := ⋯ }
this : Summable (α := ℂ) (fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ))
⊢ Eq (α := ℂ) (∑' (n : ℤ), (f : (a : ℝ) → ℂ) (x + (↑n : ℝ)) : ℂ)
    ((F : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)

Tactic:
simpa only [F, coe_mk, ← QuotientAddGroup.mk_zero, Periodic.lift_coe, zsmul_one, comp_apply,
      coe_addRight, zero_add]
       using (hasSum_apply (summable_of_locally_summable_norm h_norm).hasSum x).tsum_eq

Premises used: ContinuousMap.coe_addRight, ContinuousMap.summable_of_locally_summable_norm, ContinuousMap.hasSum_apply, ContinuousMap.comp_apply, zero_add, HasSum.tsum_eq, QuotientAddGroup.mk_zero, Summable.hasSum, ContinuousMap.coe_mk, Function.Periodic.lift_coe, zsmul_one
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : C(ℝ, ℂ)
h_norm :
  ∀ (K : Compacts ℝ),
    Summable (α := ℝ) fun (n : ℤ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight (↑n : ℝ)))‖
h_sum : Summable (α := ℂ) fun (n : ℤ) ↦ 𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ)
x : ℝ
F : C(UnitAddCircle, ℂ) :=
  {
    toFun :=
      Periodic.lift (f := (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯,
    continuous_toFun := ⋯ }
this : Summable (α := ℂ) (fourierCoeff (T := 1) (⇑F : (a : UnitAddCircle) → ℂ))
h :
  Eq (α := ℂ)
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ)
        (fourierCoeff (T := 1)
          (Periodic.lift (f :=
            (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯)
          n)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (∑' (b : ℤ),
      HSMul.hSMul (α := ℂ) (β := ℂ) (fourierCoeff (T := 1) (⇑F : (a : AddCircle 1) → ℂ) b)
        ((fourier b : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
h₁ :
  Eq (α := ℂ)
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ)
        (fourierCoeff (T := 1)
          (Periodic.lift (f :=
            (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯)
          n)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (∑' (b : ℤ),
      HMul.hMul (α := ℂ) (β := ℂ) (fourierCoeff (T := 1) (⇑F : (a : AddCircle 1) → ℂ) b : ℂ)
        ((fourier b : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
h₂ :
  Eq (α := ℂ)
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ)
        (fourierCoeff (T := 1)
          (Periodic.lift (f :=
            (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯)
          n)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (∑' (b : ℤ),
      HMul.hMul (α := ℂ) (β := ℂ)
        (fourierCoeff (T := 1)
            (⇑{
                  toFun :=
                    Periodic.lift (f :=
                      (⇑(∑' (n : ℤ), f.comp (ContinuousMap.addRight (HSMul.hSMul (β := ℝ) n 1))) : (a : ℝ) → ℂ)) ⋯,
                  continuous_toFun := ⋯ } :
              (a : AddCircle 1) → ℂ)
            b :
          ℂ)
        ((fourier b : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
⊢ Eq (α := ℂ)
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ) (𝓕 (E := (a : ℝ) → ℂ) (⇑f : (a : ℝ) → ℂ) (↑n : ℝ))
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))
    (∑' (b : ℤ),
      HSMul.hSMul (α := ℂ) (β := ℂ) (fourierCoeff (T := 1) (⇑F : (a : AddCircle 1) → ℂ) b)
        ((fourier b : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))

Tactic:
simp_rw [← Real.fourierCoeff_tsum_comp_add h_norm, smul_eq_mul, F, coe_mk]

Premises used: Real.fourierCoeff_tsum_comp_add, ContinuousMap.coe_mk, smul_eq_mul
-- 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 x : ℝ
hx : max 0 (-2 * R) < x
y : ℝ
hy : x + R ≤ y
rw : ∀ (hx : 0 < x ∧ -2 * R < x) (y : ℝ) (hy : x + R ≤ y), y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)

Tactic:
rw [max_lt_iff] at hx

Premises used: max_lt_iff
-- 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 x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
⊢ 0 < x

Tactic:
obtain ⟨hx1, hx2⟩ := hx
-- 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 x : ℝ
hx : 0 < x ∧ -2 * R < x
y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
⊢ -2 * R < x

Tactic:
obtain ⟨hx1, hx2⟩ := hx
-- 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 x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
rw : y ^ (-b) ≤ (1 / 2 * x) ^ (-b)
hx : 0 ≤ 1 / 2
hy₁ : 0 ≤ x
⊢ y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)

Tactic:
rw [← mul_rpow]

Premises used: Real.mul_rpow
-- 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 x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 0 ≤ 1 / 2

Tactic:
positivity
-- 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 x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 0 ≤ 1 / 2

Tactic:
try positivity
-- 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 x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 0 ≤ x

Tactic:
positivity
-- 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 x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ 0 ≤ x

Tactic:
try positivity
-- 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 x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
hx : 0 < 1 / 2 * x
hxy : 1 / 2 * x ≤ y
hz : -b ≤ 0
⊢ y ^ (-b) ≤ (1 / 2 * x) ^ (-b)

Tactic:
apply rpow_le_rpow_of_nonpos

Premises used: Real.rpow_le_rpow_of_nonpos
-- 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 x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
linarith : 1 / 2 * x ≤ 0 → 2 / 2 = 1
linarith₁ : 1 / 2 * x ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 / 2 * x ≤ 0 → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : 1 / 2 * x ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₄ : 1 / 2 * x ≤ 0 → 0 - x + (HMul.hMul (α := ℝ) 1 1 * (1 * x) - HMul.hMul (α := ℝ) 2 0) = 0
⊢ 0 < 1 / 2 * x

Tactic:
linarith
-- 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 x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
linarith : y < 1 / 2 * x → 2 / 2 = 1
linarith₁ : y < 1 / 2 * x → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : y < 1 / 2 * x → HMul.hMul (α := ℝ) 2 1 = 2
linarith₃ : y < 1 / 2 * x → GT.gt (α := ℝ) 2 0
linarith₄ : y < 1 / 2 * x → 2 * (x + R - y) + (-2 * R - x) + (2 * y - HMul.hMul (α := ℝ) 1 1 * (1 * x)) = 0
linarith₅ : y < 1 / 2 * x → GT.gt (α := ℝ) 2 0
⊢ 1 / 2 * x ≤ y

Tactic:
linarith
-- 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 x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
linarith : 0 < -b → 0 - b + (0 - -b) = 0
⊢ -b ≤ 0

Tactic:
linarith
-- 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 : ℝ
⊢ ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * 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
-- 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)
obtain :
  ∀ (c : ℝ) (hc : c > 0) (hc' : IsBigOWith (E := E) (F := ℝ) c atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)),
    IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) fun (x : ℝ) ↦
      |x| ^ (-b)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) fun (x : ℝ) ↦
    |x| ^ (-b)

Tactic:
obtain ⟨c, hc, hc'⟩ := hf.exists_pos

Premises used: Asymptotics.IsBigO.exists_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
hc' : IsBigOWith (E := E) (F := ℝ) c atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
simp :
  ∀ (hc' : ∃ (a : ℝ), ∀ b_1 ≥ a, Norm.norm (E := E) ((f : (a : ℝ) → E) b_1 : E) ≤ c * ‖|b_1| ^ (-b)‖),
    ∃ (c : ℝ) (a : ℝ), ∀ b_1 ≥ a, ‖‖ContinuousMap.restrict (Icc (b_1 + R) (b_1 + S)) f‖‖ ≤ c * ‖|b_1| ^ (-b)‖
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) fun (x : ℝ) ↦
    |x| ^ (-b)

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

Premises used: Asymptotics.IsBigOWith, Asymptotics.IsBigO, Filter.eventually_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 := ℝ) 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
hc' : ∃ (a : ℝ), ∀ b_1 ≥ a, Norm.norm (E := E) ((f : (a : ℝ) → E) b_1 : E) ≤ c * ‖|b_1| ^ (-b)‖
obtain :
  ∀ (d : ℝ) (hd : ∀ b_1 ≥ d, Norm.norm (E := E) ((f : (a : ℝ) → E) b_1 : E) ≤ c * ‖|b_1| ^ (-b)‖),
    ∃ (c : ℝ) (a : ℝ), ∀ b_1 ≥ a, ‖‖ContinuousMap.restrict (Icc (b_1 + R) (b_1 + S)) f‖‖ ≤ c * ‖|b_1| ^ (-b)‖
⊢ ∃ (c : ℝ) (a : ℝ), ∀ b_1 ≥ a, ‖‖ContinuousMap.restrict (Icc (b_1 + R) (b_1 + S)) f‖‖ ≤ c * ‖|b_1| ^ (-b)‖

Tactic:
obtain ⟨d, hd⟩ := hc'
-- 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)‖
⊢ ∃ (c : ℝ) (a : ℝ), ∀ b_1 ≥ a, ‖‖ContinuousMap.restrict (Icc (b_1 + R) (b_1 + S)) f‖‖ ≤ c * ‖|b_1| ^ (-b)‖

Tactic:
⟨c * (1 / 2) ^ (-b), ⟨max (1 + max 0 (-2 * R)) (d - R), fun x hx => ?_⟩⟩

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, HPow.hPow, HAdd.hAdd, Max.max, Exists.intro, OfNat.ofNat, Neg.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 := ℝ) 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)‖
refine :
  ∀ (x : ℝ) (hx : x ≥ max (1 + max 0 (-2 * R)) (d - R)),
    ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
⊢ ∃ (c : ℝ) (a : ℝ), ∀ b_1 ≥ a, ‖‖ContinuousMap.restrict (Icc (b_1 + R) (b_1 + S)) f‖‖ ≤ c * ‖|b_1| ^ (-b)‖

Tactic:
refine ⟨c * (1 / 2) ^ (-b), ⟨max (1 + max 0 (-2 * R)) (d - R), fun x hx => ?_⟩⟩
-- 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 : x ≥ max (1 + max 0 (-2 * R)) (d - R)
⊢ 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x

Tactic:
rw [ge_iff_le, max_le_iff] at hx

Premises used: ge_iff_le, max_le_iff
-- 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
linarith : x ≤ max 0 (-2 * R) → -1 + (1 + max 0 (-2 * R) - x) + (x - max 0 (-2 * R)) = 0
⊢ max 0 (-2 * R) < x

Tactic:
linarith
-- 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
⊢ max 0 (-2 * R) < x

Tactic:
have hx' : max 0 (-2 * R) < x := by linarith
-- 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' : max 0 (-2 * R) < x
⊢ 0 < x ∧ -2 * R < x

Tactic:
rw [max_lt_iff] at hx'

Premises used: max_lt_iff
-- 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
⊢ 0 ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖

Tactic:
positivity
-- 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
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) ≤
      c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖

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

Premises used: ContinuousMap.norm_le, norm_norm
-- 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)
linarith : (↑y : ℝ) < d → d - R - x + ((↑y : ℝ) - d) + (x + R - (↑y : ℝ)) = 0
⊢ (↑y : ℝ) ≥ d

Tactic:
linarith [hx.1, 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
refine : ∀ (y : (↑(Icc (x + R) (x + S)) : Type)), c * ‖|(↑y : ℝ)| ^ (-b)‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
⊢ ∀ (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) ≤
      c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖

Tactic:
refine fun y => (hd y.1 (by linarith [hx.1, y.2.1])).trans ?_

Premises used: LE.le.trans
-- 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_1 : ℝ
hx : 1 + max 0 (-2 * R) ≤ x_1 ∧ d - R ≤ x_1
hx' : 0 < x_1 ∧ -2 * R < x_1
y : (↑(Icc (x_1 + R) (x_1 + S)) : Type)
x : ℝ
⊢ 0 ≤ |x| ^ (-b)

Tactic:
positivity
-- 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)
⊢ ∀ (x : ℝ), 0 ≤ |x| ^ (-b)

Tactic:
have A : ∀ x : ℝ, 0 ≤ |x| ^ (-b) := fun x => by positivity