internlm/Lean-Github huggingface dataset:
Theorem: MellinOfSmooth1b
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
this : ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖↑ε * s‖)
⊢ ‖1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖ε * ‖s‖ ^ 2‖)
Tactic:
convert mul_le_mul_of_nonneg_left (a := 1 / ‖s‖) this ?_ using 1
Proof state after:
case h.e'_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
this : ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖↑ε * s‖)
⊢ ‖1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ = 1 / ‖s‖ * ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖

case h.e'_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
this : ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖↑ε * s‖)
⊢ c * (1 / ‖ε * ‖s‖ ^ 2‖) = 1 / ‖s‖ * (c * (1 / ‖↑ε * s‖))

case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
this : ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖↑ε * s‖)
⊢ 0 ≤ 1 / ‖s‖
Theorem: MellinOfSmooth1b
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
⊢ ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖↑ε * s‖)
Tactic:
refine hc (ε * s) ?_
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
⊢ ε * σ₁ ≤ (↑ε * s).re ∧ (↑ε * s).re ≤ ε * σ₂
Theorem: MellinOfSmooth1b
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
⊢ ε * σ₁ ≤ (↑ε * s).re ∧ (↑ε * s).re ≤ ε * σ₂
Tactic:
simp only [mul_re, ofReal_re, ofReal_im, zero_mul, sub_zero]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
⊢ ε * σ₁ ≤ ε * s.re ∧ ε * s.re ≤ ε * σ₂
Theorem: MellinOfSmooth1b
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
⊢ ε * σ₁ ≤ ε * s.re ∧ ε * s.re ≤ ε * σ₂
Tactic:
exact ⟨(mul_le_mul_left εpos).mpr hs.1, (mul_le_mul_left εpos).mpr hs.2⟩
Proof state after:
no goals
Theorem: MellinOfSmooth1b
Proof state before:
case h.e'_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
this : ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖↑ε * s‖)
⊢ ‖1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ = 1 / ‖s‖ * ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖
Tactic:
simp
Proof state after:
no goals
Theorem: MellinOfSmooth1b
Proof state before:
case h.e'_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
this : ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖↑ε * s‖)
⊢ c * (1 / ‖ε * ‖s‖ ^ 2‖) = 1 / ‖s‖ * (c * (1 / ‖↑ε * s‖))
Tactic:
simp only [Complex.norm_eq_abs, norm_mul, Real.norm_eq_abs, norm_pow, Complex.abs_abs, one_div,
mul_inv_rev, abs_ofReal]
Proof state after:
case h.e'_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
this : ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖↑ε * s‖)
⊢ c * ((Complex.abs s ^ 2)⁻¹ * |ε|⁻¹) = (Complex.abs s)⁻¹ * (c * ((Complex.abs s)⁻¹ * |ε|⁻¹))
Theorem: MellinOfSmooth1b
Proof state before:
case h.e'_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
this : ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖↑ε * s‖)
⊢ c * ((Complex.abs s ^ 2)⁻¹ * |ε|⁻¹) = (Complex.abs s)⁻¹ * (c * ((Complex.abs s)⁻¹ * |ε|⁻¹))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: MellinOfSmooth1b
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
this : ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖↑ε * s‖)
⊢ 0 ≤ 1 / ‖s‖
Tactic:
exact div_nonneg (by norm_num) (norm_nonneg s)
Proof state after:
no goals
Theorem: MellinOfSmooth1b
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
this : ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖↑ε * s‖)
⊢ 0 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: MellinOfSmooth1c
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ (fun ε => 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) 1 - 1) =O[𝓝[>] 0] id
Tactic:
have h := MellinOfDeltaSpikeAt1_asymp diffΨ suppΨ mass_one
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
h : (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) =O[𝓝[>] 0] id
⊢ (fun ε => 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) 1 - 1) =O[𝓝[>] 0] id
Theorem: MellinOfSmooth1c
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
h : (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) =O[𝓝[>] 0] id
⊢ (fun ε => 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) 1 - 1) =O[𝓝[>] 0] id
Tactic:
rw [Asymptotics.isBigO_iff] at h ⊢
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
h : ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
⊢ ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x_1 => ↑(Smooth1 Ψ x x_1)) 1 - 1‖ ≤ c * ‖id x‖
Theorem: MellinOfSmooth1c
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
h : ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
⊢ ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x_1 => ↑(Smooth1 Ψ x x_1)) 1 - 1‖ ≤ c * ‖id x‖
Tactic:
obtain ⟨c, hc⟩ := h
Proof state after:
case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
⊢ ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x_1 => ↑(Smooth1 Ψ x x_1)) 1 - 1‖ ≤ c * ‖id x‖
Theorem: MellinOfSmooth1c
Proof state before:
case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
⊢ ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x_1 => ↑(Smooth1 Ψ x x_1)) 1 - 1‖ ≤ c * ‖id x‖
Tactic:
use c
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x_1 => ↑(Smooth1 Ψ x x_1)) 1 - 1‖ ≤ c * ‖id x‖
Theorem: MellinOfSmooth1c
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x_1 => ↑(Smooth1 Ψ x x_1)) 1 - 1‖ ≤ c * ‖id x‖
Tactic:
filter_upwards [hc, Ioo_mem_nhdsWithin_Ioi' (by linarith : (0 : ℝ) < 1)] with ε hε hε'
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
ε : ℝ
hε : ‖𝓜 (fun x => ↑(Ψ x)) ↑ε - 1‖ ≤ c * ‖id ε‖
hε' : ε ∈ Ioo 0 1
⊢ ‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) 1 - 1‖ ≤ c * ‖id ε‖
Theorem: MellinOfSmooth1c
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
ε : ℝ
hε : ‖𝓜 (fun x => ↑(Ψ x)) ↑ε - 1‖ ≤ c * ‖id ε‖
hε' : ε ∈ Ioo 0 1
⊢ ‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) 1 - 1‖ ≤ c * ‖id ε‖
Tactic:
simp_rw [MellinOfSmooth1a Ψ diffΨ suppΨ hε'.1 (s := 1) (by norm_num), mul_one]
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
ε : ℝ
hε : ‖𝓜 (fun x => ↑(Ψ x)) ↑ε - 1‖ ≤ c * ‖id ε‖
hε' : ε ∈ Ioo 0 1
⊢ ‖1 / 1 * 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1‖ ≤ c * ‖id ε‖
Theorem: MellinOfSmooth1c
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
ε : ℝ
hε : ‖𝓜 (fun x => ↑(Ψ x)) ↑ε - 1‖ ≤ c * ‖id ε‖
hε' : ε ∈ Ioo 0 1
⊢ ‖1 / 1 * 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1‖ ≤ c * ‖id ε‖
Tactic:
simpa using hε
Proof state after:
no goals
Theorem: MellinOfSmooth1c
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
⊢ 0 < 1
Tactic:
linarith
Proof state after:
no goals
Theorem: MellinOfSmooth1c
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ
hc : ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
ε : ℝ
hε : ‖𝓜 (fun x => ↑(Ψ x)) ↑ε - 1‖ ≤ c * ‖id ε‖
hε' : ε ∈ Ioo 0 1
⊢ 0 < re 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: ℤθ.my_add_assoc
Proof state before:
a b c : ℤθ
⊢ add (add a b) c = add a (add b c)
Tactic:
cases a
Proof state after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ add (add { f := f✝, g := g✝, h := h✝ } b) c = add { f := f✝, g := g✝, h := h✝ } (add b c)
Theorem: ℤθ.my_add_assoc
Proof state before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ add (add { f := f✝, g := g✝, h := h✝ } b) c = add { f := f✝, g := g✝, h := h✝ } (add b c)
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ add (add { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ }) c =
    add { f := f✝¹, g := g✝¹, h := h✝¹ } (add { f := f✝, g := g✝, h := h✝ } c)
Theorem: ℤθ.my_add_assoc
Proof state before:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ add (add { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ }) c =
    add { f := f✝¹, g := g✝¹, h := h✝¹ } (add { f := f✝, g := g✝, h := h✝ } c)
Tactic:
cases c
Proof state after:
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ add (add { f := f✝², g := g✝², h := h✝² } { f := f✝¹, g := g✝¹, h := h✝¹ }) { f := f✝, g := g✝, h := h✝ } =
    add { f := f✝², g := g✝², h := h✝² } (add { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ })
Theorem: ℤθ.my_add_assoc
Proof state before:
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ add (add { f := f✝², g := g✝², h := h✝² } { f := f✝¹, g := g✝¹, h := h✝¹ }) { f := f✝, g := g✝, h := h✝ } =
    add { f := f✝², g := g✝², h := h✝² } (add { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ })
Tactic:
simp only [add, add_assoc]
Proof state after:
no goals
Theorem: ℤθ.my_zero_add
Proof state before:
a b c : ℤθ
⊢ add zero a = a
Tactic:
cases' a with x y
Proof state after:
case mk
b c : ℤθ
x y h✝ : ℤ
⊢ add zero { f := x, g := y, h := h✝ } = { f := x, g := y, h := h✝ }
Theorem: ℤθ.my_zero_add
Proof state before:
case mk
b c : ℤθ
x y h✝ : ℤ
⊢ add zero { f := x, g := y, h := h✝ } = { f := x, g := y, h := h✝ }
Tactic:
simp only [add, zero, zero_add]
Proof state after:
no goals
Theorem: ℤθ.my_add_zero
Proof state before:
a b c : ℤθ
⊢ add a zero = a
Tactic:
cases' a with x y
Proof state after:
case mk
b c : ℤθ
x y h✝ : ℤ
⊢ add { f := x, g := y, h := h✝ } zero = { f := x, g := y, h := h✝ }
Theorem: ℤθ.my_add_zero
Proof state before:
case mk
b c : ℤθ
x y h✝ : ℤ
⊢ add { f := x, g := y, h := h✝ } zero = { f := x, g := y, h := h✝ }
Tactic:
simp only [add, zero, add_zero]
Proof state after:
no goals
Theorem: ℤθ.my_add_left_neg
Proof state before:
a b c : ℤθ
⊢ add (neg a) a = zero
Tactic:
cases a
Proof state after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ add (neg { f := f✝, g := g✝, h := h✝ }) { f := f✝, g := g✝, h := h✝ } = zero
Theorem: ℤθ.my_add_left_neg
Proof state before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ add (neg { f := f✝, g := g✝, h := h✝ }) { f := f✝, g := g✝, h := h✝ } = zero
Tactic:
simp only [neg, add]
Proof state after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ { f := -f✝ + f✝, g := -g✝ + g✝, h := -h✝ + h✝ } = zero
Theorem: ℤθ.my_add_left_neg
Proof state before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ { f := -f✝ + f✝, g := -g✝ + g✝, h := -h✝ + h✝ } = zero
Tactic:
simp only [add_left_neg]
Proof state after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ { f := 0, g := 0, h := 0 } = zero
Theorem: ℤθ.my_add_left_neg
Proof state before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ { f := 0, g := 0, h := 0 } = zero
Tactic:
tauto
Proof state after:
no goals
Theorem: ℤθ.my_add_comm
Proof state before:
a b c : ℤθ
⊢ add a b = add b a
Tactic:
cases a
Proof state after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ add { f := f✝, g := g✝, h := h✝ } b = add b { f := f✝, g := g✝, h := h✝ }
Theorem: ℤθ.my_add_comm
Proof state before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ add { f := f✝, g := g✝, h := h✝ } b = add b { f := f✝, g := g✝, h := h✝ }
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ add { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ } =
    add { f := f✝, g := g✝, h := h✝ } { f := f✝¹, g := g✝¹, h := h✝¹ }
Theorem: ℤθ.my_add_comm
Proof state before:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ add { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ } =
    add { f := f✝, g := g✝, h := h✝ } { f := f✝¹, g := g✝¹, h := h✝¹ }
Tactic:
simp only [add, add_comm]
Proof state after:
no goals
Theorem: ℤθ.my_mul_assoc
Proof state before:
a b c : ℤθ
⊢ mul (mul a b) c = mul a (mul b c)
Tactic:
cases a
Proof state after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul (mul { f := f✝, g := g✝, h := h✝ } b) c = mul { f := f✝, g := g✝, h := h✝ } (mul b c)
Theorem: ℤθ.my_mul_assoc
Proof state before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul (mul { f := f✝, g := g✝, h := h✝ } b) c = mul { f := f✝, g := g✝, h := h✝ } (mul b c)
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul (mul { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ }) c =
    mul { f := f✝¹, g := g✝¹, h := h✝¹ } (mul { f := f✝, g := g✝, h := h✝ } c)
Theorem: ℤθ.my_mul_assoc
Proof state before:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul (mul { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ }) c =
    mul { f := f✝¹, g := g✝¹, h := h✝¹ } (mul { f := f✝, g := g✝, h := h✝ } c)
Tactic:
cases c
Proof state after:
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul (mul { f := f✝², g := g✝², h := h✝² } { f := f✝¹, g := g✝¹, h := h✝¹ }) { f := f✝, g := g✝, h := h✝ } =
    mul { f := f✝², g := g✝², h := h✝² } (mul { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ })
Theorem: ℤθ.my_mul_assoc
Proof state before:
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ {
      f :=
        (f✝² * f✝¹ + 6 * h✝² * h✝¹ - 2 * g✝² * h✝¹ - 2 * h✝² * g✝¹) * f✝ +
              6 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * h✝ -
            2 * (f✝² * g✝¹ + g✝² * f✝¹ + 16 * h✝² * h✝¹ - 6 * g✝² * h✝¹ - 6 * h✝² * g✝¹) * h✝ -
          2 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * g✝,
      g :=
        (f✝² * f✝¹ + 6 * h✝² * h✝¹ - 2 * g✝² * h✝¹ - 2 * h✝² * g✝¹) * g✝ +
                (f✝² * g✝¹ + g✝² * f✝¹ + 16 * h✝² * h✝¹ - 6 * g✝² * h✝¹ - 6 * h✝² * g✝¹) * f✝ +
              16 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * h✝ -
            6 * (f✝² * g✝¹ + g✝² * f✝¹ + 16 * h✝² * h✝¹ - 6 * g✝² * h✝¹ - 6 * h✝² * g✝¹) * h✝ -
          6 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * g✝,
      h :=
        (f✝² * f✝¹ + 6 * h✝² * h✝¹ - 2 * g✝² * h✝¹ - 2 * h✝² * g✝¹) * h✝ +
                  (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * f✝ +
                (f✝² * g✝¹ + g✝² * f✝¹ + 16 * h✝² * h✝¹ - 6 * g✝² * h✝¹ - 6 * h✝² * g✝¹) * g✝ +
              3 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * h✝ -
            3 * (f✝² * g✝¹ + g✝² * f✝¹ + 16 * h✝² * h✝¹ - 6 * g✝² * h✝¹ - 6 * h✝² * g✝¹) * h✝ -
          3 * (f✝² * h✝¹ + h✝² * f✝¹ + g✝² * g✝¹ + 3 * h✝² * h✝¹ - 3 * g✝² * h✝¹ - 3 * h✝² * g✝¹) * g✝ } =
    {
      f :=
        f✝² * (f✝¹ * f✝ + 6 * h✝¹ * h✝ - 2 * g✝¹ * h✝ - 2 * h✝¹ * g✝) +
              6 * h✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
            2 * g✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
          2 * h✝² * (f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝),
      g :=
        f✝² * (f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝) +
                g✝² * (f✝¹ * f✝ + 6 * h✝¹ * h✝ - 2 * g✝¹ * h✝ - 2 * h✝¹ * g✝) +
              16 * h✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
            6 * g✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
          6 * h✝² * (f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝),
      h :=
        f✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) +
                  h✝² * (f✝¹ * f✝ + 6 * h✝¹ * h✝ - 2 * g✝¹ * h✝ - 2 * h✝¹ * g✝) +
                g✝² * (f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝) +
              3 * h✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
            3 * g✝² * (f✝¹ * h✝ + h✝¹ * f✝ + g✝¹ * g✝ + 3 * h✝¹ * h✝ - 3 * g✝¹ * h✝ - 3 * h✝¹ * g✝) -
          3 * h✝² * (f✝¹ * g✝ + g✝¹ * f✝ + 16 * h✝¹ * h✝ - 6 * g✝¹ * h✝ - 6 * h✝¹ * g✝) }
Tactic:
ring
Proof state after:
no goals
Theorem: ℤθ.my_zero_mul
Proof state before:
a b c : ℤθ
⊢ mul zero a = zero
Tactic:
cases a
Proof state after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul zero { f := f✝, g := g✝, h := h✝ } = zero
Theorem: ℤθ.my_zero_mul
Proof state before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul zero { f := f✝, g := g✝, h := h✝ } = zero
Tactic:
simp [mul, zero]
Proof state after:
no goals
Theorem: ℤθ.my_mul_zero
Proof state before:
a b c : ℤθ
⊢ mul a zero = zero
Tactic:
cases a
Proof state after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝, g := g✝, h := h✝ } zero = zero
Theorem: ℤθ.my_mul_zero
Proof state before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝, g := g✝, h := h✝ } zero = zero
Tactic:
simp [mul, zero]
Proof state after:
no goals
Theorem: ℤθ.my_one_mul
Proof state before:
a b c : ℤθ
⊢ mul one a = a
Tactic:
cases a
Proof state after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul one { f := f✝, g := g✝, h := h✝ } = { f := f✝, g := g✝, h := h✝ }
Theorem: ℤθ.my_one_mul
Proof state before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul one { f := f✝, g := g✝, h := h✝ } = { f := f✝, g := g✝, h := h✝ }
Tactic:
simp [mul, one]
Proof state after:
no goals
Theorem: ℤθ.my_mul_one
Proof state before:
a b c : ℤθ
⊢ mul a one = a
Tactic:
cases a
Proof state after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝, g := g✝, h := h✝ } one = { f := f✝, g := g✝, h := h✝ }
Theorem: ℤθ.my_mul_one
Proof state before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝, g := g✝, h := h✝ } one = { f := f✝, g := g✝, h := h✝ }
Tactic:
simp [mul, one]
Proof state after:
no goals
Theorem: ℤθ.my_left_distrib
Proof state before:
a b c : ℤθ
⊢ mul a (add b c) = add (mul a b) (mul a c)
Tactic:
cases a
Proof state after:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝, g := g✝, h := h✝ } (add b c) =
    add (mul { f := f✝, g := g✝, h := h✝ } b) (mul { f := f✝, g := g✝, h := h✝ } c)
