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 := ℝ) 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)
⊢ -x ∈ Icc (-x_1 + -S) (-x_1 + -R)

Tactic:
exact ⟨by linarith [hx.2], by linarith [hx.1]⟩
-- 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 := ℝ) (cocompact ℝ) (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
K : Compacts ℝ
obtain :
  ∀ (r : ℝ) (hr : (↑K : Set ℝ) ⊆ Metric.closedBall 0 r),
    IsBigO (E := ℝ) (F := ℝ) (cocompact ℝ)
      (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)
⊢ IsBigO (E := ℝ) (F := ℝ) (cocompact ℝ)
    (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)

Tactic:
obtain ⟨r, hr⟩ := K.isCompact.isBounded.subset_closedBall 0

Premises used: IsCompact.isBounded, Bornology.IsBounded.subset_closedBall, TopologicalSpace.Compacts.isCompact, OfNat.ofNat
-- 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 := ℝ) (cocompact ℝ) (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Metric.closedBall 0 r
⊢ (↑K : Set ℝ) ⊆ Icc (-r) r

Tactic:
rw [closedBall_eq_Icc, zero_add, zero_sub] at hr

Premises used: Real.closedBall_eq_Icc, zero_add, zero_sub
-- 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 := ℝ) (cocompact ℝ) (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
x : ℝ
rw :
  ∀ (x_1 : (↑(↑K : Set ℝ) : Type)),
    Norm.norm (E := E)
        ((ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x)) : (a : (↑(↑K : Set ℝ) : Type)) → E)
            x_1 :
          E) ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
⊢ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
    ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖

Tactic:
rw [ContinuousMap.norm_le _ (norm_nonneg _)]

Premises used: ContinuousMap.norm_le, 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 := ℝ) (cocompact ℝ) (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ (↑K : Set ℝ)
⊢ Norm.norm (E := E)
      ((ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x)) : (a : (↑(↑K : Set ℝ) : Type)) → E)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ (↑K : Set ℝ)) y hy) :
        E) ≤
    ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖

Tactic:
(le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨y + 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 := ℝ) (cocompact ℝ) (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ (↑K : Set ℝ)
refine_1 :
  Norm.norm (E := E)
      ((ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x)) : (a : (↑(↑K : Set ℝ) : Type)) → E)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ (↑K : Set ℝ)) y hy) :
        E) =
    Norm.norm (E := E)
      ((ContinuousMap.restrict (Icc (x - r) (x + r)) f : (a : (↑(Icc (x - r) (x + r)) : Type)) → E)
          (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc (x - r) (x + r)) (y + x) ⋯) :
        E)
refine_2 : y + x ∈ Icc (x - r) (x + r)
⊢ Norm.norm (E := E)
      ((ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x)) : (a : (↑(↑K : Set ℝ) : Type)) → E)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ (↑K : Set ℝ)) y hy) :
        E) ≤
    ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖

Tactic:
refine (le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨y + 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 := ℝ) (cocompact ℝ) (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ (↑K : Set ℝ)
refine_1 :
  Norm.norm (E := E) ((f.comp (ContinuousMap.addRight x) : (a : ℝ) → E) y : E) =
    Norm.norm (E := E) ((f : (a : ℝ) → E) (y + x) : E)
refine_1₁ :
  Norm.norm (E := E) ((f : (a : ℝ) → E) ((ContinuousMap.addRight x : (a : ℝ) → ℝ) y : ℝ) : E) =
    Norm.norm (E := E) ((f : (a : ℝ) → E) (y + x) : E)
⊢ Norm.norm (E := E)
      ((ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x)) : (a : (↑(↑K : Set ℝ) : Type)) → E)
          (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ (↑K : Set ℝ)) y hy) :
        E) =
    Norm.norm (E := E)
      ((ContinuousMap.restrict (Icc (x - r) (x + r)) f : (a : (↑(Icc (x - r) (x + r)) : Type)) → E)
          (Subtype.mk (p := fun (x_1 : ℝ) ↦ x_1 ∈ Icc (x - r) (x + r)) (y + x) ⋯) :
        E)

Tactic:
simp_rw [ContinuousMap.restrict_apply, ContinuousMap.comp_apply, ContinuousMap.coe_addRight]

