internlm/Lean-Github huggingface dataset:
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case pos
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∈ Ioo a d
this✝ : Ψ x ∈ range Ψ
this : Ψ x ∈ Icc 0 1
⊢ Ψ x ≤ 1 x
Tactic:
simpa using this.2
Proof state after:
no goals
Theorem: smooth_urysohn_support_Ioo
Proof state before:
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∈ Ioo a d
⊢ Ψ x ∈ range Ψ
Tactic:
simp only [Set.mem_range, exists_apply_eq_apply]
Proof state after:
no goals
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case neg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ∉ Ioo a d
⊢ Ψ x ≤ 0
Tactic:
simp only [Set.mem_Ioo, Pi.one_apply] at *
Proof state after:
case neg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : ¬(a < x ∧ x < d)
⊢ Ψ x ≤ 0
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case neg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : ¬(a < x ∧ x < d)
⊢ Ψ x ≤ 0
Tactic:
simp only [not_and_or, not_lt] at h
Proof state after:
case neg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ≤ a ∨ d ≤ x
⊢ Ψ x ≤ 0
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case neg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : x ≤ a ∨ d ≤ x
⊢ Ψ x ≤ 0
Tactic:
simp_rw [hΨ0 x] at h
Proof state after:
case neg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : Ψ x = 0
⊢ Ψ x ≤ 0
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case neg
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
x : ℝ
h : Ψ x = 0
⊢ Ψ x ≤ 0
Tactic:
exact Eq.le h
Proof state after:
no goals
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.right.right.right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ Function.support Ψ = Ioo a d
Tactic:
simp_rw [Function.support, ne_eq, ←hΨ0]
Proof state after:
case h.right.right.right.right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ {x | ¬(x ≤ a ∨ d ≤ x)} = Ioo a d
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.right.right.right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ {x | ¬(x ≤ a ∨ d ≤ x)} = Ioo a d
Tactic:
push_neg
Proof state after:
case h.right.right.right.right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ {x | a < x ∧ x < d} = Ioo a d
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h.right.right.right.right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ {x | a < x ∧ x < d} = Ioo a d
Tactic:
simp [Set.ext_iff]
Proof state after:
no goals
Theorem: nterm_eq_norm_term
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℂ
⊢ nterm f σ' n = ‖term f (↑σ') n‖
Tactic:
by_cases h : n = 0 <;> simp [nterm, term, h]
Proof state after:
no goals
Theorem: hf_coe1
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ↑‖term f (↑σ') i‖₊ ≠ ⊤
Tactic:
simp_rw [ENNReal.tsum_coe_ne_top_iff_summable_coe, ← norm_toNNReal]
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hσ : 1 < σ'
⊢ Summable fun a => ↑‖term f (↑σ') a‖.toNNReal
Theorem: hf_coe1
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hσ : 1 < σ'
⊢ Summable fun a => ↑‖term f (↑σ') a‖.toNNReal
Tactic:
norm_cast
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hσ : 1 < σ'
⊢ Summable fun a => ‖term f (↑σ') a‖.toNNReal
Theorem: hf_coe1
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hσ : 1 < σ'
⊢ Summable fun a => ‖term f (↑σ') a‖.toNNReal
Tactic:
apply Summable.toNNReal
Proof state after:
case hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hσ : 1 < σ'
⊢ Summable fun n => ‖term f (↑σ') n‖
Theorem: hf_coe1
Proof state before:
case hf
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hσ : 1 < σ'
⊢ Summable fun n => ‖term f (↑σ') n‖
Tactic:
convert hf σ' hσ with i
Proof state after:
case h.e'_5.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hσ : 1 < σ'
i : ℕ
⊢ ‖term f (↑σ') i‖ = nterm f σ' i
Theorem: hf_coe1
Proof state before:
case h.e'_5.h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hσ : 1 < σ'
i : ℕ
⊢ ‖term f (↑σ') i‖ = nterm f σ' i
Tactic:
simp [nterm_eq_norm_term]
Proof state after:
no goals
Theorem: first_fourier_aux1
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hψ : Continuous ψ
x : ℝ
n : ℕ
⊢ Measurable fun u => ↑‖𝐞 (-(u * (1 / (2 * π) * (↑n / x).log))) • ψ u‖₊
Tactic:
refine Measurable.comp ?_ (by fun_prop) |>.smul (by fun_prop)
  |>.nnnorm |>.coe_nnreal_ennreal
Proof state after:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hψ : Continuous ψ
x : ℝ
n : ℕ
⊢ Measurable ⇑𝐞
Theorem: first_fourier_aux1
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hψ : Continuous ψ
x : ℝ
n : ℕ
⊢ Measurable ⇑𝐞
Tactic:
exact Continuous.measurable Real.continuous_fourierChar
Proof state after:
no goals
Theorem: first_fourier_aux1
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hψ : Continuous ψ
x : ℝ
n : ℕ
⊢ Measurable fun u => -(u * (1 / (2 * π) * (↑n / x).log))
Tactic:
fun_prop
Proof state after:
no goals
Theorem: first_fourier_aux1
Proof state before:
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hψ : Continuous ψ
x : ℝ
n : ℕ
⊢ Measurable fun u => ψ u
Tactic:
fun_prop
Proof state after:
no goals
Theorem: first_fourier_aux2a
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) = -(↑y * ↑(↑n / x).log)
Tactic:
calc
  _ = -(y * (((2 : ℂ) * π) / (2 * π) * Real.log ((n) / x))) := by ring
  _ = _ := by rw [div_self (by norm_num; exact pi_ne_zero), one_mul]
Proof state after:
no goals
Theorem: first_fourier_aux2a
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) = -(↑y * (2 * ↑π / (2 * ↑π) * ↑(↑n / x).log))
Tactic:
ring
Proof state after:
no goals
Theorem: first_fourier_aux2a
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ -(↑y * (2 * ↑π / (2 * ↑π) * ↑(↑n / x).log)) = -(↑y * ↑(↑n / x).log)
Tactic:
rw [div_self (by norm_num; exact pi_ne_zero), one_mul]
Proof state after:
no goals
Theorem: first_fourier_aux2a
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ 2 * ↑π ≠ 0
Tactic:
norm_num
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ ¬π = 0
Theorem: first_fourier_aux2a
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
⊢ ¬π = 0
Tactic:
exact pi_ne_zero
Proof state after:
no goals
Theorem: first_fourier_aux2
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))
Tactic:
by_cases hn : n = 0
Proof state after:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : n = 0
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))

case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))
Theorem: first_fourier_aux2
Proof state before:
case pos
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : n = 0
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))

