internlm/Lean-Github huggingface dataset:
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 = ∅
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))

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 = ∅
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Tactic:
simp [tsupport_eq_empty_iff.mp hh]
Proof state after:
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 = ∅
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Theorem: limiting_fourier_lim3
Proof state before:
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 = ∅
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Tactic:
obtain ⟨a₀, ha₀⟩ := Set.nonempty_iff_ne_empty.mpr hh
Proof state after:
case neg.intro
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
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro
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
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Tactic:
let S : Set ℂ := Set.reProdIm (Icc 1 2) (tsupport ψ)
Proof state after:
case neg.intro
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
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro
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
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Tactic:
have l2 : S ⊆ {s : ℂ | 1 ≤ s.re} := fun z hz => (mem_reProdIm.mp hz).1.1
Proof state after:
case neg.intro
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}
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro
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
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Tactic:
have l4 : S.Nonempty := ⟨1 + a₀ * I, by simp [S, mem_reProdIm, ha₀]⟩
Proof state after:
case neg.intro
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
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro
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
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Tactic:
obtain ⟨z, -, hmax⟩ := l1.exists_isMaxOn l4 l3
Proof state after:
case neg.intro.intro.intro
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
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro.intro.intro
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
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Tactic:
let MG := ‖G z‖
Proof state after:
case neg.intro.intro.intro
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‖
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro.intro.intro
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‖
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Tactic:
let bound (a : ℝ) : ℝ := MG * ‖ψ a‖
Proof state after:
case neg.intro.intro.intro
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‖
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro.intro.intro
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‖
⊢ Tendsto (fun σ' => ∫ (t : ℝ), G (↑σ' + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)) (𝓝[>] 1)
    (𝓝 (∫ (t : ℝ), G (1 + ↑t * I) * ψ.toFun t * ↑x ^ (↑t * I)))
Tactic:
apply tendsto_integral_filter_of_dominated_convergence (bound := bound)
Proof state after:
case neg.intro.intro.intro.hF_meas
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, AEStronglyMeasurable (fun a => G (↑n + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)) volume

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

case neg.intro.intro.intro.bound_integrable
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‖
⊢ Integrable bound volume

case neg.intro.intro.intro.h_lim
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‖
⊢ ∀ᵐ (a : ℝ),
    Tendsto (fun n => G (↑n + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)) (𝓝[>] 1)
      (𝓝 (G (1 + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)))
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
⊢ IsCompact S
Tactic:
refine Metric.isCompact_iff_isClosed_bounded.mpr ⟨?_, ?_⟩
Proof state after:
case refine_1
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
⊢ IsClosed S

case refine_2
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
⊢ Bornology.IsBounded S
Theorem: limiting_fourier_lim3
Proof state before:
case refine_1
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
⊢ IsClosed S
Tactic:
exact isClosed_Icc.reProdIm (isClosed_tsupport ψ)
Proof state after:
no goals
Theorem: limiting_fourier_lim3
Proof state before:
case refine_2
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
⊢ Bornology.IsBounded S
Tactic:
exact (Metric.isBounded_Icc 1 2).reProdIm ψ.h2.isBounded
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
⊢ 1 + ↑a₀ * I ∈ S
Tactic:
simp [S, mem_reProdIm, ha₀]
Proof state after:
no goals
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro.intro.intro.hF_meas
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, AEStronglyMeasurable (fun a => G (↑n + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)) volume
Tactic:
apply eventually_of_mem (U := Icc 1 2) (Icc_mem_nhdsWithin_Ioi (by simp))
Proof state after:
case neg.intro.intro.intro.hF_meas
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, AEStronglyMeasurable (fun a => G (↑x_1 + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)) volume
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro.intro.intro.hF_meas
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, AEStronglyMeasurable (fun a => G (↑x_1 + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)) volume
Tactic:
intro u hu
Proof state after:
case neg.intro.intro.intro.hF_meas
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
⊢ AEStronglyMeasurable (fun a => G (↑u + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)) volume
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro.intro.intro.hF_meas
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
⊢ AEStronglyMeasurable (fun a => G (↑u + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)) volume
Tactic:
apply Continuous.aestronglyMeasurable
Proof state after:
case neg.intro.intro.intro.hF_meas.hf
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 a => G (↑u + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro.intro.intro.hF_meas.hf
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 a => G (↑u + ↑a * I) * ψ.toFun a * ↑x ^ (↑a * I)
Tactic:
apply Continuous.mul
Proof state after:
case neg.intro.intro.intro.hF_meas.hf.hf
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 => G (↑u + ↑x * I) * ψ.toFun x

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
⊢ Continuous fun x_1 => ↑x ^ (↑x_1 * I)
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‖
⊢ 1 ∈ Ico 1 2
Tactic:
simp
Proof state after:
no goals
Theorem: limiting_fourier_lim3
Proof state before:
case neg.intro.intro.intro.hF_meas.hf.hf
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 => G (↑u + ↑x * I) * ψ.toFun x
Tactic:
exact (hG.comp_continuous (by continuity) (by simp [hu.1])).mul ψ.h1.continuous
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 => ↑u + ↑x * I
Tactic:
continuity
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
⊢ ∀ (x : ℝ), ↑u + ↑x * I ∈ {s | 1 ≤ s.re}
Tactic:
simp [hu.1]
Proof state after:
no goals
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
⊢ Continuous fun x_1 => ↑x ^ (↑x_1 * I)
Tactic:
apply Continuous.const_cpow (by continuity)
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 ∨ ∀ (a : ℝ), ↑a * I ≠ 0