Unit shifts of Dirichlet parameters and their integral identities

noncomputable def DirichletTransform.addDirichletUnit {ι : Type u_1} (b : ι → ℂ) (i : ι) : ι → ℂ

The Dirichlet parameter vector obtained by increasing coordinate i by one.

Equations

• DirichletTransform.addDirichletUnit b i = Function.update b i (b i + 1)

@[simp]

theorem DirichletTransform.sum_addDirichletUnit {ι : Type u_1} [Fintype ι] (b : ι → ℂ) (i : ι) : ∑ j : ι, addDirichletUnit b i j = ∑ j : ι, b j + 1

A unit parameter shift increases the total parameter by one.

theorem DirichletTransform.addDirichletUnit_mem_mvBetaConvergent {ι : Type u_1} {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (i : ι) : addDirichletUnit b i ∈ Complex.mvBetaConvergent

A positive unit shift preserves the native convergence region.

theorem DirichletTransform.mul_regDirichletDensity_addDirichletUnit {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (i : ι) (u : ι → ℝ) : b i * ProbabilityTheory.regDirichletDensity (addDirichletUnit b i) u = ↑(u i) * ProbabilityTheory.regDirichletDensity b u

Increasing one Dirichlet parameter by one multiplies the regularized density by the corresponding simplex coordinate, up to the factor b i.

theorem DirichletTransform.mul_regDirichletIntegral_addDirichletUnit {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (i : ι) (f : (ι → ℝ) → ℂ) : b i * ProbabilityTheory.regDirichletIntegral (addDirichletUnit b i) f = ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => ↑(u i) * f u

Integral form of the regularized one-coordinate parameter-shift identity.

theorem DirichletTransform.mul_regDirichletDensity_update_add_one {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (i : ι) (u : ι → ℝ) : b i * ProbabilityTheory.regDirichletDensity (Function.update b i (b i + 1)) u = ↑(u i) * ProbabilityTheory.regDirichletDensity b u

Compatibility spelling for the density-shift lemma used by the earlier R-function development.

theorem DirichletTransform.mul_regDirichletIntegral_update_add_one {ι : Type u_1} [Fintype ι] {b : ι → ℂ} (hb : b ∈ Complex.mvBetaConvergent) (i : ι) (f : (ι → ℝ) → ℂ) : b i * ProbabilityTheory.regDirichletIntegral (Function.update b i (b i + 1)) f = ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => ↑(u i) * f u

Compatibility spelling for the integral parameter-shift lemma.