Premises used: ContinuousMap.coe_addRight, ContinuousMap.comp_apply, ContinuousMap.restrict_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 := ℝ) (cocompact ℝ) (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ (↑K : Set ℝ)
linarith : y + x < x - r → y + x - (x - r) + (-r - y) = 0
⊢ x - r ≤ y + x

Tactic:
linarith [(hr hy).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 := ℝ) (cocompact ℝ) (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ (↑K : Set ℝ)
linarith : x + r < y + x → x + r - (y + x) + (y - r) = 0
⊢ y + x ≤ x + r

Tactic:
linarith [(hr hy).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 := ℝ) (cocompact ℝ) (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
x y : ℝ
hy : y ∈ (↑K : Set ℝ)
⊢ y + x ∈ Icc (x - r) (x + r)

Tactic:
exact ⟨by linarith [(hr hy).1], by linarith [(hr hy).2]⟩
-- 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 := ℝ) (cocompact ℝ) (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
⊢ ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖

Tactic:
have : ∀ x : ℝ,
      ‖(f.comp (ContinuousMap.addRight x)).restrict K‖ ≤ ‖f.restrict (Icc (x - r) (x + r))‖ := by
    intro x
    rw [ContinuousMap.norm_le _ (norm_nonneg _)]
    rintro ⟨y, hy⟩
    refine (le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨y + x, ?_⟩)
    · simp_rw [ContinuousMap.restrict_apply, ContinuousMap.comp_apply, ContinuousMap.coe_addRight]
    · exact ⟨by linarith [(hr hy).1], by linarith [(hr hy).2]⟩
-- 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 := ℝ) (cocompact ℝ) (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
simp_rw :
  ∀
    (hf :
      (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
        IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)),
    (IsBigO (E := ℝ) (F := ℝ) atBot
        (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦
        |x| ^ (-b)) ∧
      IsBigO (E := ℝ) (F := ℝ) atTop
        (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦
        |x| ^ (-b)
⊢ IsBigO (E := ℝ) (F := ℝ) (cocompact ℝ)
    (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)

Tactic:
simp_rw [cocompact_eq_atBot_atTop, isBigO_sup] at hf ⊢

Premises used: cocompact_eq_atBot_atTop, Asymptotics.isBigO_sup
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf :
  (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
    IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
left :
  IsBigO (E := ℝ) (F := ℝ) atBot
    (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)
right :
  IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)
⊢ (IsBigO (E := ℝ) (F := ℝ) atBot
      (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦
      |x| ^ (-b)) ∧
    IsBigO (E := ℝ) (F := ℝ) atTop
      (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)

Tactic:
constructor
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf :
  (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
    IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
⊢ IsBigO (E := ℝ) (F := ℝ) atBot
    (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)

Tactic:
(isBigO_of_le atBot ?_).trans (isBigO_norm_Icc_restrict_atBot hb hf.1 (-r) r)

Premises used: Asymptotics.IsBigO.trans, And.left, isBigO_norm_Icc_restrict_atBot, Filter.atBot, Asymptotics.isBigO_of_le, Neg.neg
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf :
  (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
    IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
left :
  ∀ (x : ℝ),
    ‖‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖‖ ≤
      ‖‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖‖
⊢ IsBigO (E := ℝ) (F := ℝ) atBot
    (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)

Tactic:
refine (isBigO_of_le atBot ?_).trans (isBigO_norm_Icc_restrict_atBot hb hf.1 (-r) r)

Premises used: Asymptotics.IsBigO.trans, And.left, isBigO_norm_Icc_restrict_atBot, Filter.atBot, Asymptotics.isBigO_of_le, Neg.neg
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf :
  (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
    IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
left :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖
⊢ ∀ (x : ℝ),
    ‖‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖‖ ≤
      ‖‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖‖

Tactic:
simp_rw [norm_norm]

Premises used: norm_norm
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf :
  (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
    IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
⊢ ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖

Tactic:
this

Premises used: setOf
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf :
  (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
    IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
⊢ ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖

Tactic:
exact this
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf :
  (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
    IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)

Tactic:
(isBigO_of_le atTop ?_).trans (isBigO_norm_Icc_restrict_atTop hb hf.2 (-r) r)

Premises used: isBigO_norm_Icc_restrict_atTop, Asymptotics.IsBigO.trans, Filter.atTop, And.right, Asymptotics.isBigO_of_le, Neg.neg
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf :
  (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
    IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
right :
  ∀ (x : ℝ),
    ‖‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖‖ ≤
      ‖‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖‖
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)

Tactic:
refine (isBigO_of_le atTop ?_).trans (isBigO_norm_Icc_restrict_atTop hb hf.2 (-r) r)

Premises used: isBigO_norm_Icc_restrict_atTop, Asymptotics.IsBigO.trans, Filter.atTop, And.right, Asymptotics.isBigO_of_le, Neg.neg
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
K : Compacts ℝ
r : ℝ
hr : (↑K : Set ℝ) ⊆ Icc (-r) r
this :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x - r) (x + r)) f‖
hf :
  (IsBigO (E := E) (F := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)) ∧
    IsBigO (E := E) (F := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
right :
  ∀ (x : ℝ),
    ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖ ≤
      ‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖
⊢ ∀ (x : ℝ),
    ‖‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖‖ ≤
      ‖‖ContinuousMap.restrict (Icc (x + -r) (x + r)) f‖‖

Tactic:
simp_rw [norm_norm]

Premises used: norm_norm
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : ℝ → ℂ
hc : Continuous f
b : ℝ
hb : 1 < b
hf : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ |x| ^ (-b)
hFf : Summable (α := ℂ) fun (n : ℤ) ↦ 𝓕 f (↑n : ℝ)
x : ℝ
⊢ Eq (α := ℂ) (∑' (n : ℤ), f (x + (↑n : ℝ)))
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ) (𝓕 f (↑n : ℝ)) ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))

Tactic:
Real.tsum_eq_tsum_fourier (fun K => summable_of_isBigO (Real.summable_abs_int_rpow hb)
    ((isBigO_norm_restrict_cocompact ⟨_, hc⟩ (zero_lt_one.trans hb) hf K).comp_tendsto
    Int.tendsto_coe_cofinite)) hFf x

Premises used: Real.tsum_eq_tsum_fourier, ContinuousMap.mk, Real.summable_abs_int_rpow, zero_lt_one, LT.lt.trans, summable_of_isBigO, Asymptotics.IsBigO.comp_tendsto, Int.tendsto_coe_cofinite, isBigO_norm_restrict_cocompact
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : ℝ → ℂ
hc : Continuous f
b : ℝ
hb : 1 < b
hf : IsBigO (F := ℝ) (cocompact ℝ) f fun (x : ℝ) ↦ |x| ^ (-b)
hFf : IsBigO (F := ℝ) (cocompact ℝ) (𝓕 f) fun (x : ℝ) ↦ |x| ^ (-b)
x : ℝ
⊢ Eq (α := ℂ) (∑' (n : ℤ), f (x + (↑n : ℝ)))
    (∑' (n : ℤ),
      HMul.hMul (β := ℂ) (𝓕 f (↑n : ℝ)) ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))

Tactic:
Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summable hc hb hf (summable_of_isBigO
    (Real.summable_abs_int_rpow hb) (hFf.comp_tendsto Int.tendsto_coe_cofinite)) x

Premises used: Real.summable_abs_int_rpow, Real.tsum_eq_tsum_fourier_of_rpow_decay_of_summable, summable_of_isBigO, Asymptotics.IsBigO.comp_tendsto, Int.tendsto_coe_cofinite
-- Module: Mathlib.Analysis.Fourier.PoissonSummation
Goal:
f : 𝓢(ℝ, ℂ)
x : ℝ
⊢ Eq (α := ℂ) (∑' (n : ℤ), (f : (a : ℝ) → ℂ) (x + (↑n : ℝ)))
    (∑' (n : ℤ),
      HMul.hMul (α := ℂ) (β := ℂ) ((𝓕 f : (a : ℝ) → ℂ) (↑n : ℝ) : ℂ)
        ((fourier n : (a : AddCircle 1) → ℂ) (↑x : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ))

Tactic:
apply Real.tsum_eq_tsum_fourier_of_rpow_decay f.continuous one_lt_two
    (f.isBigO_cocompact_rpow (-2)) ((𝓕 f).isBigO_cocompact_rpow (-2))

Premises used: SchwartzMap.continuous, Real.tsum_eq_tsum_fourier_of_rpow_decay, one_lt_two, OfNat.ofNat, Neg.neg, SchwartzMap.isBigO_cocompact_rpow
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
h : HPow.hPow (β := ℕ) ‖w‖ 2 ≠ 0
⊢ ⟪i w, w⟫ = 1 / 2

Tactic:
rw [inner_smul_left, inner_self_eq_norm_sq_to_K, RCLike.ofReal_real_eq_id, id,
      RCLike.conj_to_real, ← div_div, div_mul_cancel₀]

Premises used: div_mul_cancel₀, inner_self_eq_norm_sq_to_K, id, RCLike.ofReal_real_eq_id, RCLike.conj_to_real, div_div, inner_smul_left
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
h : ¬HPow.hPow (β := ℕ) ‖w‖ 2 = 0
h₁ : ¬‖w‖ = 0
h₂ h₃ h₄ h₅ : ¬w = 0
⊢ HPow.hPow (β := ℕ) ‖w‖ 2 ≠ 0

Tactic:
rwa [Ne, sq_eq_zero_iff, norm_eq_zero]

Premises used: norm_eq_zero, Ne, sq_eq_zero_iff
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
⊢ ⟪i w, w⟫ = 1 / 2

Tactic:
have hiw : ⟪i w, w⟫ = 1 / 2 := by
    rw [inner_smul_left, inner_self_eq_norm_sq_to_K, RCLike.ofReal_real_eq_id, id,
      RCLike.conj_to_real, ← div_div, div_mul_cancel₀]
    rwa [Ne, sq_eq_zero_iff, norm_eq_zero]
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
h :
  ∀ (v : V),
    HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f (v + i w)) =
      (fun (x : V) ↦ -HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪x, w⟫) : Circle) (f x)) (v + i w)
⊢ Eq (α := (v : V) → E)
    (fun (v : V) ↦ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f (v + i w))) fun (v : V) ↦
    (fun (x : V) ↦ -HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪x, w⟫) : Circle) (f x)) (v + i w)

Tactic:
ext1 v
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
h :
  cexp ((↑(2 * π * -⟪v, w⟫) : ℂ) * I) • f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w) =
    -((cexp ((↑(2 * π * -⟪v, w⟫) : ℂ) * I) * cexp ((↑(2 * π * -(1 / 2)) : ℂ) * I)) •
        f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w))
⊢ HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪v, w⟫) : Circle) (f (v + i w)) =
    (fun (x : V) ↦ -HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-⟪x, w⟫) : Circle) (f x)) (v + i w)

