internlm/Lean-Github huggingface dataset:
Theorem: limiting_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
l1 :
  Tendsto (fun σ' => ∑' (n : ℕ), term f (↑σ') n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)) (𝓝[>] 1)
    (𝓝 (∑' (n : ℕ), f n / ↑n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log)))
l2 :
  Tendsto
    (fun σ' =>
      ↑A * ↑(x ^ (1 - σ')) * ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (σ' - 1))) * 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π)))
    (𝓝[>] 1) (𝓝 (↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π))))
l3 :
  Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
⊢ (fun x_1 =>
      ∑' (n : ℕ), term f (↑x_1) n * 𝓕 (W21.ofCS2 ψ).toFun (1 / (2 * π) * (↑n / x).log) -
        ↑A * ↑(x ^ (1 - x_1)) *
          ∫ (u : ℝ) in Ici (-x.log), ↑(rexp (-u * (x_1 - 1))) * 𝓕 (W21.ofCS2 ψ).toFun (u / (2 * π))) =ᶠ[𝓝[>] 1]
    fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)
Tactic:
simpa [eventuallyEq_nhdsWithin_iff] using eventually_of_forall (limiting_fourier_aux hG' hf ψ hx)
Proof state after:
no goals
Theorem: limiting_fourier
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
ψ : CS 2 ℂ
hx : 1 ≤ x
⊢ 0 < ?m.1975794
Tactic:
linarith
Proof state after:
no goals
Theorem: limiting_cor_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * ↑x ^ (↑t * I)) atTop (𝓝 0)
Tactic:
have l1 : ∀ᶠ x : ℝ in atTop, ∀ t : ℝ, x ^ (t * I) = exp (log x * t * I) := by
  filter_upwards [eventually_ne_atTop 0, eventually_ge_atTop 0] with x hx hx' t
  rw [Complex.cpow_def_of_ne_zero (ofReal_ne_zero.mpr hx), ofReal_log hx'] ; ring_nf
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * ↑x ^ (↑t * I)) atTop (𝓝 0)
Theorem: limiting_cor_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * ↑x ^ (↑t * I)) atTop (𝓝 0)
Tactic:
have l2 : ∀ᶠ x : ℝ in atTop, ∫ t, f t * x ^ (t * I) = ∫ t, f t * exp (log x * t * I) := by
  filter_upwards [l1] with x hx
  refine integral_congr_ae (eventually_of_forall (fun x => by simp [hx]))
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * ↑x ^ (↑t * I)) atTop (𝓝 0)
Theorem: limiting_cor_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * ↑x ^ (↑t * I)) atTop (𝓝 0)
Tactic:
simp_rw [tendsto_congr' l2]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)) atTop (𝓝 0)
Theorem: limiting_cor_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)) atTop (𝓝 0)
Tactic:
convert_to Tendsto (fun x => 𝓕 f (-Real.log x / (2 * π))) atTop (𝓝 0)
Proof state after:
case h.e'_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ (fun x => ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)) = fun x => 𝓕 f (-x.log / (2 * π))

