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 := ℝ) 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
⊢ 1 / 2 * x ≤ y
have linarith₁ : y < 1 / 2 * x → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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 := ℝ) 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
⊢ 1 / 2 * x ≤ y
have linarith₂ : y < 1 / 2 * x → HMul.hMul (α := ℝ) 2 1 = 2
Tactic: linarith
-- 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 := ℝ) 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
⊢ 1 / 2 * x ≤ y
have linarith₃ : y < 1 / 2 * x → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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 := ℝ) 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
⊢ 1 / 2 * x ≤ y
have linarith₄ : y < 1 / 2 * x → 2 * (x + R - y) + (-2 * R - x) + (2 * y - HMul.hMul (α := ℝ) 1 1 * (1 * x)) = 0
Tactic: linarith
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S x y : ℝ
hy : x + R ≤ y
hx1 : 0 < x
hx2 : -2 * R < x
⊢ -b ≤ 0
have linarith : 0 < -b → 0 - b + (0 - -b) = 0
Tactic: linarith
-- 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 := ℝ) atTop (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) fun (x : ℝ) ↦
    |x| ^ (-b)
have claim : ∀ (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
-- 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 := ℝ) 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)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) fun (x : ℝ) ↦
    |x| ^ (-b)
have 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)
Tactic: obtain ⟨c, hc, hc'⟩ := hf.exists_pos
-- 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 := ℝ) 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)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) fun (x : ℝ) ↦
    |x| ^ (-b)
have 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)‖
Tactic: simp only [IsBigO, IsBigOWith, eventually_atTop] at hc' ⊢
Cleared hypotheses: hc'
-- 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 := ℝ) 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)‖
⊢ ∃ (c : ℝ) (a : ℝ), ∀ b_1 ≥ a, ‖‖ContinuousMap.restrict (Icc (b_1 + R) (b_1 + S)) f‖‖ ≤ c * ‖|b_1| ^ (-b)‖
have 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)‖
Tactic: obtain ⟨d, hd⟩ := hc'
Cleared hypotheses: hc'
-- 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 := ℝ) 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)‖
have 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)‖
Tactic: refine ⟨c * (1 / 2) ^ (-b), ⟨max (1 + max 0 (-2 * R)) (d - R), fun x hx => ?_⟩⟩
-- 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 := ℝ) 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)
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
have hx₁ : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x
Tactic: rw [ge_iff_le, max_le_iff] at hx
Cleared hypotheses: hx
-- 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 := ℝ) 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
have linarith : x ≤ max 0 (-2 * R) → -1 + (1 + max 0 (-2 * R) - x) + (x - max 0 (-2 * R)) = 0
Tactic: linarith
-- 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 := ℝ) 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
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
have hx' : max 0 (-2 * R) < x
Tactic: have hx' : max 0 (-2 * R) < x := by linarith
-- 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 := ℝ) 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
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
have hx'₁ : 0 < x ∧ -2 * R < x
Tactic: rw [max_lt_iff] at hx'
Cleared hypotheses: hx'
-- 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 := ℝ) 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
⊢ ‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
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) ≤
    c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