Tactic:
simp_rw [inner_add_left, hiw, Circle.smul_def, Real.fourierChar_apply, neg_add, mul_add,
      ofReal_add, add_mul, exp_add]

Premises used: add_mul, Complex.exp_add, Circle.smul_def, neg_add, Complex.ofReal_add, inner_add_left, Real.fourierChar_apply, mul_add
-- Module: Mathlib.Analysis.Fourier.RiemannLebesgueLemma
Goal:
E : Type u_1
V : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : V → E
inst_2 : NormedAddCommGroup V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
inst_5 : InnerProductSpace ℝ V
inst_6 : FiniteDimensional ℝ V
w : V
hw : w ≠ 0
hiw : ⟪i w, w⟫ = 1 / 2
v : V
match_scalars :
  cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * 1 =
    -(cexp (2 * (↑π : ℂ) * -(↑⟪v, w⟫ : ℂ) * I) * cexp (2 * (↑π : ℂ) * -HDiv.hDiv (α := ℂ) 1 2 * I) * 1)
⊢ cexp ((↑(2 * π * -⟪v, w⟫) : ℂ) * I) • f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w) =
    -((cexp ((↑(2 * π * -⟪v, w⟫) : ℂ) * I) * cexp ((↑(2 * π * -(1 / 2)) : ℂ) * I)) •
        f (v + (1 / (2 * HPow.hPow (β := ℕ) ‖w‖ 2)) • w))

Tactic:
match_scalars