internlm/Lean-Github huggingface dataset:
Theorem: MellinInversion_aux1
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℂ
s : ℂ
s_ne_zero : s ≠ 0
fDiff : DifferentiableOn ℝ f (Ioi 0)
hfs : Tendsto (fun x => f x * ↑x ^ s) (𝓝[>] 0) (𝓝 0)
hfinf : Tendsto (fun x => f x * ↑x ^ s) atTop (𝓝 0)
⊢ ∫ (x : ℝ) in Ioi 0, f x * ↑x ^ s / ↑x = -∫ (x : ℝ) in Ioi 0, deriv f x * ↑x ^ s / s
Tactic:
sorry
Proof state after:
no goals
Theorem: MellinInversion_aux2
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℂ
s : ℂ
fDiff : DifferentiableOn ℝ f (Ioi 0)
fDiff2 : DifferentiableOn ℝ (deriv f) (Ioi 0)
hfs : Tendsto (fun x => deriv f x * ↑x ^ s) (𝓝[>] 0) (𝓝 0)
hfinf : Tendsto (fun x => deriv f x * ↑x ^ s) atTop (𝓝 0)
⊢ ∫ (x : ℝ) in Ioi 0, deriv f x * ↑x ^ s = -∫ (x : ℝ) in Ioi 0, deriv (deriv f) x * ↑x ^ (s + 1) / (s + 1)
Tactic:
sorry
Proof state after:
no goals
Theorem: MellinInversion_aux3
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℂ
σ : ℝ
σ_ne_zero : σ ≠ 0
σ_ne_negOne : σ ≠ -1
fInt : IntegrableOn (fun x => f x * ↑x ^ ↑σ) (Ioi 0) volume
⊢ IntegrableOn
    (fun x =>
      match x with
      | (x, t) => f x * ↑x ^ (↑σ + ↑t * I) / ((↑σ + ↑t * I) * (↑σ + ↑t * I + 1)))
    ((Ioi 0).prod univ) volume
Tactic:
sorry
Proof state after:
no goals
Theorem: MellinInversion_aux4
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℂ
σ : ℝ
σ_ne_zero : σ ≠ 0
σ_ne_negOne : σ ≠ -1
fInt : IntegrableOn (fun x => f x * ↑x ^ ↑σ) (Ioi 0) volume
⊢ VerticalIntegral (fun s => ∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s + 1) / (s * (s + 1))) σ =
    ∫ (x : ℝ) in Ioi 0, VerticalIntegral (fun s => f x * ↑x ^ (s + 1) / (s * (s + 1))) σ
