internlm/Lean-Github huggingface dataset:
Theorem: Smooth1LeOne
Proof state before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ 0 ≤ Ψ ((x / y) ^ (1 / ε)) / (ε * y)
Tactic:
apply mul_nonneg
Proof state after:
case neg.ha
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ 0 ≤ Ψ ((x / y) ^ (1 / ε))

case neg.hb
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ 0 ≤ (ε * y)⁻¹
Theorem: Smooth1LeOne
Proof state before:
case neg.ha
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ 0 ≤ Ψ ((x / y) ^ (1 / ε))
Tactic:
apply Ψnonneg
Proof state after:
case neg.ha.a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ (x / y) ^ (1 / ε) > 0
Theorem: Smooth1LeOne
Proof state before:
case neg.ha.a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ (x / y) ^ (1 / ε) > 0
Tactic:
exact rpow_pos_of_pos (div_pos xpos <| mem_Ioi.mp hy) _
Proof state after:
no goals
Theorem: Smooth1LeOne
Proof state before:
case neg.hb
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
Ψnonneg : ∀ x > 0, 0 ≤ Ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
xpos : 0 < x
this : ∫ (y : ℝ) in Ioi 0, Ψ ((x / y) ^ (1 / ε)) / ε / y = 1
y : ℝ
hy : y ∈ Ioi 0
h : ¬y ≤ 1
⊢ 0 ≤ (ε * y)⁻¹
Tactic:
apply inv_nonneg.mpr <| mul_nonneg εpos.le (mem_Ioi.mp hy).le
Proof state after:
no goals
Theorem: MellinOfSmooth1a
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let f' : ℝ → ℂ := fun x ↦ DeltaSpike Ψ ε x
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Theorem: MellinOfSmooth1a
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let f : ℝ → ℂ := fun x ↦ DeltaSpike Ψ ε x / x
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Theorem: MellinOfSmooth1a
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let g : ℝ → ℂ := fun x ↦ if 0 < x ∧ x ≤ 1 then 1 else 0
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Theorem: MellinOfSmooth1a
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let F : ℝ × ℝ → ℂ := Function.uncurry fun x y ↦ f y * g (x / y) * (x : ℂ) ^ (s - 1)
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Theorem: MellinOfSmooth1a
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let S := {⟨x, y⟩ : ℝ × ℝ | 0 < x  ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Theorem: MellinOfSmooth1a
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let F' : ℝ × ℝ → ℂ := piecewise S (fun ⟨x, y⟩ ↦ f y * (x : ℂ) ^ (s - 1))
   (fun _ ↦ 0)
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Theorem: MellinOfSmooth1a
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let Tx := Ioc 0 ((2 : ℝ) ^ ε)
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Theorem: MellinOfSmooth1a
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let Ty := Icc ((2 : ℝ) ^ (-ε)) ((2 : ℝ) ^ ε)
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Theorem: MellinOfSmooth1a
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
have SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0 :=
  fun z hz ↦ ⟨hz.1, lt_of_lt_of_le (by apply rpow_pos_of_pos; norm_num) hz.2.2.1⟩
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Theorem: MellinOfSmooth1a
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
have SsubT: S ⊆ Tx ×ˢ Ty := by simp_rw [Seq, inter_subset_left]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Theorem: MellinOfSmooth1a
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
have Smeas : MeasurableSet S := by
  rw [Seq]; apply MeasurableSet.inter ?_ <| measurableSet_le measurable_fst measurable_snd
  simp [measurableSet_prod, Tx, Ty]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Theorem: MellinOfSmooth1a
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
have : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s := by
  rw [mul_comm, ← MellinConvolutionTransform f' g s (by convert int_F using 1; field_simp [F, f, f'])]
  dsimp [MellinTransform]; rw [setIntegral_congr (by simp)]
  intro x hx; simp_rw [MellinConvolutionSymmetric _ _ <| mem_Ioi.mp hx]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Theorem: MellinOfSmooth1a
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
convert this using 1
Proof state after:
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 𝓜 (MellinConvolution g f') s

case h.e'_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
⊢ 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s) = 𝓜 g s * 𝓜 f' s
Theorem: MellinOfSmooth1a
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
⊢ S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
Tactic:
ext ⟨x, y⟩
Proof state after:
case h.mk
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
x y : ℝ
⊢ (x, y) ∈ S ↔ (x, y) ∈ Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}