n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => 𝓕 f (-x.log / (2 * π))) atTop (𝓝 0)
Theorem: limiting_cor_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => 𝓕 f (-x.log / (2 * π))) atTop (𝓝 0)
Tactic:
refine (zero_at_infty_fourierIntegral f).comp <| Tendsto.mono_right ?_ _root_.atBot_le_cocompact
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => -x.log / (2 * π)) atTop atBot
Theorem: limiting_cor_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ Tendsto (fun x => -x.log / (2 * π)) atTop atBot
Tactic:
exact (tendsto_neg_atBot_iff.mpr tendsto_log_atTop).atBot_mul_const (inv_pos.mpr two_pi_pos)
Proof state after:
no goals
Theorem: limiting_cor_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
Tactic:
filter_upwards [eventually_ne_atTop 0, eventually_ge_atTop 0] with x hx hx' t
Proof state after:
case h
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
x : ℝ
hx : x ≠ 0
hx' : 0 ≤ x
t : ℝ
⊢ ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
Theorem: limiting_cor_aux
Proof state before:
case h
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
x : ℝ
hx : x ≠ 0
hx' : 0 ≤ x
t : ℝ
⊢ ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
Tactic:
rw [Complex.cpow_def_of_ne_zero (ofReal_ne_zero.mpr hx), ofReal_log hx']
Proof state after:
case h
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
x : ℝ
hx : x ≠ 0
hx' : 0 ≤ x
t : ℝ
⊢ cexp ((↑x).log * (↑t * I)) = cexp ((↑x).log * ↑t * I)
Theorem: limiting_cor_aux
Proof state before:
case h
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
x : ℝ
hx : x ≠ 0
hx' : 0 ≤ x
t : ℝ
⊢ cexp ((↑x).log * (↑t * I)) = cexp ((↑x).log * ↑t * I)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: limiting_cor_aux
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
⊢ ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
Tactic:
filter_upwards [l1] with x hx
Proof state after:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
x : ℝ
hx : ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
⊢ ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
Theorem: limiting_cor_aux
Proof state before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
x : ℝ
hx : ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
⊢ ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
Tactic:
refine integral_congr_ae (eventually_of_forall (fun x => by simp [hx]))
Proof state after:
no goals
Theorem: limiting_cor_aux
Proof state before:
n : ℕ
A a b c d u x✝¹ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
x✝ : ℝ
hx : ∀ (t : ℝ), ↑x✝ ^ (↑t * I) = cexp (↑x✝.log * ↑t * I)
x : ℝ
⊢ (fun t => f t * ↑x✝ ^ (↑t * I)) x = (fun t => f t * cexp (↑x✝.log * ↑t * I)) x
Tactic:
simp [hx]
Proof state after:
no goals
Theorem: limiting_cor_aux
Proof state before:
case h.e'_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
⊢ (fun x => ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)) = fun x => 𝓕 f (-x.log / (2 * π))
Tactic:
ext
Proof state after:
case h.e'_3.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝ : ℝ
⊢ ∫ (t : ℝ), f t * cexp (↑x✝.log * ↑t * I) = 𝓕 f (-x✝.log / (2 * π))
Theorem: limiting_cor_aux
Proof state before:
case h.e'_3.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝ : ℝ
⊢ ∫ (t : ℝ), f t * cexp (↑x✝.log * ↑t * I) = 𝓕 f (-x✝.log / (2 * π))
Tactic:
congr
Proof state after:
case h.e'_3.h.e_f
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝ : ℝ
⊢ (fun t => f t * cexp (↑x✝.log * ↑t * I)) = fun v => 𝐞 (-((innerₗ ℝ) v) (-x✝.log / (2 * π))) • f v
Theorem: limiting_cor_aux
Proof state before:
case h.e'_3.h.e_f
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝ : ℝ
⊢ (fun t => f t * cexp (↑x✝.log * ↑t * I)) = fun v => 𝐞 (-((innerₗ ℝ) v) (-x✝.log / (2 * π))) • f v
Tactic:
ext
Proof state after:
case h.e'_3.h.e_f.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ f x✝ * cexp (↑x✝¹.log * ↑x✝ * I) = 𝐞 (-((innerₗ ℝ) x✝) (-x✝¹.log / (2 * π))) • f x✝
Theorem: limiting_cor_aux
Proof state before:
case h.e'_3.h.e_f.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ f x✝ * cexp (↑x✝¹.log * ↑x✝ * I) = 𝐞 (-((innerₗ ℝ) x✝) (-x✝¹.log / (2 * π))) • f x✝
Tactic:
simp [Real.fourierChar, expMapCircle, mul_comm (f _)]
Proof state after:
case h.e'_3.h.e_f.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ cexp (↑x✝¹.log * ↑x✝ * I) = cexp (-(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))) * I)) ∨ f x✝ = 0
Theorem: limiting_cor_aux
Proof state before:
case h.e'_3.h.e_f.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ cexp (↑x✝¹.log * ↑x✝ * I) = cexp (-(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))) * I)) ∨ f x✝ = 0
Tactic:
left
Proof state after:
case h.e'_3.h.e_f.h.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ cexp (↑x✝¹.log * ↑x✝ * I) = cexp (-(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))) * I))
Theorem: limiting_cor_aux
Proof state before:
case h.e'_3.h.e_f.h.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ cexp (↑x✝¹.log * ↑x✝ * I) = cexp (-(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))) * I))
Tactic:
congr
Proof state after:
case h.e'_3.h.e_f.h.h.e_z
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ ↑x✝¹.log * ↑x✝ * I = -(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))) * I)
Theorem: limiting_cor_aux
Proof state before:
case h.e'_3.h.e_f.h.h.e_z
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ ↑x✝¹.log * ↑x✝ * I = -(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))) * I)
Tactic:
rw [← neg_mul]
Proof state after:
case h.e'_3.h.e_f.h.h.e_z
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ ↑x✝¹.log * ↑x✝ * I = -(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π)))) * I
Theorem: limiting_cor_aux
Proof state before:
case h.e'_3.h.e_f.h.h.e_z
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ ↑x✝¹.log * ↑x✝ * I = -(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π)))) * I
Tactic:
congr
Proof state after:
case h.e'_3.h.e_f.h.h.e_z.e_a
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ ↑x✝¹.log * ↑x✝ = -(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))))
Theorem: limiting_cor_aux
Proof state before:
case h.e'_3.h.e_f.h.h.e_z.e_a
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ ↑x✝¹.log * ↑x✝ = -(2 * ↑π * (↑x✝ * (-↑x✝¹.log / (2 * ↑π))))
Tactic:
norm_cast
Proof state after:
case h.e'_3.h.e_f.h.h.e_z.e_a
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ x✝¹.log * x✝ = -(2 * π * (x✝ * (-x✝¹.log / (2 * π))))
Theorem: limiting_cor_aux
Proof state before:
case h.e'_3.h.e_f.h.h.e_z.e_a
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ x✝¹.log * x✝ = -(2 * π * (x✝ * (-x✝¹.log / (2 * π))))
Tactic:
field_simp
Proof state after:
case h.e'_3.h.e_f.h.h.e_z.e_a
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ x✝¹.log * x✝ = x✝ * x✝¹.log
Theorem: limiting_cor_aux
Proof state before:
case h.e'_3.h.e_f.h.h.e_z.e_a
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℝ → ℂ
l1 : ∀ᶠ (x : ℝ) in atTop, ∀ (t : ℝ), ↑x ^ (↑t * I) = cexp (↑x.log * ↑t * I)
l2 : ∀ᶠ (x : ℝ) in atTop, ∫ (t : ℝ), f t * ↑x ^ (↑t * I) = ∫ (t : ℝ), f t * cexp (↑x.log * ↑t * I)
x✝¹ x✝ : ℝ
⊢ x✝¹.log * x✝ = x✝ * x✝¹.log
Tactic:
ring
Proof state after:
no goals
Theorem: limiting_cor
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
⊢ Tendsto
    (fun x =>
      ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
        ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π)))
    atTop (𝓝 0)