Tactic:
sorry
Proof state after:
no goals
Theorem: MellinTransform_eq
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
⊢ 𝓜 = mellin
Tactic:
unfold mellin MellinTransform
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
⊢ (fun f s => ∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s - 1)) = fun f s => ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t
Theorem: MellinTransform_eq
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
⊢ (fun f s => ∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s - 1)) = fun f s => ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t
Tactic:
simp_rw [smul_eq_mul, mul_comm]
Proof state after:
no goals
Theorem: MellinInverseTransform_eq
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
⊢ MellinInverseTransform f σ = mellinInv σ f
Tactic:
unfold mellinInv MellinInverseTransform VerticalIntegral' VerticalIntegral
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
⊢ (fun x => (1 / (2 * ↑π * I)) • I • ∫ (t : ℝ), (fun s => ↑x ^ (-s) * f s) (↑σ + ↑t * I)) = fun x =>
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)
Theorem: MellinInverseTransform_eq
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
⊢ (fun x => (1 / (2 * ↑π * I)) • I • ∫ (t : ℝ), (fun s => ↑x ^ (-s) * f s) (↑σ + ↑t * I)) = fun x =>
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)
Tactic:
beta_reduce
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
⊢ (fun x => (1 / (2 * ↑π * I)) • I • ∫ (t : ℝ), ↑x ^ (-(↑σ + ↑t * I)) * f (↑σ + ↑t * I)) = fun x =>
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)
Theorem: MellinInverseTransform_eq
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
⊢ (fun x => (1 / (2 * ↑π * I)) • I • ∫ (t : ℝ), ↑x ^ (-(↑σ + ↑t * I)) * f (↑σ + ↑t * I)) = fun x =>
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)
Tactic:
ext x
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
x : ℝ
⊢ (1 / (2 * ↑π * I)) • I • ∫ (t : ℝ), ↑x ^ (-(↑σ + ↑t * I)) * f (↑σ + ↑t * I) =
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)
Theorem: MellinInverseTransform_eq
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
x : ℝ
⊢ (1 / (2 * ↑π * I)) • I • ∫ (t : ℝ), ↑x ^ (-(↑σ + ↑t * I)) * f (↑σ + ↑t * I) =
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)
Tactic:
rw [← smul_assoc, smul_eq_mul (a' := I), div_mul]
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
x : ℝ
⊢ (1 / (2 * ↑π * I / I)) • ∫ (t : ℝ), ↑x ^ (-(↑σ + ↑t * I)) * f (↑σ + ↑t * I) =
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)
Theorem: MellinInverseTransform_eq
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
x : ℝ
⊢ (1 / (2 * ↑π * I / I)) • ∫ (t : ℝ), ↑x ^ (-(↑σ + ↑t * I)) * f (↑σ + ↑t * I) =
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)
Tactic:
simp
Proof state after:
no goals
Theorem: MellinInversion
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℝ → ℂ
x : ℝ
hx : 0 < x
hf : MellinConvergent f ↑σ
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
⊢ MellinInverseTransform (𝓜 f) σ x = f x
Tactic:
rw [MellinTransform_eq, MellinInverseTransform_eq, mellin_inversion σ f hx hf hFf hfx]
Proof state after:
no goals
Theorem: MellinConvolutionSymmetric
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → 𝕂
x : ℝ
xpos : 0 < x
⊢ MellinConvolution f g x = MellinConvolution g f x
Tactic:
unfold MellinConvolution
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → 𝕂
x : ℝ
xpos : 0 < x
⊢ ∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y = ∫ (y : ℝ) in Ioi 0, g y * f (x / y) / ↑y
Theorem: MellinConvolutionSymmetric
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → 𝕂
x : ℝ
xpos : 0 < x
⊢ ∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y = ∫ (y : ℝ) in Ioi 0, g y * f (x / y) / ↑y
Tactic:
calc
  _ = ∫ y in Ioi 0, f (y * x) * g (1 / y) / y := ?_
  _ = _ := ?_
Proof state after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → 𝕂
x : ℝ
xpos : 0 < x
⊢ ∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y = ∫ (y : ℝ) in Ioi 0, f (y * x) * g (1 / y) / ↑y

