internlm/Lean-Github huggingface dataset:
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro.intro.intro.hF_meas.hf.hg
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
⊢ ↑x ≠ 0 ∨ ∀ (a : ℝ), ↑a * I ≠ 0
Tactic:
simp
Proof state after:
case neg.intro.intro.intro.hF_meas.hf.hg
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
⊢ ¬x = 0
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro.intro.intro.hF_meas.hf.hg
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
⊢ ¬x = 0
Tactic:
linarith
Proof state after:
no goals
Theorem: limiting_fourier_lim3
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
⊢ Continuous fun x => ↑x * I
Tactic:
continuity
Proof state after:
no goals
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro.intro.intro.h_bound
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 1, ∀ᵐ (a : ℝ), ‖G (↑n + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)‖ ≤ bound a
Tactic:
apply eventually_of_mem (U := Icc 1 2) (Icc_mem_nhdsWithin_Ioi (by simp))
Proof state after:
case neg.intro.intro.intro.h_bound
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
⊢ ∀ x_1 ∈ Icc 1 2, ∀ᵐ (a : ℝ), ‖G (↑x_1 + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)‖ ≤ bound a
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro.intro.intro.h_bound
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
⊢ ∀ x_1 ∈ Icc 1 2, ∀ᵐ (a : ℝ), ‖G (↑x_1 + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)‖ ≤ bound a
Tactic:
intro u hu
Proof state after:
case neg.intro.intro.intro.h_bound
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
⊢ ∀ᵐ (a : ℝ), ‖G (↑u + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)‖ ≤ bound a
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro.intro.intro.h_bound
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
⊢ ∀ᵐ (a : ℝ), ‖G (↑u + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)‖ ≤ bound a
Tactic:
apply eventually_of_forall
Proof state after:
case neg.intro.intro.intro.h_bound.hp
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
⊢ ∀ (x_1 : ℝ), ‖G (↑u + ↑x_1 * I) * ψ.toFun x_1 * ↑x ^ (↑x_1 * I)‖ ≤ bound x_1
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro.intro.intro.h_bound.hp
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
⊢ ∀ (x_1 : ℝ), ‖G (↑u + ↑x_1 * I) * ψ.toFun x_1 * ↑x ^ (↑x_1 * I)‖ ≤ bound x_1
Tactic:
intro v
Proof state after:
case neg.intro.intro.intro.h_bound.hp
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
⊢ ‖G (↑u + ↑v * I) * ψ.toFun v * ↑x ^ (↑v * I)‖ ≤ bound v
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro.intro.intro.h_bound.hp
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
⊢ ‖G (↑u + ↑v * I) * ψ.toFun v * ↑x ^ (↑v * I)‖ ≤ bound v
Tactic:
by_cases h : v ∈ tsupport ψ
Proof state after:
case pos
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
⊢ ‖G (↑u + ↑v * I) * ψ.toFun v * ↑x ^ (↑v * I)‖ ≤ bound v

