Theorem: MellinConvolutionSymmetric (PrimeNumberTheoremAnd/MellinCalculus.lean)

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
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

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 := ?_
  _ = _ := ?_
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

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]
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

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]
State after:
no goals

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
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✝

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]
State after:
no goals