case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))
Tactic:
simp [term, hn]
Proof state after:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))
Theorem: first_fourier_aux2
Proof state before:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ term f (↑σ') n * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = term f (↑σ' + ↑y * I) n • (ψ y * ↑x ^ (↑y * I))
Tactic:
simp only [term, hn, ↓reduceIte, fourierChar_apply]
Proof state after:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n / ↑n ^ ↑σ' * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = (f n / ↑n ^ (↑σ' + ↑y * I)) • (ψ y * ↑x ^ (↑y * I))
Theorem: first_fourier_aux2
Proof state before:
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n / ↑n ^ ↑σ' * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = (f n / ↑n ^ (↑σ' + ↑y * I)) • (ψ y * ↑x ^ (↑y * I))
Tactic:
calc
  _ = (f n * (cexp ((2 * π * -(y * (1 / (2 * π) * Real.log (n / x)))) * I) / ↑((n : ℝ) ^ σ'))) • ψ y := by
    have : ((↑n : ℂ) ^ (σ' : ℂ) : ℂ) = ((↑n : ℝ) ^ (σ' : ℝ) : ℝ) := by
      rw [Complex.cpow_def_of_ne_zero (by simp [hn]), Real.rpow_def_of_nonneg (Nat.cast_nonneg n)]
      simp [hn]
    simp [Real.fourierChar, expMapCircle, smul_eq_mul, mul_assoc, this] ; ring
  _ = (f n * (x ^ (y * I) / n ^ (σ' + y * I))) • ψ y := by
    congr 2
    have l1 : 0 < (n : ℝ) := by simpa using Nat.pos_iff_ne_zero.mpr hn
    have l2 : (x : ℂ) ≠ 0 := by simp [hx.ne.symm]
    have l3 : (n : ℂ) ≠ 0 := by simp [hn]
    rw [Real.rpow_def_of_pos l1, Complex.cpow_def_of_ne_zero l2, Complex.cpow_def_of_ne_zero l3]
    push_cast
    simp_rw [← Complex.exp_sub]
    congr 1
    rw [first_fourier_aux2a, Real.log_div l1.ne.symm hx.ne.symm]
    push_cast
    rw [Complex.ofReal_log hx.le]
    ring
  _ = _ := by simp ; group
Proof state after:
no goals
Theorem: first_fourier_aux2
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n / ↑n ^ ↑σ' * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    (f n * (cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ'))) • ψ y
Tactic:
have : ((↑n : ℂ) ^ (σ' : ℂ) : ℂ) = ((↑n : ℝ) ^ (σ' : ℝ) : ℝ) := by
  rw [Complex.cpow_def_of_ne_zero (by simp [hn]), Real.rpow_def_of_nonneg (Nat.cast_nonneg n)]
  simp [hn]
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
this : ↑n ^ ↑σ' = ↑(↑n ^ σ')
⊢ f n / ↑n ^ ↑σ' * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    (f n * (cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ'))) • ψ y
Theorem: first_fourier_aux2
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
this : ↑n ^ ↑σ' = ↑(↑n ^ σ')
⊢ f n / ↑n ^ ↑σ' * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y =
    (f n * (cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ'))) • ψ y
Tactic:
simp [Real.fourierChar, expMapCircle, smul_eq_mul, mul_assoc, this]
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
this : ↑n ^ ↑σ' = ↑(↑n ^ σ')
⊢ f n / ↑(↑n ^ σ') * (cexp (-(2 * (↑π * (↑y * ((↑π)⁻¹ * (2⁻¹ * (↑(↑n / x).log * I))))))) * ψ y) =
    f n * (cexp (-(2 * (↑π * (↑y * ((↑π)⁻¹ * (2⁻¹ * (↑(↑n / x).log * I))))))) / ↑(↑n ^ σ') * ψ y)
Theorem: first_fourier_aux2
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
this : ↑n ^ ↑σ' = ↑(↑n ^ σ')
⊢ f n / ↑(↑n ^ σ') * (cexp (-(2 * (↑π * (↑y * ((↑π)⁻¹ * (2⁻¹ * (↑(↑n / x).log * I))))))) * ψ y) =
    f n * (cexp (-(2 * (↑π * (↑y * ((↑π)⁻¹ * (2⁻¹ * (↑(↑n / x).log * I))))))) / ↑(↑n ^ σ') * ψ y)
Tactic:
ring
Proof state after:
no goals
Theorem: first_fourier_aux2
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ ↑n ^ ↑σ' = ↑(↑n ^ σ')
Tactic:
rw [Complex.cpow_def_of_ne_zero (by simp [hn]), Real.rpow_def_of_nonneg (Nat.cast_nonneg n)]
Proof state after:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ cexp ((↑n).log * ↑σ') = ↑(if ↑n = 0 then if σ' = 0 then 1 else 0 else rexp ((↑n).log * σ'))
Theorem: first_fourier_aux2
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ cexp ((↑n).log * ↑σ') = ↑(if ↑n = 0 then if σ' = 0 then 1 else 0 else rexp ((↑n).log * σ'))
Tactic:
simp [hn]
Proof state after:
no goals
Theorem: first_fourier_aux2
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ ↑n ≠ 0
Tactic:
simp [hn]
Proof state after:
no goals
Theorem: first_fourier_aux2
Proof state before:
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ (f n * (cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ'))) • ψ y =
    (f n * (↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I))) • ψ y
Tactic:
congr 2
Proof state after:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)
Theorem: first_fourier_aux2
Proof state before:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)
Tactic:
have l1 : 0 < (n : ℝ) := by simpa using Nat.pos_iff_ne_zero.mpr hn
Proof state after:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)
Theorem: first_fourier_aux2
Proof state before:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)
Tactic:
have l2 : (x : ℂ) ≠ 0 := by simp [hx.ne.symm]
Proof state after:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)
Theorem: first_fourier_aux2
Proof state before:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)
Tactic:
have l3 : (n : ℂ) ≠ 0 := by simp [hn]
Proof state after:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)
Theorem: first_fourier_aux2
Proof state before:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(↑n ^ σ') = ↑x ^ (↑y * I) / ↑n ^ (↑σ' + ↑y * I)
Tactic:
rw [Real.rpow_def_of_pos l1, Complex.cpow_def_of_ne_zero l2, Complex.cpow_def_of_ne_zero l3]
Proof state after:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(rexp ((↑n).log * σ')) =
    cexp ((↑x).log * (↑y * I)) / cexp ((↑n).log * (↑σ' + ↑y * I))
Theorem: first_fourier_aux2
Proof state before:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / ↑(rexp ((↑n).log * σ')) =
    cexp ((↑x).log * (↑y * I)) / cexp ((↑n).log * (↑σ' + ↑y * I))
Tactic:
push_cast
Proof state after:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / cexp ((↑n).log * ↑σ') =
    cexp ((↑x).log * (↑y * I)) / cexp ((↑n).log * (↑σ' + ↑y * I))
Theorem: first_fourier_aux2
Proof state before:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I) / cexp ((↑n).log * ↑σ') =
    cexp ((↑x).log * (↑y * I)) / cexp ((↑n).log * (↑σ' + ↑y * I))
Tactic:
simp_rw [← Complex.exp_sub]
Proof state after:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I - (↑n).log * ↑σ') =
    cexp ((↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I))
Theorem: first_fourier_aux2
Proof state before:
case e_a.e_a
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ cexp (2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I - (↑n).log * ↑σ') =
    cexp ((↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I))
Tactic:
congr 1
Proof state after:
case e_a.e_a.e_z
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
l1 : 0 < ↑n
l2 : ↑x ≠ 0
l3 : ↑n ≠ 0
⊢ 2 * ↑π * -(↑y * (1 / (2 * ↑π) * ↑(↑n / x).log)) * I - (↑n).log * ↑σ' = (↑x).log * (↑y * I) - (↑n).log * (↑σ' + ↑y * I)