awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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 : ℝ
⊢ ‖‖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)
have 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 := sorry : C(ℝ, ℝ) })‖
Tactic: rw [norm_norm, Function.comp_apply, norm_norm, ContinuousMap.norm_le _ (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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)
      ((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(ℝ, ℝ) })‖
have 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 := sorry : C(ℝ, ℝ) })‖
Tactic: rw [ContinuousMap.restrict_apply_mk]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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(ℝ, ℝ) })‖
have 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 := sorry : 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) sorry) :
      E)
Tactic: refine (le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨-x, ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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)
⊢ 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(ℝ, ℝ) })‖
have refine_2 : -x ∈ Icc (-x_1 + -S) (-x_1 + -R)
Tactic: refine (le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨-x, ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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) =
    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)
have refine_1 : Norm.norm (E := E) ((f : (a : ℝ) → E) x : E) =
  Norm.norm (E := E) ((f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := sorry : C(ℝ, ℝ) } : (a : ℝ) → E) (-x) : E)
Tactic: rw [ContinuousMap.restrict_apply_mk, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
      ContinuousMap.coe_mk, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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)
⊢ 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)
have refine_1₁ : Norm.norm (E := E) ((f : (a : ℝ) → E) x : E) =
  Norm.norm (E := E)
    ((f : (a : ℝ) → E) (({ toFun := fun (a : ℝ) ↦ -a, continuous_toFun := sorry } : (a : ℝ) → ℝ) (-x) : ℝ) : E)
Tactic: rw [ContinuousMap.restrict_apply_mk, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
      ContinuousMap.coe_mk, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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)
⊢ 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)
have refine_1₂ : ‖f.toFun x‖ = ‖f.toFun (({ toFun := fun (a : ℝ) ↦ -a, continuous_toFun := sorry : C(ℝ, ℝ) } : (a : ℝ) → ℝ) (-x))‖
Tactic: rw [ContinuousMap.restrict_apply_mk, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
      ContinuousMap.coe_mk, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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))‖
⊢ 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)
have refine_1₃ : ‖f.toFun x‖ = ‖f.toFun (- -x)‖
Tactic: rw [ContinuousMap.restrict_apply_mk, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
      ContinuousMap.coe_mk, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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)‖
⊢ 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)
have refine_1₄ : ‖f.toFun x‖ = ‖f.toFun x‖
Tactic: rw [ContinuousMap.restrict_apply_mk, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
      ContinuousMap.coe_mk, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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_1 + -S ≤ -x
have linarith : -x < -x_1 + -S → -x - (-x_1 + -S) + (x - (x_1 + S)) = 0
Tactic: linarith [hx.2]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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 ≤ -x_1 + -R
have linarith : -x_1 + -R < -x → -x_1 + -R - -x + (x_1 + R - x) = 0
Tactic: linarith [hx.1]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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 ℝ
⊢ IsBigO (E := ℝ) (F := ℝ) (cocompact ℝ)
    (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)
have 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)
Tactic: obtain ⟨r, hr⟩ := K.isCompact.isBounded.subset_closedBall 0
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (hypothesis)
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
⊢ IsBigO (E := ℝ) (F := ℝ) (cocompact ℝ)
    (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (↑K : Set ℝ) (f.comp (ContinuousMap.addRight x))‖) fun (x : ℝ) ↦ |x| ^ (-b)
have hr₁ : (↑K : Set ℝ) ⊆ Icc (-r) r
Tactic: rw [closedBall_eq_Icc, zero_add, zero_sub] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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‖
have 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‖
Tactic: rw [ContinuousMap.norm_le _ (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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‖
have 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) sorry) :
      E)
Tactic: refine (le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨y + x, ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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)
⊢ 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‖
have refine_2 : y + x ∈ Icc (x - r) (x + r)
Tactic: refine (le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨y + x, ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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) =
    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)
have 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)
Tactic: simp_rw [ContinuousMap.restrict_apply, ContinuousMap.comp_apply, ContinuousMap.coe_addRight]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [ContinuousMap.restrict_apply, ContinuousMap.comp_apply, ContinuousMap.coe_addRight]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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 ℝ)
⊢ x - r ≤ y + x
have linarith : y + x < x - r → y + x - (x - r) + (-r - y) = 0
Tactic: linarith [(hr hy).1]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.PoissonSummation (goal)
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 ≤ x + r
have linarith : x + r < y + x → x + r - (y + x) + (y - r) = 0
Tactic: linarith [(hr hy).2]