case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → 𝕂
x : ℝ
xpos : 0 < x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * x) * g (1 / y) / ↑y = ∫ (y : ℝ) in Ioi 0, g y * f (x / y) / ↑y
Theorem: MellinConvolutionSymmetric
Proof state before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → 𝕂
x : ℝ
xpos : 0 < x
⊢ ∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y = ∫ (y : ℝ) in Ioi 0, f (y * x) * g (1 / y) / ↑y
Tactic:
rw [← integral_comp_mul_right_I0i_haar (fun y ↦ f y * g (x / y)) xpos]
Proof state after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → 𝕂
x : ℝ
xpos : 0 < x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * x) * g (x / (y * x)) / ↑y = ∫ (y : ℝ) in Ioi 0, f (y * x) * g (1 / y) / ↑y
Theorem: MellinConvolutionSymmetric
Proof state before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → 𝕂
x : ℝ
xpos : 0 < x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * x) * g (x / (y * x)) / ↑y = ∫ (y : ℝ) in Ioi 0, f (y * x) * g (1 / y) / ↑y
Tactic:
simp [div_mul_cancel_right₀ <| ne_of_gt xpos]
Proof state after:
no goals
Theorem: MellinConvolutionSymmetric
Proof state before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → 𝕂
x : ℝ
xpos : 0 < x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * x) * g (1 / y) / ↑y = ∫ (y : ℝ) in Ioi 0, g y * f (x / y) / ↑y
Tactic:
convert (integral_comp_inv_I0i_haar fun y ↦ f (y * x) * g (1 / y)).symm using 3
Proof state after:
case h.e'_3.h.e'_7.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → 𝕂
x : ℝ
xpos : 0 < x
x✝ : ℝ
⊢ g x✝ * f (x / x✝) / ↑x✝ = f (1 / x✝ * x) * g (1 / (1 / x✝)) / ↑x✝
Theorem: MellinConvolutionSymmetric
Proof state before:
case h.e'_3.h.e'_7.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → 𝕂
x : ℝ
xpos : 0 < x
x✝ : ℝ
⊢ g x✝ * f (x / x✝) / ↑x✝ = f (1 / x✝ * x) * g (1 / (1 / x✝)) / ↑x✝
Tactic:
rw [one_div_one_div, mul_comm, mul_comm_div, one_mul]
Proof state after:
no goals
Theorem: MellinConvolutionTransform
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
⊢ 𝓜 (MellinConvolution f g) s = 𝓜 f s * 𝓜 g s
Tactic:
dsimp [MellinTransform, MellinConvolution]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, (∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y) * ↑x ^ (s - 1) =
    (∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
Theorem: MellinConvolutionTransform
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, (∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y) * ↑x ^ (s - 1) =
    (∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
Tactic:
set f₁ : ℝ × ℝ → ℂ := fun ⟨x, y⟩ ↦ f y * g (x / y) / (y : ℂ) * (x : ℂ) ^ (s - 1)
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioi 0, (∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y) * ↑x ^ (s - 1) =
    (∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
Theorem: MellinConvolutionTransform
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioi 0, (∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y) * ↑x ^ (s - 1) =
    (∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
Tactic:
calc
  _ = ∫ (x : ℝ) in Ioi 0, ∫ (y : ℝ) in Ioi 0, f₁ (x, y) := ?_
  _ = ∫ (y : ℝ) in Ioi 0, ∫ (x : ℝ) in Ioi 0, f₁ (x, y) := setIntegral_integral_swap _ hf
  _ = ∫ (y : ℝ) in Ioi 0, ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) := rfl
  _ = ∫ (y : ℝ) in Ioi 0, ∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) / ↑y * ↑(x * y) ^ (s - 1) * y := ?_
  _ = ∫ (y : ℝ) in Ioi 0, ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) := ?_
  _ = ∫ (y : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1) := ?_
  _ = _ := integral_mul_right _ _
<;> try (rw [setIntegral_congr (by simp)]; intro y hy; simp only [ofReal_mul])
Proof state after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ (∫ (y_1 : ℝ) in Ioi 0, f y_1 * g (y / y_1) / ↑y_1) * ↑y ^ (s - 1) = ∫ (y_1 : ℝ) in Ioi 0, f₁ (y, y_1)

case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y

case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y =
    ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))

case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) =
    f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
Theorem: MellinConvolutionTransform
Proof state before:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
⊢ ∫ (y : ℝ) (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) =
    ∫ (y : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
Tactic:
(rw [setIntegral_congr (by simp)]; intro y hy; simp only [ofReal_mul])
Proof state after:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) =
    f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
Theorem: MellinConvolutionTransform
Proof state before:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
⊢ ∫ (y : ℝ) (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) =
    ∫ (y : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
Tactic:
rw [setIntegral_congr (by simp)]
Proof state after:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
⊢ EqOn (fun y => ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)))
    (fun x => f x * ↑x ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)) (Ioi 0)
Theorem: MellinConvolutionTransform
Proof state before:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
⊢ EqOn (fun y => ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)))
    (fun x => f x * ↑x ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)) (Ioi 0)
Tactic:
intro y hy
Proof state after:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) y =
    (fun x => f x * ↑x ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)) y
Theorem: MellinConvolutionTransform
Proof state before:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) y =
    (fun x => f x * ↑x ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)) y