case neg
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∉ tsupport ψ.toFun
⊢ ‖G (↑u + ↑v * I) * ψ.toFun v * ↑x ^ (↑v * I)‖ ≤ bound v
Theorem: limiting_fourier_lim3
Proof state before:
case pos
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
⊢ ‖G (↑u + ↑v * I) * ψ.toFun v * ↑x ^ (↑v * I)‖ ≤ bound v
Tactic:
have r1 : u + v * I ∈ S := by simp [S, mem_reProdIm, hu.1, hu.2, h]
Proof state after:
case pos
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
⊢ ‖G (↑u + ↑v * I) * ψ.toFun v * ↑x ^ (↑v * I)‖ ≤ bound v
Theorem: limiting_fourier_lim3
Proof state before:
case pos
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
⊢ ‖G (↑u + ↑v * I) * ψ.toFun v * ↑x ^ (↑v * I)‖ ≤ bound v
Tactic:
have r2 := isMaxOn_iff.mp hmax _ r1
Proof state after:
case pos
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
⊢ ‖G (↑u + ↑v * I) * ψ.toFun v * ↑x ^ (↑v * I)‖ ≤ bound v
Theorem: limiting_fourier_lim3
Proof state before:
case pos
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
⊢ ‖G (↑u + ↑v * I) * ψ.toFun v * ↑x ^ (↑v * I)‖ ≤ bound v
Tactic:
have r4 : (x : ℂ) ≠ 0 := by simp ; linarith
Proof state after:
case pos
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
r4 : ↑x ≠ 0
⊢ ‖G (↑u + ↑v * I) * ψ.toFun v * ↑x ^ (↑v * I)‖ ≤ bound v
Theorem: limiting_fourier_lim3
Proof state before:
case pos
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
r4 : ↑x ≠ 0
⊢ ‖G (↑u + ↑v * I) * ψ.toFun v * ↑x ^ (↑v * I)‖ ≤ bound v
Tactic:
have r5 : arg x = 0 := by simp [arg_eq_zero_iff] ; linarith
Proof state after:
case pos
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
r4 : ↑x ≠ 0
r5 : (↑x).arg = 0
⊢ ‖G (↑u + ↑v * I) * ψ.toFun v * ↑x ^ (↑v * I)‖ ≤ bound v
Theorem: limiting_fourier_lim3
Proof state before:
case pos
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
r4 : ↑x ≠ 0
r5 : (↑x).arg = 0
⊢ ‖G (↑u + ↑v * I) * ψ.toFun v * ↑x ^ (↑v * I)‖ ≤ bound v
Tactic:
have r3 : ‖(x : ℂ) ^ (v * I)‖ = 1 := by simp [abs_cpow_of_ne_zero r4, r5]
Proof state after:
case pos
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
r4 : ↑x ≠ 0
r5 : (↑x).arg = 0
r3 : ‖↑x ^ (↑v * I)‖ = 1
⊢ ‖G (↑u + ↑v * I) * ψ.toFun v * ↑x ^ (↑v * I)‖ ≤ bound v
Theorem: limiting_fourier_lim3
Proof state before:
case pos
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
r4 : ↑x ≠ 0
r5 : (↑x).arg = 0
r3 : ‖↑x ^ (↑v * I)‖ = 1
⊢ ‖G (↑u + ↑v * I) * ψ.toFun v * ↑x ^ (↑v * I)‖ ≤ bound v
Tactic:
simp_rw [norm_mul, r3, mul_one]
Proof state after:
case pos
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
r4 : ↑x ≠ 0
r5 : (↑x).arg = 0
r3 : ‖↑x ^ (↑v * I)‖ = 1
⊢ ‖G (↑u + ↑v * I)‖ * ‖ψ.toFun v‖ ≤ bound v
Theorem: limiting_fourier_lim3
Proof state before:
case pos
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
r4 : ↑x ≠ 0
r5 : (↑x).arg = 0
r3 : ‖↑x ^ (↑v * I)‖ = 1
⊢ ‖G (↑u + ↑v * I)‖ * ‖ψ.toFun v‖ ≤ bound v
Tactic:
exact mul_le_mul_of_nonneg_right r2 (norm_nonneg _)
Proof state after:
no goals
Theorem: limiting_fourier_lim3
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
⊢ ↑u + ↑v * I ∈ S
Tactic:
simp [S, mem_reProdIm, hu.1, hu.2, h]
Proof state after:
no goals
Theorem: limiting_fourier_lim3
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
⊢ ↑x ≠ 0
Tactic:
simp
Proof state after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
⊢ ¬x = 0
Theorem: limiting_fourier_lim3
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
⊢ ¬x = 0
Tactic:
linarith
Proof state after:
no goals
Theorem: limiting_fourier_lim3
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
r4 : ↑x ≠ 0
⊢ (↑x).arg = 0
Tactic:
simp [arg_eq_zero_iff]
Proof state after:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
r4 : ↑x ≠ 0
⊢ 0 ≤ x
Theorem: limiting_fourier_lim3
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
r4 : ↑x ≠ 0
⊢ 0 ≤ x
Tactic:
linarith
Proof state after:
no goals
Theorem: limiting_fourier_lim3
Proof state before:
n : ℕ
A a b c d u✝ x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hG : ContinuousOn G {s | 1 ≤ s.re}
ψ : CS 2 ℂ
hx : 1 ≤ x
hh : ¬tsupport ψ.toFun = ∅
a₀ : ℝ
ha₀ : a₀ ∈ tsupport ψ.toFun
S : Set ℂ := Icc 1 2 ×ℂ tsupport ψ.toFun
l1 : IsCompact S
l2 : S ⊆ {s | 1 ≤ s.re}
l3 : ContinuousOn (fun x => ‖G x‖) S
l4 : S.Nonempty
z : ℂ
hmax : IsMaxOn (fun x => ‖G x‖) S z
MG : ℝ := ‖G z‖
bound : ℝ → ℝ := fun a => MG * ‖ψ.toFun a‖
u : ℝ
hu : u ∈ Icc 1 2
v : ℝ
h : v ∈ tsupport ψ.toFun
r1 : ↑u + ↑v * I ∈ S
r2 : ‖G (↑u + ↑v * I)‖ ≤ ‖G z‖
r4 : ↑x ≠ 0
r5 : (↑x).arg = 0
⊢ ‖↑x ^ (↑v * I)‖ = 1
Tactic:
simp [abs_cpow_of_ne_zero r4, r5]
Proof state after:
no goals