Source indexedlemma · leanprover/lean4:v4.32.0

MellinConvolutionSymmetric

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:293 to 324

Source documentation

Let us start with a simple property of the Mellin convolution.

Exact Lean statement

@[blueprint
  (title := "MellinConvolutionSymmetric")
  (statement := /--
  Let $f$ and $g$ be functions from $\mathbb{R}_{>0}$ to $\mathbb{R}$ or $\mathbb{C}$, for $x\neq0$,
  $$
    (f\ast g)(x)=(g\ast f)(x)
    .
  $$
  -/)
  (proof := /--
  By Definition \ref{MellinConvolution},
  $$
    (f\ast g)(x) = \int_0^\infty f(y)g(x/y)\frac{dy}{y}
  $$
  in which we change variables to $z=x/y$:
  $$
    (f\ast g)(x) = \int_0^\infty f(x/z)g(z)\frac{dz}{z}
    =(g\ast f)(x)
    .
  $$
  -/)
  (latexEnv := "lemma")]
lemma MellinConvolutionSymmetric (f g : ℝ → 𝕂) {x : ℝ} (xpos : 0 < x) :
    MellinConvolution f g x = MellinConvolution g f x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "MellinConvolutionSymmetric")  (statement := /--  Let $f$ and $g$ be functions from $\mathbb{R}_{>0}$ to $\mathbb{R}$ or $\mathbb{C}$, for $x\neq0$,  $$    (f\ast g)(x)=(g\ast f)(x)    .  $$  -/)  (proof := /--  By Definition \ref{MellinConvolution},  $$    (f\ast g)(x) = \int_0^\infty f(y)g(x/y)\frac{dy}{y}  $$  in which we change variables to $z=x/y$:  $$    (f\ast g)(x) = \int_0^\infty f(x/z)g(z)\frac{dz}{z}    =(g\ast f)(x)    .  $$  -/)  (latexEnv := "lemma")]lemma MellinConvolutionSymmetric (f g : ℝ → 𝕂) {x : ℝ} (xpos : 0 < x) :    MellinConvolution f g x = MellinConvolution g f x := by  unfold MellinConvolution  calc    _ = ∫ y in Ioi 0, f (y * x) * g (1 / y) / y := ?_    _ = _ := ?_  · rw [← integral_comp_mul_right_I0i_haar (fun y ↦ f y * g (x / y)) xpos]    simp [div_mul_cancel_right₀ <| ne_of_gt xpos]  · convert (integral_comp_inv_I0i_haar fun y ↦ f (y * x) * g (1 / y)).symm using 3    rw [one_div_one_div, mul_comm, mul_comm_div, one_mul]