Theorem: ℤθ.my_left_distrib
Proof state before:
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝, g := g✝, h := h✝ } (add b c) =
    add (mul { f := f✝, g := g✝, h := h✝ } b) (mul { f := f✝, g := g✝, h := h✝ } c)
Tactic:
cases b
Proof state after:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝¹, g := g✝¹, h := h✝¹ } (add { f := f✝, g := g✝, h := h✝ } c) =
    add (mul { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ }) (mul { f := f✝¹, g := g✝¹, h := h✝¹ } c)
Theorem: ℤθ.my_left_distrib
Proof state before:
case mk.mk
c : ℤθ
f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝¹, g := g✝¹, h := h✝¹ } (add { f := f✝, g := g✝, h := h✝ } c) =
    add (mul { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ }) (mul { f := f✝¹, g := g✝¹, h := h✝¹ } c)
Tactic:
cases c
Proof state after:
case mk.mk.mk
f✝² g✝² h✝² f✝¹ g✝¹ h✝¹ f✝ g✝ h✝ : ℤ
⊢ mul { f := f✝², g := g✝², h := h✝² } (add { f := f✝¹, g := g✝¹, h := h✝¹ } { f := f✝, g := g✝, h := h✝ }) =
    add (mul { f := f✝², g := g✝², h := h✝² } { f := f✝¹, g := g✝¹, h := h✝¹ })
      (mul { f := f✝², g := g✝², h := h✝² } { f := f✝, g := g✝, h := h✝ })