Tactic:
apply limiting_cor_aux.congr'
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
⊢ (fun x => ∫ (t : ℝ), ?m.2055554 t * ↑x ^ (↑t * I)) =ᶠ[atTop] fun x =>
    ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))

n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
⊢ ℝ → ℂ
Theorem: limiting_cor
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
⊢ (fun x => ∫ (t : ℝ), ?m.2055554 t * ↑x ^ (↑t * I)) =ᶠ[atTop] fun x =>
    ∑' (n : ℕ), f n / ↑n * 𝓕 ψ.toFun (1 / (2 * π) * (↑n / x).log) -
      ↑A * ∫ (u : ℝ) in Ici (-x.log), 𝓕 ψ.toFun (u / (2 * π))

n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ψ : CS 2 ℂ
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hcheby : cheby f
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries f s - ↑A / (s - 1)) {s | 1 < s.re}
⊢ ℝ → ℂ
Tactic:
filter_upwards [eventually_ge_atTop 1] with x hx using limiting_fourier hcheby hG hG' hf ψ hx |>.symm
Proof state after:
no goals
Theorem: smooth_urysohn
Proof state before:
n : ℕ
A a✝ b✝ c✝ d✝ u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b c d : ℝ
h1 : a < b
h3 : c < d
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1
Tactic:
obtain ⟨ψ, l1, l2, l3, l4, -⟩ := smooth_urysohn_support_Ioo h1 h3
Proof state after:
case intro.intro.intro.intro.intro
n : ℕ
A a✝ b✝ c✝ d✝ u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b c d : ℝ
h1 : a < b
h3 : c < d
ψ : ℝ → ℝ
l1 : ContDiff ℝ ⊤ ψ
l2 : HasCompactSupport ψ
l3 : (Icc b c).indicator 1 ≤ ψ
l4 : ψ ≤ (Ioo a d).indicator 1
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1
Theorem: smooth_urysohn
Proof state before:
case intro.intro.intro.intro.intro
n : ℕ
A a✝ b✝ c✝ d✝ u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b c d : ℝ
h1 : a < b
h3 : c < d
ψ : ℝ → ℝ
l1 : ContDiff ℝ ⊤ ψ
l2 : HasCompactSupport ψ
l3 : (Icc b c).indicator 1 ≤ ψ
l4 : ψ ≤ (Ioo a d).indicator 1
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1
Tactic:
refine ⟨ψ, l1, l2, l3, l4⟩
Proof state after:
no goals
Theorem: one_div_sub_one
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
n : ℕ
⊢ 1 / ↑(n - 1) ≤ 2 / ↑n
Tactic:
match n with
| 0 => simp
| 1 => simp
| n + 2 => { norm_cast ; rw [div_le_div_iff] <;> simp [mul_add] <;> linarith }
Proof state after:
no goals
Theorem: one_div_sub_one
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
n : ℕ
⊢ 1 / ↑(0 - 1) ≤ 2 / ↑0
Tactic:
simp
Proof state after:
no goals
Theorem: one_div_sub_one
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
n : ℕ
⊢ 1 / ↑(1 - 1) ≤ 2 / ↑1
Tactic:
simp
Proof state after:
no goals
Theorem: one_div_sub_one
Proof state before:
n✝¹ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
n✝ n : ℕ
⊢ 1 / ↑(n + 2 - 1) ≤ 2 / ↑(n + 2)
Tactic:
rw [div_le_div_iff] <;> simp [mul_add] <;> linarith
Proof state after:
no goals
Theorem: quadratic_pos
Proof state before:
n : ℕ
A a✝ b✝ c✝ d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b c x : ℝ
ha : 0 < a
hΔ : discrim a b c < 0
⊢ 0 < a * x ^ 2 + b * x + c
Tactic:
have l1 : a * x ^ 2 + b * x + c = a * (x + b / (2 * a)) ^ 2 - discrim a b c / (4 * a) := by
  field_simp [discrim] ; ring
Proof state after:
n : ℕ
A a✝ b✝ c✝ d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a b c x : ℝ
ha : 0 < a
hΔ : discrim a b c < 0
l1 : a * x ^ 2 + b * x + c = a * (x + b / (2 * a)) ^ 2 - discrim a b c / (4 * a)
⊢ 0 < a * x ^ 2 + b * x + c