internlm/Lean-Github huggingface dataset:
Theorem: WienerIkeharaInterval
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : S ψ ≤ᶠ[atTop] S Iab
l4 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S ψ)
l3 : liminf (S ψ) atTop ≤ liminf (S Iab) atTop
⊢ A * (b - a - ε) ≤ liminf (S ψ) atTop
Tactic:
rw [l1.liminf_eq]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : S ψ ≤ᶠ[atTop] S Iab
l4 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S ψ)
l3 : liminf (S ψ) atTop ≤ liminf (S Iab) atTop
⊢ A * (b - a - ε) ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
Theorem: WienerIkeharaInterval
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
l2 : S ψ ≤ᶠ[atTop] S Iab
l4 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S ψ)
l3 : liminf (S ψ) atTop ≤ liminf (S Iab) atTop
⊢ A * (b - a - ε) ≤ A * ∫ (y : ℝ) in Ioi 0, ψ y
Tactic:
gcongr
Proof state after:
no goals
Theorem: WienerIkeharaInterval
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
ha : 0 < a
hb : a < b
S : (ℝ → ℝ) → ℝ → ℝ := fun g x => (∑' (n : ℕ), f n * g (↑n / x)) / x
hSnonneg : ∀ {g : ℝ → ℝ}, 0 ≤ g → ∀ᶠ (x : ℝ) in atTop, 0 ≤ S g x
hA : 0 ≤ A
Iab : ℝ → ℝ := (Ico a b).indicator 1
hIab : HasCompactSupport Iab
Iab_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ S Iab x
Iab2 : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
Iab3 : IsBoundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab0 : IsCoboundedUnder (fun x x_1 => x ≥ x_1) atTop (S Iab)
Iab1 : IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop (S Iab)
sup_le : limsup (S Iab) atTop ≤ A * (b - a)
ε : ℝ
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : closure (Function.support ψ) ⊆ Ioi 0
h5 : ψ ≤ (Ico a b).indicator 1
h6 : b - a - ε ≤ ∫ (y : ℝ) in Ioi 0, ψ y
l1 : Tendsto (S ψ) atTop (𝓝 (A * ∫ (y : ℝ) in Ioi 0, ψ y))
⊢ S ψ ≤ᶠ[atTop] S Iab
Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx using WI_sum_le hpos h5 hx h2 hIab
Proof state after:
no goals
Theorem: le_floor_mul_iff
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hb : 0 ≤ b
hx : 0 < x
⊢ n ≤ ⌊b * x⌋₊ ↔ ↑n / x ≤ b
Tactic:
rw [div_le_iff hx, Nat.le_floor_iff]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hb : 0 ≤ b
hx : 0 < x
⊢ 0 ≤ b * x
Theorem: le_floor_mul_iff
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hb : 0 ≤ b
hx : 0 < x
⊢ 0 ≤ b * x
Tactic:
positivity
Proof state after:
no goals
Theorem: lt_ceil_mul_iff
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ n < ⌈b * x⌉₊ ↔ ↑n / x < b
Tactic:
rw [div_lt_iff hx, Nat.lt_ceil]
Proof state after:
no goals
Theorem: ceil_mul_le_iff
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ ⌈a * x⌉₊ ≤ n ↔ a ≤ ↑n / x
Tactic:
rw [le_div_iff hx, Nat.ceil_le]
Proof state after:
no goals
Theorem: mem_Icc_iff_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hb : 0 ≤ b
hx : 0 < x
⊢ n ∈ Finset.Icc ⌈a * x⌉₊ ⌊b * x⌋₊ ↔ ↑n / x ∈ Icc a b
Tactic:
rw [Finset.mem_Icc, mem_Icc, ceil_mul_le_iff hx, le_floor_mul_iff hb hx]
Proof state after:
no goals
Theorem: mem_Ico_iff_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
⊢ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊ ↔ ↑n / x ∈ Ico a b
Tactic:
rw [Finset.mem_Ico, mem_Ico, ceil_mul_le_iff hx, lt_ceil_mul_iff hx]
Proof state after:
no goals
Theorem: tsum_indicator
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
⊢ ∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x) = ∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n
Tactic:
have l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * indicator (Ico a b) 1 (↑n / x) = 0 := by
  simp [mem_Ico_iff_div hx] ; tauto
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x) = ∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n
Theorem: tsum_indicator
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x) = ∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n
Tactic:
rw [tsum_eq_sum l1]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∑ b_1 ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f b_1 * (Ico a b).indicator 1 (↑b_1 / x) =
    ∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n
