internlm/Lean-Github huggingface dataset:
Theorem: hh_deriv
Proof state before:
case h.e'_7
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
l3 : HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l2 : HasDerivAt (fun t => 1 + (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
⊢ 1 + 2 * a ^ 2 * t.log + a ^ 2 * t.log ^ 2 = 1 * (1 + (a * t.log) ^ 2) + _root_.id t * (2 * a ^ 2 * t⁻¹ * t.log)
Tactic:
field_simp
Proof state after:
case h.e'_7
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
l3 : HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l2 : HasDerivAt (fun t => 1 + (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
⊢ 1 + 2 * a ^ 2 * t.log + a ^ 2 * t.log ^ 2 = 1 + (a * t.log) ^ 2 + 2 * a ^ 2 * t.log
Theorem: hh_deriv
Proof state before:
case h.e'_7
n : ℕ
A a✝ b c d u x y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a t : ℝ
ht : t ≠ 0
e1 : t * (1 + (a * t.log) ^ 2) ≠ 0
l5 : HasDerivAt (fun t => t.log) t⁻¹ t
l4 : HasDerivAt (fun t => a * t.log) (a * t⁻¹) t
l3 : HasDerivAt (fun t => (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
l2 : HasDerivAt (fun t => 1 + (a * t.log) ^ 2) (2 * a ^ 2 * t⁻¹ * t.log) t
⊢ 1 + 2 * a ^ 2 * t.log + a ^ 2 * t.log ^ 2 = 1 + (a * t.log) ^ 2 + 2 * a ^ 2 * t.log
Tactic:
ring
Proof state after:
no goals
Theorem: hh'_nonpos
Proof state before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
ha : a ∈ Ioo (-1) 1
⊢ hh' a x ≤ 0
Tactic:
have := pp_pos ha (log x)
Proof state after:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
ha : a ∈ Ioo (-1) 1
this : 0 < pp a x.log
⊢ hh' a x ≤ 0
Theorem: hh'_nonpos
Proof state before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
ha : a ∈ Ioo (-1) 1
this : 0 < pp a x.log
⊢ hh' a x ≤ 0
Tactic:
simp only [hh', neg_mul, Left.neg_nonpos_iff, ge_iff_le]
Proof state after:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
ha : a ∈ Ioo (-1) 1
this : 0 < pp a x.log
⊢ 0 ≤ pp a x.log * hh a x ^ 2
Theorem: hh'_nonpos
Proof state before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a x : ℝ
ha : a ∈ Ioo (-1) 1
this : 0 < pp a x.log
⊢ 0 ≤ pp a x.log * hh a x ^ 2
Tactic:
positivity
Proof state after:
no goals
Theorem: hh_antitone
Proof state before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
⊢ AntitoneOn (hh a) (Ioi 0)
Tactic:
have l1 x (hx : x ∈ interior (Ioi 0)) : HasDerivWithinAt (hh a) (hh' a x) (interior (Ioi 0)) x := by
  have : x ≠ 0 := by contrapose! hx ; simp [hx]
  exact (hh_deriv a this).hasDerivWithinAt
Proof state after:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
l1 : ∀ x ∈ interior (Ioi 0), HasDerivWithinAt (hh a) (hh' a x) (interior (Ioi 0)) x
⊢ AntitoneOn (hh a) (Ioi 0)
Theorem: hh_antitone
Proof state before:
n : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
l1 : ∀ x ∈ interior (Ioi 0), HasDerivWithinAt (hh a) (hh' a x) (interior (Ioi 0)) x
⊢ AntitoneOn (hh a) (Ioi 0)
Tactic:
apply antitoneOn_of_hasDerivWithinAt_nonpos (convex_Ioi _) (hh_continuous _) l1 (fun x _ => hh'_nonpos ha)
Proof state after:
no goals
Theorem: hh_antitone
Proof state before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
hx : x ∈ interior (Ioi 0)
⊢ HasDerivWithinAt (hh a) (hh' a x) (interior (Ioi 0)) x
Tactic:
have : x ≠ 0 := by contrapose! hx ; simp [hx]
Proof state after:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
hx : x ∈ interior (Ioi 0)
this : x ≠ 0
⊢ HasDerivWithinAt (hh a) (hh' a x) (interior (Ioi 0)) x
Theorem: hh_antitone
Proof state before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
hx : x ∈ interior (Ioi 0)
this : x ≠ 0
⊢ HasDerivWithinAt (hh a) (hh' a x) (interior (Ioi 0)) x
Tactic:
exact (hh_deriv a this).hasDerivWithinAt
Proof state after:
no goals
Theorem: hh_antitone
Proof state before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
hx : x ∈ interior (Ioi 0)
⊢ x ≠ 0
Tactic:
contrapose! hx
Proof state after:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
hx : x = 0
⊢ x ∉ interior (Ioi 0)
Theorem: hh_antitone
Proof state before:
n : ℕ
A a✝ b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℝ
ha : a ∈ Ioo (-1) 1
x : ℝ
hx : x = 0
⊢ x ∉ interior (Ioi 0)
Tactic:
simp [hx]
Proof state after:
no goals
Theorem: gg_of_hh
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : x ≠ 0
i : ℝ
⊢ gg x i = x⁻¹ * hh (1 / (2 * π)) (i / x)
Tactic:
field_simp [gg, hh]
Proof state after:
no goals
Theorem: gg_l1
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
n : ℕ
⊢ |gg x ↑n| ≤ 1 / ↑n
Tactic:
simp only [gg_of_hh hx.ne.symm, one_div, mul_inv_rev, abs_mul]
Proof state after:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
n : ℕ
⊢ |x⁻¹| * |hh (π⁻¹ * 2⁻¹) (↑n / x)| ≤ (↑n)⁻¹
Theorem: gg_l1
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
n : ℕ
⊢ |x⁻¹| * |hh (π⁻¹ * 2⁻¹) (↑n / x)| ≤ (↑n)⁻¹
Tactic:
apply mul_le_mul le_rfl (hh_le _ _ (by positivity)) (by positivity) (by positivity) |>.trans (le_of_eq ?_)
Proof state after:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
n : ℕ
⊢ |x⁻¹| * (↑n / x)⁻¹ = (↑n)⁻¹
Theorem: gg_l1
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
n : ℕ
⊢ |x⁻¹| * (↑n / x)⁻¹ = (↑n)⁻¹
Tactic:
simp [abs_inv, abs_eq_self.mpr hx.le]
Proof state after:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
n : ℕ
⊢ x⁻¹ * (x / ↑n) = (↑n)⁻¹
Theorem: gg_l1
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
n : ℕ
⊢ x⁻¹ * (x / ↑n) = (↑n)⁻¹
Tactic:
field_simp
Proof state after:
no goals
Theorem: gg_l1
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
n : ℕ
⊢ 0 ≤ ↑n / x
Tactic:
positivity
Proof state after:
no goals
Theorem: gg_l1
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
n : ℕ
⊢ 0 ≤ |hh (π⁻¹ * 2⁻¹) (↑n / x)|
Tactic:
positivity
Proof state after:
no goals
Theorem: gg_l1
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
x : ℝ
hx : 0 < x
n : ℕ
⊢ 0 ≤ |x⁻¹|
Tactic:
positivity
Proof state after:
no goals
Theorem: gg_le_one
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
⊢ gg x ↑i ≤ 1
Tactic:
by_cases hi : i = 0 <;> simp [gg, hi]
Proof state after:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
⊢ (↑i)⁻¹ * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹ ≤ 1
Theorem: gg_le_one
Proof state before:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
⊢ (↑i)⁻¹ * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹ ≤ 1
Tactic:
have l1 : 1 ≤ (i : ℝ) := by simp ; omega
Proof state after:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
⊢ (↑i)⁻¹ * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹ ≤ 1
Theorem: gg_le_one
Proof state before:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
⊢ (↑i)⁻¹ * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹ ≤ 1
Tactic:
have l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * Real.log (↑i / x)) ^ 2 := by simp ; positivity
Proof state after:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ (↑i)⁻¹ * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹ ≤ 1
Theorem: gg_le_one
Proof state before:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ (↑i)⁻¹ * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)⁻¹ ≤ 1
Tactic:
rw [← mul_inv]
Proof state after:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ (↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2))⁻¹ ≤ 1
Theorem: gg_le_one
Proof state before:
case neg
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ (↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2))⁻¹ ≤ 1
Tactic:
apply inv_le_one
Proof state after:
case neg.ha
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ 1 ≤ ↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)
Theorem: gg_le_one
Proof state before:
case neg.ha
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ 1 ≤ ↑i * (1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2)
Tactic:
simpa using mul_le_mul l1 l2 zero_le_one (by simp)
Proof state after:
no goals
Theorem: gg_le_one
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
⊢ 1 ≤ ↑i
Tactic:
simp
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
⊢ 1 ≤ i
Theorem: gg_le_one
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
⊢ 1 ≤ i
Tactic:
omega
Proof state after:
no goals
Theorem: gg_le_one
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
⊢ 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
Tactic:
simp
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
⊢ 0 ≤ (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
Theorem: gg_le_one
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
⊢ 0 ≤ (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
Tactic:
positivity
Proof state after:
no goals
Theorem: gg_le_one
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
i : ℕ
hi : ¬i = 0
l1 : 1 ≤ ↑i
l2 : 1 ≤ 1 + (π⁻¹ * 2⁻¹ * (↑i / x).log) ^ 2
⊢ 0 ≤ ↑i
Tactic:
simp
Proof state after:
no goals
Theorem: one_div_two_pi_mem_Ioo
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 / (2 * π) ∈ Ioo (-1) 1
Tactic:
constructor
Proof state after:
case left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ -1 < 1 / (2 * π)

case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 / (2 * π) < 1
Theorem: one_div_two_pi_mem_Ioo
Proof state before:
case left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ -1 < 1 / (2 * π)
Tactic:
trans 0
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ -1 < 0

n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 0 < 1 / (2 * π)
Theorem: one_div_two_pi_mem_Ioo
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ -1 < 0

n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 0 < 1 / (2 * π)
Tactic:
linarith
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 0 < 1 / (2 * π)
Theorem: one_div_two_pi_mem_Ioo
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 0 < 1 / (2 * π)
Tactic:
positivity
Proof state after:
no goals
Theorem: one_div_two_pi_mem_Ioo
Proof state before:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 / (2 * π) < 1
Tactic:
rw [div_lt_iff (by positivity)]
Proof state after:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 < 1 * (2 * π)
Theorem: one_div_two_pi_mem_Ioo
Proof state before:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 < 1 * (2 * π)
Tactic:
convert_to 1 * 1 < 2 * π
Proof state after:
case h.e'_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 = 1 * 1

case h.e'_4
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 * (2 * π) = 2 * π

case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 * 1 < 2 * π
Theorem: one_div_two_pi_mem_Ioo
Proof state before:
case h.e'_3
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 = 1 * 1

case h.e'_4
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 * (2 * π) = 2 * π

case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 * 1 < 2 * π
Tactic:
simp
Proof state after:
case h.e'_4
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 * (2 * π) = 2 * π

case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 * 1 < 2 * π
Theorem: one_div_two_pi_mem_Ioo
Proof state before:
case h.e'_4
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 * (2 * π) = 2 * π

case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 * 1 < 2 * π
Tactic:
simp
Proof state after:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 * 1 < 2 * π
Theorem: one_div_two_pi_mem_Ioo
Proof state before:
case right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 * 1 < 2 * π
Tactic:
apply mul_lt_mul one_lt_two ?_ zero_lt_one zero_le_two
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 ≤ π
Theorem: one_div_two_pi_mem_Ioo
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 ≤ π
Tactic:
trans 2
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 ≤ 2

n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 2 ≤ π
Theorem: one_div_two_pi_mem_Ioo
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 1 ≤ 2

n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 2 ≤ π
Tactic:
exact one_le_two
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 2 ≤ π
Theorem: one_div_two_pi_mem_Ioo
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 2 ≤ π
Tactic:
exact two_le_pi
Proof state after:
no goals
Theorem: one_div_two_pi_mem_Ioo
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 0 < 2 * π
Tactic:
positivity
Proof state after:
no goals
Theorem: sum_telescopic
Proof state before:
n✝ : ℕ
A a✝ b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
a : ℕ → ℝ
n : ℕ
⊢ ∑ i ∈ Finset.range n, (a (i + 1) - a i) = a n - a 0
Tactic:
apply Finset.sum_range_sub
Proof state after:
no goals
Theorem: cancel_aux
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
⊢ ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        ((n - 1 - 1) • (C * g 0) - ∑ x ∈ Finset.range (n - 1 - 1), C * g (x + 1)))
Tactic:
have l1 (n : ℕ) : (g n - g (n + 1)) * ∑ i in Finset.range (n + 1), f i ≤ (g n - g (n + 1)) * (C * (n + 1)) := by
  apply mul_le_mul le_rfl (by simpa using hf' (n + 1)) (Finset.sum_nonneg' hf) ?_
  simp ; apply hg' ; simp
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
l1 : ∀ (n : ℕ), (g n - g (n + 1)) * ∑ i ∈ Finset.range (n + 1), f i ≤ (g n - g (n + 1)) * (C * (↑n + 1))
⊢ ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        ((n - 1 - 1) • (C * g 0) - ∑ x ∈ Finset.range (n - 1 - 1), C * g (x + 1)))
Theorem: cancel_aux
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
l1 : ∀ (n : ℕ), (g n - g (n + 1)) * ∑ i ∈ Finset.range (n + 1), f i ≤ (g n - g (n + 1)) * (C * (↑n + 1))
⊢ ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        ((n - 1 - 1) • (C * g 0) - ∑ x ∈ Finset.range (n - 1 - 1), C * g (x + 1)))
Tactic:
have l2 (x : ℕ) : C * (↑(x + 1) + 1) - C * (↑x + 1) = C := by simp ; ring
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
l1 : ∀ (n : ℕ), (g n - g (n + 1)) * ∑ i ∈ Finset.range (n + 1), f i ≤ (g n - g (n + 1)) * (C * (↑n + 1))
l2 : ∀ (x : ℕ), C * (↑(x + 1) + 1) - C * (↑x + 1) = C
⊢ ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        ((n - 1 - 1) • (C * g 0) - ∑ x ∈ Finset.range (n - 1 - 1), C * g (x + 1)))
Theorem: cancel_aux
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
l1 : ∀ (n : ℕ), (g n - g (n + 1)) * ∑ i ∈ Finset.range (n + 1), f i ≤ (g n - g (n + 1)) * (C * (↑n + 1))
l2 : ∀ (x : ℕ), C * (↑(x + 1) + 1) - C * (↑x + 1) = C
⊢ ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        ((n - 1 - 1) • (C * g 0) - ∑ x ∈ Finset.range (n - 1 - 1), C * g (x + 1)))
Tactic:
have l3 (n : ℕ) : 0 ≤ cumsum f n := Finset.sum_nonneg' hf
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
l1 : ∀ (n : ℕ), (g n - g (n + 1)) * ∑ i ∈ Finset.range (n + 1), f i ≤ (g n - g (n + 1)) * (C * (↑n + 1))
l2 : ∀ (x : ℕ), C * (↑(x + 1) + 1) - C * (↑x + 1) = C
l3 : ∀ (n : ℕ), 0 ≤ cumsum f n
⊢ ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        ((n - 1 - 1) • (C * g 0) - ∑ x ∈ Finset.range (n - 1 - 1), C * g (x + 1)))
Theorem: cancel_aux
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
l1 : ∀ (n : ℕ), (g n - g (n + 1)) * ∑ i ∈ Finset.range (n + 1), f i ≤ (g n - g (n + 1)) * (C * (↑n + 1))
l2 : ∀ (x : ℕ), C * (↑(x + 1) + 1) - C * (↑x + 1) = C
l3 : ∀ (n : ℕ), 0 ≤ cumsum f n
⊢ ∑ i ∈ Finset.range n, f i * g i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        ((n - 1 - 1) • (C * g 0) - ∑ x ∈ Finset.range (n - 1 - 1), C * g (x + 1)))
Tactic:
convert_to ∑ i in Finset.range n, (g i) • (f i) ≤ _
Proof state after:
case h.e'_3
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
l1 : ∀ (n : ℕ), (g n - g (n + 1)) * ∑ i ∈ Finset.range (n + 1), f i ≤ (g n - g (n + 1)) * (C * (↑n + 1))
l2 : ∀ (x : ℕ), C * (↑(x + 1) + 1) - C * (↑x + 1) = C
l3 : ∀ (n : ℕ), 0 ≤ cumsum f n
⊢ ∑ i ∈ Finset.range n, f i * g i = ∑ i ∈ Finset.range n, g i • f i

case convert_2
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
f g : ℕ → ℝ
hf : 0 ≤ f
hg : 0 ≤ g
hf' : ∀ (n : ℕ), cumsum f n ≤ C * ↑n
hg' : Antitone g
n : ℕ
l1 : ∀ (n : ℕ), (g n - g (n + 1)) * ∑ i ∈ Finset.range (n + 1), f i ≤ (g n - g (n + 1)) * (C * (↑n + 1))
l2 : ∀ (x : ℕ), C * (↑(x + 1) + 1) - C * (↑x + 1) = C
l3 : ∀ (n : ℕ), 0 ≤ cumsum f n
⊢ ∑ i ∈ Finset.range n, g i • f i ≤
    g (n - 1) * (C * ↑n) +
      (C * (↑(n - 1 - 1) + 1) * g 0 - C * (↑(n - 1 - 1) + 1) * g (n - 1) -
        ((n - 1 - 1) • (C * g 0) - ∑ x ∈ Finset.range (n - 1 - 1), C * g (x + 1)))