Tactic: rw [norm_norm, ContinuousMap.norm_le _ (by positivity)]
-- 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 := ℝ) 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)
⊢ (↑y : ℝ) ≥ d
have linarith : (↑y : ℝ) < d → d - R - x + ((↑y : ℝ) - d) + (x + R - (↑y : ℝ)) = 0
Tactic: linarith [hx.1, y.2.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 := ℝ) 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
⊢ ∀ (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)‖
have refine : ∀ (y : (↑(Icc (x + R) (x + S)) : Type)), c * ‖|(↑y : ℝ)| ^ (-b)‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
Tactic: refine fun y => (hd y.1 (by linarith [hx.1, y.2.1])).trans ?_
-- 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 := ℝ) 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)
⊢ c * ‖|(↑y : ℝ)| ^ (-b)‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
have A : ∀ (x : ℝ), 0 ≤ |x| ^ (-b)
Tactic: have A : ∀ x : ℝ, 0 ≤ |x| ^ (-b) := fun x => by positivity
-- 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 := ℝ) 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)
⊢ c * ‖|(↑y : ℝ)| ^ (-b)‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
have rw : |(↑y : ℝ)| ^ (-b) ≤ (1 / 2) ^ (-b) * |x| ^ (-b)
Tactic: rw [mul_assoc, mul_le_mul_iff_right₀ hc, norm_of_nonneg (A _), norm_of_nonneg (A _)]
-- 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 := ℝ) 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)
⊢ max 0 (-2 * R) < x
have linarith : x ≤ max 0 (-2 * R) → -1 + (x - max 0 (-2 * R)) + (1 + max 0 (-2 * R) - x) = 0
Tactic: linarith only [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 := ℝ) 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)
⊢ |(↑y : ℝ)| ^ (-b) ≤ (1 / 2) ^ (-b) * |x| ^ (-b)
have h : |(↑y : ℝ)| = (↑y : ℝ)
Tactic: convert! claim x (by linarith only [hx.1]) y.1 y.2.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 := ℝ) 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 : ℝ)
⊢ |(↑y : ℝ)| ^ (-b) ≤ (1 / 2) ^ (-b) * |x| ^ (-b)
have h₁ : |x| = x
Tactic: convert! claim x (by linarith only [hx.1]) y.1 y.2.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 := ℝ) 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)
⊢ |(↑y : ℝ)| = (↑y : ℝ)
have h : 0 ≤ (↑y : ℝ)
Tactic: apply abs_of_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 := ℝ) 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)
⊢ 0 ≤ (↑y : ℝ)
have linarith : (↑y : ℝ) < 0 → 0 - x + (-2 * R - x) + 2 * ((↑y : ℝ) - 0) + 2 * (x + R - (↑y : ℝ)) = 0
Tactic: linarith [y.2.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 := ℝ) 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
⊢ 0 ≤ (↑y : ℝ)
have linarith₁ : (↑y : ℝ) < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [y.2.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 := ℝ) 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)
have h : Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ |x| ^ (-b)) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg)
Tactic: convert! hf.comp_tendsto tendsto_neg_atTop_atBot using 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 := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
⊢ Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ |x| ^ (-b)) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg)
have h : ∀ (x : ℝ), |x| ^ (-b) = ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) x
Tactic: ext1 x
-- 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 := ℝ) atBot (⇑f : (a : ℝ) → E) fun (x : ℝ) ↦ |x| ^ (-b)
R S : ℝ
⊢ IsBigO (E := ℝ) (F := ℝ) atBot (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) fun (x : ℝ) ↦
    |x| ^ (-b)
have h1 : IsBigO (E := E) (F := ℝ) atTop (⇑(f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := sorry : 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]
-- 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 := ℝ) 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 + R) (x + S)) f‖) fun (x : ℝ) ↦
    |x| ^ (-b)
have h2 : IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atBot
  ((fun (x : ℝ) ↦
      ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
          (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := sorry : 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
-- 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)) ∘ Neg.neg)
⊢ Eq (α := ℝ → ℝ) ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) fun (x : ℝ) ↦ |x| ^ (-b)
have h : ∀ (x : ℝ), ((fun (x : ℝ) ↦ |x| ^ (-b)) ∘ Neg.neg) x = |x| ^ (-b)
Tactic: ext1 x
-- 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 := ℝ) 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)
⊢ IsBigO (E := ℝ) (F := ℝ) atBot (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) fun (x : ℝ) ↦
    |x| ^ (-b)
have this : 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]
-- 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 := ℝ) 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 + R) (x + S)) f‖) fun (x : ℝ) ↦
    |x| ^ (-b)
have h2₁ : IsBigO (E := ℝ) (F := ℝ) atBot
  ((fun (x : ℝ) ↦
      ‖ContinuousMap.restrict (Icc (x + -S) (x + -R))
          (f.comp { toFun := fun (a : ℝ) ↦ -a, continuous_toFun := sorry : C(ℝ, ℝ) })‖) ∘
    Neg.neg)
  fun (x : ℝ) ↦ |x| ^ (-b)
Tactic: rw [this] at h2
Cleared hypotheses: h2, this
-- 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)
⊢ IsBigO (E := ℝ) (F := ℝ) atBot (fun (x : ℝ) ↦ ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) fun (x : ℝ) ↦
    |x| ^ (-b)
have 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 := sorry : C(ℝ, ℝ) })‖) ∘
          Neg.neg)
        x)
Tactic: refine (isBigO_of_le _ fun x => ?_).trans h2