Theorem: tsum_indicator
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∑ b_1 ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f b_1 * (Ico a b).indicator 1 (↑b_1 / x) =
    ∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n
Tactic:
apply Finset.sum_congr rfl
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∀ x_1 ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f x_1 * (Ico a b).indicator 1 (↑x_1 / x) = f x_1
Theorem: tsum_indicator
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∀ x_1 ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f x_1 * (Ico a b).indicator 1 (↑x_1 / x) = f x_1
Tactic:
simp only [mem_Ico_iff_div hx]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∀ (x_1 : ℕ), ↑x_1 / x ∈ Ico a b → f x_1 * (Ico a b).indicator 1 (↑x_1 / x) = f x_1
Theorem: tsum_indicator
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∀ (x_1 : ℕ), ↑x_1 / x ∈ Ico a b → f x_1 * (Ico a b).indicator 1 (↑x_1 / x) = f x_1
Tactic:
intro n hn
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
n : ℕ
hn : ↑n / x ∈ Ico a b
⊢ f n * (Ico a b).indicator 1 (↑n / x) = f n
Theorem: tsum_indicator
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
n : ℕ
hn : ↑n / x ∈ Ico a b
⊢ f n * (Ico a b).indicator 1 (↑n / x) = f n
Tactic:
simp [hn]
Proof state after:
no goals
Theorem: tsum_indicator
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
⊢ ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
Tactic:
simp [mem_Ico_iff_div hx]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
⊢ ∀ (n : ℕ), (a ≤ ↑n / x → b ≤ ↑n / x) → f n = 0 ∨ (a ≤ ↑n / x → b ≤ ↑n / x)
Theorem: tsum_indicator
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
⊢ ∀ (n : ℕ), (a ≤ ↑n / x → b ≤ ↑n / x) → f n = 0 ∨ (a ≤ ↑n / x → b ≤ ↑n / x)
Tactic:
tauto
Proof state after:
no goals
Theorem: WienerIkeharaInterval_discrete
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
ha : 0 < a
hb : a ≤ b
⊢ Tendsto (fun x => (∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n) / x) atTop (𝓝 (A * (b - a)))
Tactic:
apply (WienerIkeharaInterval hpos hf hcheby hG hG' ha hb).congr'
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
ha : 0 < a
hb : a ≤ b
⊢ (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) =ᶠ[atTop] fun x =>
    (∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n) / x
Theorem: WienerIkeharaInterval_discrete
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
ha : 0 < a
hb : a ≤ b
⊢ (fun x => (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x) =ᶠ[atTop] fun x =>
    (∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n) / x
Tactic:
filter_upwards [eventually_gt_atTop 0] 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 : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
ha : 0 < a
hb : a ≤ b
x : ℝ
hx : 0 < x
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x = (∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n) / x
Theorem: WienerIkeharaInterval_discrete
Proof state before:
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm (fun n => ↑(f n)) σ')
hcheby : cheby fun n => ↑(f n)
hG : ContinuousOn G {s | 1 ≤ s.re}
hG' : EqOn G (fun s => LSeries (fun n => ↑(f n)) s - ↑A / (s - 1)) {s | 1 < s.re}
ha : 0 < a
hb : a ≤ b
x : ℝ
hx : 0 < x
⊢ (∑' (n : ℕ), f n * (Ico a b).indicator 1 (↑n / x)) / x = (∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n) / x
Tactic:
rw [tsum_indicator hx]
Proof state after:
no goals
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ Tendsto (fun p => ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2) (𝓝[>] 0 ×ˢ atTop) (𝓝 0)
Tactic:
rw [Metric.tendsto_nhds]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ ∀ ε > 0, ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < ε
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ ∀ ε > 0, ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < ε
Tactic:
intro δ hδ
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
⊢ ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < δ
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
⊢ ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < δ
Tactic:
have l1 : ∀ᶠ ε : ℝ in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2) := inter_mem_nhdsWithin _ (Iio_mem_nhds (by positivity))
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
⊢ ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < δ
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
⊢ ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < δ
Tactic:
have l2 : ∀ᶠ N : ℕ in atTop, 1 ≤ δ / 2 * N := by
  apply Tendsto.eventually_ge_atTop
  exact tendsto_natCast_atTop_atTop.const_mul_atTop (by positivity)
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
⊢ ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < δ
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
⊢ ∀ᶠ (x : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, dist (↑⌈x.1 * ↑x.2⌉₊ / ↑x.2) 0 < δ
Tactic:
filter_upwards [l1.prod_mk l2] with (ε, N) ⟨⟨hε, h1⟩, h2⟩
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < (ε, N).1
h1 : (ε, N).1 < δ / 2
h2 : 1 ≤ δ / 2 * ↑(ε, N).2
⊢ dist (↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2) 0 < δ
Theorem: tendsto_mul_ceil_div
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < (ε, N).1
h1 : (ε, N).1 < δ / 2
h2 : 1 ≤ δ / 2 * ↑(ε, N).2
⊢ dist (↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2) 0 < δ
Tactic:
dsimp only at *
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ
Theorem: tendsto_mul_ceil_div
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ
Tactic:
have l3 : 0 < (N : ℝ) := by
  simp ; rw [Nat.pos_iff_ne_zero] ; rintro rfl ; simp at h2 ; linarith
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ
Theorem: tendsto_mul_ceil_div
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ
Tactic:
have l5 : 0 ≤ ε * ↑N := by positivity
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ
Theorem: tendsto_mul_ceil_div
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ
Tactic:
have l6 : ε * N ≤ δ / 2 * N := mul_le_mul h1.le le_rfl (by positivity) (by positivity)
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
l6 : ε * ↑N ≤ δ / 2 * ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ
Theorem: tendsto_mul_ceil_div
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
l6 : ε * ↑N ≤ δ / 2 * ↑N
⊢ dist (↑⌈ε * ↑N⌉₊ / ↑N) 0 < δ
Tactic:
simp [div_lt_iff l3]
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
l6 : ε * ↑N ≤ δ / 2 * ↑N
⊢ ↑⌈ε * ↑N⌉₊ < δ * ↑N
Theorem: tendsto_mul_ceil_div
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
l6 : ε * ↑N ≤ δ / 2 * ↑N
⊢ ↑⌈ε * ↑N⌉₊ < δ * ↑N
Tactic:
convert (Nat.ceil_lt_add_one l5).trans_le (add_le_add l6 h2) using 1
Proof state after:
case h.e'_4
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
l6 : ε * ↑N ≤ δ / 2 * ↑N
⊢ δ * ↑N = δ / 2 * ↑N + δ / 2 * ↑N
Theorem: tendsto_mul_ceil_div
Proof state before:
case h.e'_4
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
l2 : ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
ε : ℝ
N : ℕ
hε : 0 < ε
h1 : ε < δ / 2
h2 : 1 ≤ δ / 2 * ↑N
l3 : 0 < ↑N
l5 : 0 ≤ ε * ↑N
l6 : ε * ↑N ≤ δ / 2 * ↑N
⊢ δ * ↑N = δ / 2 * ↑N + δ / 2 * ↑N
Tactic:
ring
Proof state after:
no goals
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
⊢ 0 < δ / 2
Tactic:
positivity
Proof state after:
no goals
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
⊢ ∀ᶠ (N : ℕ) in atTop, 1 ≤ δ / 2 * ↑N
Tactic:
apply Tendsto.eventually_ge_atTop
Proof state after:
case hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
⊢ Tendsto (fun x => δ / 2 * ↑x) atTop atTop
Theorem: tendsto_mul_ceil_div
Proof state before:
case hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
⊢ Tendsto (fun x => δ / 2 * ↑x) atTop atTop
Tactic:
exact tendsto_natCast_atTop_atTop.const_mul_atTop (by positivity)
Proof state after:
no goals
Theorem: tendsto_mul_ceil_div
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
δ : ℝ
hδ : δ > 0
l1 : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ε ∈ Ioo 0 (δ / 2)
⊢ 0 < δ / 2
Tactic:
positivity
Proof state after:
no goals