Theorem: LSeries_sub_eventuallyEq_zero_of_LSeries_eventually_eq (EulerProducts/LSeriesUnique.lean)

State before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x => LSeries f ↑x) =ᶠ[atTop] fun x => LSeries g ↑x
⊢ (fun x => LSeries (f - g) ↑x) =ᶠ[atTop] 0
Tactic:
rw [EventuallyEq, eventually_atTop] at h ⊢
State after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : ∃ a, ∀ b ≥ a, LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

State before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : ∃ a, ∀ b ≥ a, LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Tactic:
obtain ⟨x₀, hx₀⟩ := h
State after:
case intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

State before:
case intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Tactic:
obtain ⟨yf, hyf₁, hyf₂⟩ := exists_between hf
State after:
case intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : EReal
hyf₁ : abscissaOfAbsConv f < yf
hyf₂ : yf < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

State before:
case intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : EReal
hyf₁ : abscissaOfAbsConv f < yf
hyf₂ : yf < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Tactic:
obtain ⟨yg, hyg₁, hyg₂⟩ := exists_between hg
State after:
case intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : EReal
hyf₁ : abscissaOfAbsConv f < yf
hyf₂ : yf < ⊤
yg : EReal
hyg₁ : abscissaOfAbsConv g < yg
hyg₂ : yg < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

State before:
case intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : EReal
hyf₁ : abscissaOfAbsConv f < yf
hyf₂ : yf < ⊤
yg : EReal
hyg₁ : abscissaOfAbsConv g < yg
hyg₂ : yg < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Tactic:
lift yf to ℝ using ⟨hyf₂.ne, ((OrderBot.bot_le _).trans_lt hyf₁).ne'⟩
State after:
case intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yg : EReal
hyg₁ : abscissaOfAbsConv g < yg
hyg₂ : yg < ⊤
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

State before:
case intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yg : EReal
hyg₁ : abscissaOfAbsConv g < yg
hyg₂ : yg < ⊤
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Tactic:
lift yg to ℝ using ⟨hyg₂.ne, ((OrderBot.bot_le _).trans_lt hyg₁).ne'⟩
State after:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b

State before:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
⊢ ∃ a, ∀ b ≥ a, LSeries (f - g) ↑b = 0 b
Tactic:
refine ⟨max x₀ (max yf yg), fun x hx ↦ ?_⟩
State after:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ LSeries (f - g) ↑x = 0 x

State before:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ LSeries (f - g) ↑x = 0 x
Tactic:
have Hf : LSeriesSummable f x := by
  refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <| (ofReal_re x).symm ▸ hyf₁.trans_le ?_
  refine (le_max_left _ (yg : EReal)).trans <| (le_max_right (x₀ : EReal) _).trans ?_
  simpa only [max_le_iff, EReal.coe_le_coe_iff] using hx
State after:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
⊢ LSeries (f - g) ↑x = 0 x

State before:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
⊢ LSeries (f - g) ↑x = 0 x
Tactic:
have Hg : LSeriesSummable g x := by
  refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <| (ofReal_re x).symm ▸ hyg₁.trans_le ?_
  refine (le_max_right (yf : EReal) _).trans <| (le_max_right (x₀ : EReal) _).trans ?_
  simpa only [max_le_iff, EReal.coe_le_coe_iff] using hx
State after:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
Hg : LSeriesSummable g ↑x
⊢ LSeries (f - g) ↑x = 0 x

State before:
case intro.intro.intro.intro.intro.intro.intro
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
Hg : LSeriesSummable g ↑x
⊢ LSeries (f - g) ↑x = 0 x
Tactic:
rw [LSeries_sub Hf Hg, hx₀ x <| (le_max_left ..).trans hx, sub_self, Pi.zero_apply]
State after:
no goals

State before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ LSeriesSummable f ↑x
Tactic:
refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <| (ofReal_re x).symm ▸ hyf₁.trans_le ?_
State after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ ↑yf ≤ ↑x

State before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ ↑yf ≤ ↑x
Tactic:
refine (le_max_left _ (yg : EReal)).trans <| (le_max_right (x₀ : EReal) _).trans ?_
State after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ max (↑x₀) (max ↑yf ↑yg) ≤ ↑x

State before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
⊢ max (↑x₀) (max ↑yf ↑yg) ≤ ↑x
Tactic:
simpa only [max_le_iff, EReal.coe_le_coe_iff] using hx
State after:
no goals

State before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
⊢ LSeriesSummable g ↑x
Tactic:
refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <| (ofReal_re x).symm ▸ hyg₁.trans_le ?_
State after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
⊢ ↑yg ≤ ↑x

State before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
⊢ ↑yg ≤ ↑x
Tactic:
refine (le_max_right (yf : EReal) _).trans <| (le_max_right (x₀ : EReal) _).trans ?_
State after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
⊢ max (↑x₀) (max ↑yf ↑yg) ≤ ↑x

State before:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ b ≥ x₀, LSeries f ↑b = LSeries g ↑b
yf : ℝ
hyf₁ : abscissaOfAbsConv f < ↑yf
hyf₂ : ↑yf < ⊤
yg : ℝ
hyg₁ : abscissaOfAbsConv g < ↑yg
hyg₂ : ↑yg < ⊤
x : ℝ
hx : x ≥ max x₀ (max yf yg)
Hf : LSeriesSummable f ↑x
⊢ max (↑x₀) (max ↑yf ↑yg) ≤ ↑x
Tactic:
simpa only [max_le_iff, EReal.coe_le_coe_iff] using hx
State after:
no goals