internlm/Lean-Github huggingface dataset:
Theorem: Perron.HolomorphicOn.upperUIntegral_eq_zero
Proof state before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ (↑σ + I * ↑T).re ≤ (↑σ' + I * ↑x✝¹).re
Tactic:
simp [hσ]
Proof state after:
no goals
Theorem: Perron.HolomorphicOn.upperUIntegral_eq_zero
Proof state before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ (↑σ + I * ↑T).im ≤ (↑σ' + I * ↑x✝¹).im
Tactic:
simp [hTU]
Proof state after:
no goals
Theorem: Perron.HolomorphicOn.upperUIntegral_eq_zero
Proof state before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ T ≤ z.im}
htop : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atTop (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ σ ≤ x✝.re → x✝.re ≤ σ' → T ≤ x✝.im → x✝.im ≤ x✝¹ → σ ≤ x✝.re ∧ x✝.re ≤ σ' ∧ T ≤ x✝.im
Tactic:
tauto
Proof state after:
no goals
Theorem: Perron.HolomorphicOn.lowerUIntegral_eq_zero
Proof state before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ LowerUIntegral f σ σ' T = 0
Tactic:
suffices h : - LowerUIntegral f σ σ' T = 0 by exact neg_eq_zero.mp h
Proof state after:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ -LowerUIntegral f σ σ' T = 0
Theorem: Perron.HolomorphicOn.lowerUIntegral_eq_zero
Proof state before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ -LowerUIntegral f σ σ' T = 0
Tactic:
apply tendsto_nhds_unique (RectangleIntegral_tendsTo_LowerU hbot hleft hright)
Proof state after:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 0)
Theorem: Perron.HolomorphicOn.lowerUIntegral_eq_zero
Proof state before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ Tendsto (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) atTop (𝓝 0)
Tactic:
apply EventuallyEq.tendsto
Proof state after:
case hf
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) =ᶠ[atTop] fun x => 0
Theorem: Perron.HolomorphicOn.lowerUIntegral_eq_zero
Proof state before:
case hf
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ (fun U => RectangleIntegral f (↑σ - I * ↑U) (↑σ' - I * ↑T)) =ᶠ[atTop] fun x => 0
Tactic:
filter_upwards [eventually_ge_atTop T]
Proof state after:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ ∀ (a : ℝ), T ≤ a → RectangleIntegral f (↑σ - I * ↑a) (↑σ' - I * ↑T) = 0
Theorem: Perron.HolomorphicOn.lowerUIntegral_eq_zero
Proof state before:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
⊢ ∀ (a : ℝ), T ≤ a → RectangleIntegral f (↑σ - I * ↑a) (↑σ' - I * ↑T) = 0
Tactic:
refine fun _ hTU ↦ hf.vanishesOnRectangle fun _ ↦ ?_
Proof state after:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ x✝ ∈ Rectangle (↑σ - I * ↑x✝¹) (↑σ' - I * ↑T) → x✝ ∈ {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
Theorem: Perron.HolomorphicOn.lowerUIntegral_eq_zero
Proof state before:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ x✝ ∈ Rectangle (↑σ - I * ↑x✝¹) (↑σ' - I * ↑T) → x✝ ∈ {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
Tactic:
rw [mem_Rect (by simp [hσ]) (by simp [hTU])]
Proof state after:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ (↑σ - I * ↑x✝¹).re ≤ x✝.re ∧ x✝.re ≤ (↑σ' - I * ↑T).re ∧ (↑σ - I * ↑x✝¹).im ≤ x✝.im ∧ x✝.im ≤ (↑σ' - I * ↑T).im →
    x✝ ∈ {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
Theorem: Perron.HolomorphicOn.lowerUIntegral_eq_zero
Proof state before:
case h
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ (↑σ - I * ↑x✝¹).re ≤ x✝.re ∧ x✝.re ≤ (↑σ' - I * ↑T).re ∧ (↑σ - I * ↑x✝¹).im ≤ x✝.im ∧ x✝.im ≤ (↑σ' - I * ↑T).im →
    x✝ ∈ {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
Tactic:
simpa using by tauto
Proof state after:
no goals
Theorem: Perron.HolomorphicOn.lowerUIntegral_eq_zero
Proof state before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
h : -LowerUIntegral f σ σ' T = 0
⊢ LowerUIntegral f σ σ' T = 0
Tactic:
exact neg_eq_zero.mp h
Proof state after:
no goals
Theorem: Perron.HolomorphicOn.lowerUIntegral_eq_zero
Proof state before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ (↑σ - I * ↑x✝¹).re ≤ (↑σ' - I * ↑T).re
Tactic:
simp [hσ]
Proof state after:
no goals
Theorem: Perron.HolomorphicOn.lowerUIntegral_eq_zero
Proof state before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ (↑σ - I * ↑x✝¹).im ≤ (↑σ' - I * ↑T).im
Tactic:
simp [hTU]
Proof state after:
no goals
Theorem: Perron.HolomorphicOn.lowerUIntegral_eq_zero
Proof state before:
x σ✝ σ'✝ σ'' T✝ : ℝ
f : ℂ → ℂ
σ σ' T : ℝ
hσ : σ ≤ σ'
hf : HolomorphicOn f {z | σ ≤ z.re ∧ z.re ≤ σ' ∧ z.im ≤ -T}
hbot : Tendsto (fun y => ∫ (x : ℝ) in σ..σ', f (↑x + ↑y * I)) atBot (𝓝 0)
hleft : Integrable (fun y => f (↑σ + ↑y * I)) volume
hright : Integrable (fun y => f (↑σ' + ↑y * I)) volume
x✝¹ : ℝ
hTU : T ≤ x✝¹
x✝ : ℂ
⊢ σ ≤ x✝.re → x✝.re ≤ σ' → -x✝¹ ≤ x✝.im → x✝.im ≤ -T → σ ≤ x✝.re ∧ x✝.re ≤ σ' ∧ x✝.im ≤ -T
Tactic:
tauto
Proof state after:
no goals
Theorem: Perron.keyIdentity
Proof state before:
x✝ σ σ' σ'' T x : ℝ
s : ℂ
s_ne_zero : s ≠ 0
s_ne_neg_one : s ≠ -1
⊢ ↑x ^ s / (s * (s + 1)) = ↑x ^ s / s - ↑x ^ s / (s + 1)
Tactic:
field_simp [sPlusOneNeZero, mul_ne_zero]
Proof state after:
x✝ σ σ' σ'' T x : ℝ
s : ℂ
s_ne_zero : s ≠ 0
s_ne_neg_one : s ≠ -1
⊢ ↑x ^ s = ↑x ^ s * (s + 1) - s * ↑x ^ s
Theorem: Perron.keyIdentity
Proof state before:
x✝ σ σ' σ'' T x : ℝ
s : ℂ
s_ne_zero : s ≠ 0
s_ne_neg_one : s ≠ -1
⊢ ↑x ^ s = ↑x ^ s * (s + 1) - s * ↑x ^ s
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Filter.Tendsto.eventually_bddAbove
Proof state before:
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
⊢ ∀ᶠ (s : Set α) in l.smallSets, BddAbove (f '' s)
Tactic:
obtain ⟨y', hy'⟩ := exists_gt y
Proof state after:
case intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
y' : β
hy' : y < y'
⊢ ∀ᶠ (s : Set α) in l.smallSets, BddAbove (f '' s)
Theorem: Filter.Tendsto.eventually_bddAbove
Proof state before:
case intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
y' : β
hy' : y < y'
⊢ ∀ᶠ (s : Set α) in l.smallSets, BddAbove (f '' s)
Tactic:
obtain ⟨s, hsl, hs⟩ := (eventually_le_of_tendsto_lt hy' hf).exists_mem
Proof state after:
case intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
y' : β
hy' : y < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
⊢ ∀ᶠ (s : Set α) in l.smallSets, BddAbove (f '' s)
Theorem: Filter.Tendsto.eventually_bddAbove
Proof state before:
case intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
y' : β
hy' : y < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
⊢ ∀ᶠ (s : Set α) in l.smallSets, BddAbove (f '' s)
Tactic:
simp_rw [Filter.eventually_smallSets, bddAbove_def]
Proof state after:
case intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
y' : β
hy' : y < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
⊢ ∃ s ∈ l, ∀ t ⊆ s, ∃ x, ∀ y ∈ f '' t, y ≤ x
Theorem: Filter.Tendsto.eventually_bddAbove
Proof state before:
case intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y)
y' : β
hy' : y < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
⊢ ∃ s ∈ l, ∀ t ⊆ s, ∃ x, ∀ y ∈ f '' t, y ≤ x
Tactic:
refine ⟨s, hsl, fun t ht ↦ ⟨y', fun y hy ↦ ?_⟩⟩
Proof state after:
case intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y✝ : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y✝)
y' : β
hy' : y✝ < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
t : Set α
ht : t ⊆ s
y : β
hy : y ∈ f '' t
⊢ y ≤ y'
Theorem: Filter.Tendsto.eventually_bddAbove
Proof state before:
case intro.intro.intro
x σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y✝ : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y✝)
y' : β
hy' : y✝ < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
t : Set α
ht : t ⊆ s
y : β
hy : y ∈ f '' t
⊢ y ≤ y'
Tactic:
obtain ⟨x, hxt, hxy⟩ := hy
Proof state after:
case intro.intro.intro.intro.intro
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y✝ : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y✝)
y' : β
hy' : y✝ < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
t : Set α
ht : t ⊆ s
y : β
x : α
hxt : x ∈ t
hxy : f x = y
⊢ y ≤ y'
Theorem: Filter.Tendsto.eventually_bddAbove
Proof state before:
case intro.intro.intro.intro.intro
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y✝ : β
l : Filter α
f : α → β
hf : Tendsto f l (𝓝 y✝)
y' : β
hy' : y✝ < y'
s : Set α
hsl : s ∈ l
hs : ∀ y ∈ s, f y ≤ y'
t : Set α
ht : t ⊆ s
y : β
x : α
hxt : x ∈ t
hxy : f x = y
⊢ y ≤ y'
Tactic:
exact hxy ▸ hs x (ht hxt)
Proof state after:
no goals
Theorem: Perron.bddAbove_square_of_tendsto
Proof state before:
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove (f '' (Square x c \ {x}))
Tactic:
obtain ⟨t, htf, ht⟩ := eventually_smallSets.mp hf.eventually_bddAbove
Proof state after:
case intro.intro
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
t : Set ℂ
htf : t ∈ 𝓝[≠] x
ht : ∀ t_1 ⊆ t, BddAbove (f '' t_1)
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove (f '' (Square x c \ {x}))
Theorem: Perron.bddAbove_square_of_tendsto
Proof state before:
case intro.intro
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
t : Set ℂ
htf : t ∈ 𝓝[≠] x
ht : ∀ t_1 ⊆ t, BddAbove (f '' t_1)
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove (f '' (Square x c \ {x}))
Tactic:
obtain ⟨ε, hε0, hε⟩ := nhdsWithin_hasBasis (nhds_hasBasis_square x) {x}ᶜ |>.1 t |>.mp htf
Proof state after:
case intro.intro.intro.intro
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
t : Set ℂ
htf : t ∈ 𝓝[≠] x
ht : ∀ t_1 ⊆ t, BddAbove (f '' t_1)
ε : ℝ
hε0 : 0 < ε
hε : Square x ε ∩ {x}ᶜ ⊆ t
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove (f '' (Square x c \ {x}))
Theorem: Perron.bddAbove_square_of_tendsto
Proof state before:
case intro.intro.intro.intro
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
t : Set ℂ
htf : t ∈ 𝓝[≠] x
ht : ∀ t_1 ⊆ t, BddAbove (f '' t_1)
ε : ℝ
hε0 : 0 < ε
hε : Square x ε ∩ {x}ᶜ ⊆ t
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove (f '' (Square x c \ {x}))
Tactic:
filter_upwards [Ioo_mem_nhdsWithin_Ioi' hε0] with ε' ⟨hε'0, hε'⟩
Proof state after:
case h
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
t : Set ℂ
htf : t ∈ 𝓝[≠] x
ht : ∀ t_1 ⊆ t, BddAbove (f '' t_1)
ε : ℝ
hε0 : 0 < ε
hε : Square x ε ∩ {x}ᶜ ⊆ t
ε' : ℝ
hε'0 : 0 < ε'
hε' : ε' < ε
⊢ BddAbove (f '' (Square x ε' \ {x}))
Theorem: Perron.bddAbove_square_of_tendsto
Proof state before:
case h
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
f : ℂ → β
x : ℂ
hf : Tendsto f (𝓝[≠] x) (𝓝 y)
t : Set ℂ
htf : t ∈ 𝓝[≠] x
ht : ∀ t_1 ⊆ t, BddAbove (f '' t_1)
ε : ℝ
hε0 : 0 < ε
hε : Square x ε ∩ {x}ᶜ ⊆ t
ε' : ℝ
hε'0 : 0 < ε'
hε' : ε' < ε
⊢ BddAbove (f '' (Square x ε' \ {x}))
Tactic:
exact ht _ <| (diff_subset_diff (square_subset_square hε'0 hε'.le) subset_rfl).trans hε
Proof state after:
no goals
Theorem: Perron.diffBddAtZero
Proof state before:
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ ∀ᶠ (c : ℝ) in 𝓝[>] 0, BddAbove ((Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) '' (Square 0 c \ {0}))
Tactic:
apply bddAbove_square_of_tendsto
Proof state after:
case hf
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) (𝓝[≠] 0) (𝓝 ?y)

case y
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ ℝ
Theorem: Perron.diffBddAtZero
Proof state before:
case hf
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) (𝓝[≠] 0) (𝓝 ?y)

case y
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ ℝ
Tactic:
suffices Tendsto (norm ∘ (fun (s : ℂ) ↦ ↑x ^ s / s - ↑x ^ (0 : ℂ) / s - ↑x ^ s / (1 + s)))
    (𝓝[≠] 0) (𝓝 (‖(deriv (fun (s : ℂ) ↦ (x : ℂ) ^ s) 0) - x ^ (0 : ℂ) / (1 + 0)‖)) by
  apply this.congr'
  filter_upwards [diff_mem_nhdsWithin_compl (isOpen_compl_singleton.mem_nhds
    (Set.mem_compl_singleton_iff.mpr (by norm_num : (0 : ℂ) ≠ -1))) {0}] with s hs
  rw [Function.comp_apply, Function.comp_apply, keyIdentity _ hs.2 hs.1, cpow_zero]; ring_nf
Proof state after:
case hf
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
Theorem: Perron.diffBddAtZero
Proof state before:
case hf
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
Tactic:
have hx0 : (x : ℂ) ≠ 0 := slitPlane_ne_zero (.inl xpos)
Proof state after:
case hf
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
Theorem: Perron.diffBddAtZero
Proof state before:
case hf
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
Tactic:
refine (Tendsto.sub ?_ (tendsto_nhdsWithin_of_tendsto_nhds ?_)).norm
Proof state after:
case hf.refine_1
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
⊢ Tendsto (fun x_1 => ↑x ^ x_1 / x_1 - ↑x ^ 0 / x_1) (𝓝[≠] 0) (𝓝 (deriv (fun s => ↑x ^ s) 0))

case hf.refine_2
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
hx0 : ↑x ≠ 0
⊢ Tendsto (fun x_1 => ↑x ^ x_1 / (1 + x_1)) (𝓝 0) (𝓝 (↑x ^ 0 / (1 + 0)))
Theorem: Perron.diffBddAtZero
Proof state before:
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
this :
  Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
⊢ Tendsto (Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) (𝓝[≠] 0) (𝓝 ?y)
Tactic:
apply this.congr'
Proof state after:
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
this :
  Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
⊢ (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) =ᶠ[𝓝[≠] 0]
    Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s
Theorem: Perron.diffBddAtZero
Proof state before:
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
this :
  Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
⊢ (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) =ᶠ[𝓝[≠] 0]
    Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s
Tactic:
filter_upwards [diff_mem_nhdsWithin_compl (isOpen_compl_singleton.mem_nhds
  (Set.mem_compl_singleton_iff.mpr (by norm_num : (0 : ℂ) ≠ -1))) {0}] with s hs
Proof state after:
case h
x✝ σ σ' σ'' T : ℝ
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder β
inst✝¹ : TopologicalSpace β
inst✝ : ClosedIciTopology β
y : β
l : Filter α
x : ℝ
xpos : 0 < x
this :
  Tendsto (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) (𝓝[≠] 0)
    (𝓝 ‖deriv (fun s => ↑x ^ s) 0 - ↑x ^ 0 / (1 + 0)‖)
s : ℂ
hs : s ∈ {-1}ᶜ \ {0}
⊢ (Norm.norm ∘ fun s => ↑x ^ s / s - ↑x ^ 0 / s - ↑x ^ s / (1 + s)) s =
    (Norm.norm ∘ fun s => ↑x ^ s / (s * (s + 1)) - 1 / s) s