internlm/Lean-Github huggingface dataset:
Theorem: MellinOfSmooth1a
Proof state before:
case hf
𝕂 : 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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ Integrable (fun x => ↑x ^ (s - 1)) (volume.restrict Tx)
Tactic:
apply integrableOn_Ioc_iff_integrableOn_Ioo.mpr ?_
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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ IntegrableOn (fun x => ↑x ^ (s - 1)) (Ioo 0 (2 ^ ε)) volume
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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ IntegrableOn (fun x => ↑x ^ (s - 1)) (Ioo 0 (2 ^ ε)) volume
Tactic:
apply (intervalIntegral.integrableOn_Ioo_cpow_iff (s := s - 1) (t := (2 : ℝ) ^ ε) ?_).mpr
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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ -1 < (s - 1).re

𝕂 : 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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ 0 < 2 ^ ε
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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ -1 < (s - 1).re
Tactic:
simp [hs]
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
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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ 0 < 2 ^ ε
Tactic:
apply rpow_pos_of_pos (by norm_num)
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
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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ 0 < 2
Tactic:
norm_num
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
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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ ContinuousOn (fun x => ↑(DeltaSpike Ψ ε x)) (Icc (2 ^ (-ε)) (2 ^ ε))
Tactic:
exact (DeltaSpikeOfRealContinuous εpos diffΨ).continuousOn
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
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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ ContinuousOn (fun x => ↑x) (Icc (2 ^ (-ε)) (2 ^ ε))
Tactic:
exact continuous_ofReal.continuousOn
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
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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ ∀ x ∈ Icc (2 ^ (-ε)) (2 ^ ε), ↑x ≠ 0
Tactic:
intro x 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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
⊢ ↑x ≠ 0
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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
⊢ ↑x ≠ 0
Tactic:
simp only [mem_Icc] at 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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
⊢ ↑x ≠ 0
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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
⊢ ↑x ≠ 0
Tactic:
simp only [ofReal_ne_zero]
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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
⊢ x ≠ 0
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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
⊢ x ≠ 0
Tactic:
linarith [(by apply rpow_pos_of_pos (by norm_num) : (0 : ℝ) < 2 ^ (-ε))]
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
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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
⊢ 0 < 2 ^ (-ε)
Tactic:
apply rpow_pos_of_pos (by norm_num)
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
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
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
⊢ 0 < 2
Tactic:
norm_num
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
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
⊢ 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
Tactic:
rw [mul_comm, ← MellinConvolutionTransform f' g s (by convert int_F using 1; field_simp [F, f, f'])]
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
⊢ 𝓜 (MellinConvolution g f') s = 𝓜 (MellinConvolution f' g) 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
⊢ 𝓜 (MellinConvolution g f') s = 𝓜 (MellinConvolution f' g) s
Tactic:
dsimp [MellinTransform]
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
⊢ ∫ (x : ℝ) in Ioi 0, MellinConvolution g f' x * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, MellinConvolution f' g x * ↑x ^ (s - 1)
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
⊢ ∫ (x : ℝ) in Ioi 0, MellinConvolution g f' x * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, MellinConvolution f' g x * ↑x ^ (s - 1)
Tactic:
rw [setIntegral_congr (by simp)]
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
⊢ EqOn (fun x => MellinConvolution g f' x * ↑x ^ (s - 1)) (fun x => MellinConvolution f' g x * ↑x ^ (s - 1)) (Ioi 0)