Tactic:
simp only [ofReal_mul]
Proof state after:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) =
    f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
Theorem: MellinConvolutionTransform
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
Proof state after:
no goals
Theorem: MellinConvolutionTransform
Proof state before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ (∫ (y_1 : ℝ) in Ioi 0, f y_1 * g (y / y_1) / ↑y_1) * ↑y ^ (s - 1) = ∫ (y_1 : ℝ) in Ioi 0, f₁ (y, y_1)
Tactic:
simp only [integral_mul_right]
Proof state after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ (∫ (y_1 : ℝ) in Ioi 0, f y_1 * g (y / y_1) / ↑y_1) * ↑y ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f a * g (y / a) / ↑a) * ↑y ^ (s - 1)
Theorem: MellinConvolutionTransform
Proof state before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ (∫ (y_1 : ℝ) in Ioi 0, f y_1 * g (y / y_1) / ↑y_1) * ↑y ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f a * g (y / a) / ↑a) * ↑y ^ (s - 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: MellinConvolutionTransform
Proof state before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y
Tactic:
simp only [integral_mul_right]
Proof state after:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) / ↑y * (↑a * ↑y) ^ (s - 1)) * ↑y
Theorem: MellinConvolutionTransform
Proof state before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) / ↑y * (↑a * ↑y) ^ (s - 1)) * ↑y
Tactic:
have := integral_comp_mul_right_Ioi (fun x ↦ f y * g (x / y) / (y : ℂ) * (x : ℂ) ^ (s - 1)) 0 hy
Proof state after:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
this :
  ∫ (x : ℝ) in Ioi 0, (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (x * y) =
    y⁻¹ • ∫ (x : ℝ) in Ioi (0 * y), (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) x
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) / ↑y * (↑a * ↑y) ^ (s - 1)) * ↑y
Theorem: MellinConvolutionTransform
Proof state before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
this :
  ∫ (x : ℝ) in Ioi 0, (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (x * y) =
    y⁻¹ • ∫ (x : ℝ) in Ioi (0 * y), (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) x
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) / ↑y * (↑a * ↑y) ^ (s - 1)) * ↑y
Tactic:
have y_ne_zeroℂ : (y : ℂ) ≠ 0 := slitPlane_ne_zero (Or.inl hy)
Proof state after:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
this :
  ∫ (x : ℝ) in Ioi 0, (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (x * y) =
    y⁻¹ • ∫ (x : ℝ) in Ioi (0 * y), (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) x
y_ne_zeroℂ : ↑y ≠ 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) / ↑y * (↑a * ↑y) ^ (s - 1)) * ↑y
Theorem: MellinConvolutionTransform
Proof state before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
this :
  ∫ (x : ℝ) in Ioi 0, (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (x * y) =
    y⁻¹ • ∫ (x : ℝ) in Ioi (0 * y), (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) x
y_ne_zeroℂ : ↑y ≠ 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) / ↑y * (↑a * ↑y) ^ (s - 1)) * ↑y
Tactic:
field_simp at this ⊢
Proof state after:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
y_ne_zeroℂ : ↑y ≠ 0
this :
  (∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) * (↑x * ↑y) ^ (s - 1) / ↑y) * ↑y =
    ∫ (x : ℝ) in Ioi 0, f y * g (x / y) * ↑x ^ (s - 1) / ↑y
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) * ↑x ^ (s - 1) / ↑y =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) * (↑a * ↑y) ^ (s - 1) / ↑y) * ↑y
Theorem: MellinConvolutionTransform
Proof state before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
y_ne_zeroℂ : ↑y ≠ 0
this :
  (∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) * (↑x * ↑y) ^ (s - 1) / ↑y) * ↑y =
    ∫ (x : ℝ) in Ioi 0, f y * g (x / y) * ↑x ^ (s - 1) / ↑y
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) * ↑x ^ (s - 1) / ↑y =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) * (↑a * ↑y) ^ (s - 1) / ↑y) * ↑y
Tactic:
rw [this]
Proof state after:
no goals