Integration by parts for regularized Dirichlet integrals

The normalized positive power x₊ ^ (a - 1) / Gamma a has derivative x₊ ^ (a - 2) / Gamma (a - 1) when 2 < re a, including at zero. Products of these functions give the Dirichlet density in a free-coordinate chart, extended by zero outside the simplex. Mathlib's integration-by-parts theorem on the ambient coordinate space then gives regDirichletIntegral_tangent_ibp without a boundary term. This result uses only the native integral theory.

noncomputable def DirichletTransform.dirichletChartDensity {ι : Type u_1} [Fintype ι] (i : ι) (b : ι → ℂ) (x : { j : ι // j ≠ i } → ℝ) : ℂ

The regularized density in a free-coordinate chart, extended by zero.

Equations

• DirichletTransform.dirichletChartDensity i b x = ∏ j : ι, DirichletTransform.positiveGammaPower (b j) (stdSimplexCoordMap i x j)

theorem DirichletTransform.prod_positiveGammaPower_eq_regDirichletDensity {ι : Type u_1} [Fintype ι] (b : ι → ℂ) (u : ι → ℝ) (hu : ∑ j : ι, u j = 1) : ∏ j : ι, positiveGammaPower (b j) (u j) = ProbabilityTheory.regDirichletDensity b u

theorem DirichletTransform.dirichletChartDensity_eq {ι : Type u_1} [Fintype ι] (i : ι) (b : ι → ℂ) (x : { j : ι // j ≠ i } → ℝ) : dirichletChartDensity i b x = ProbabilityTheory.regDirichletDensity b (stdSimplexCoordMap i x)

theorem DirichletTransform.tsupport_dirichletChartDensity_subset {ι : Type u_1} [Fintype ι] (i : ι) (b : ι → ℂ) : tsupport (dirichletChartDensity i b) ⊆ stdSimplexCoordMap i ⁻¹' Convexity.StdSimplex.coordinateSet ℝ ι

theorem DirichletTransform.dirichletChartDensity_mul_eq_indicator {ι : Type u_1} [Fintype ι] (i : ι) (b : ι → ℂ) (f : (ι → ℝ) → ℂ) : (fun (x : { j : ι // j ≠ i } → ℝ) => dirichletChartDensity i b x * f (stdSimplexCoordMap i x)) = (stdSimplexFreeCoords i).indicator fun (x : { j : ι // j ≠ i } → ℝ) => ProbabilityTheory.regDirichletDensity b (stdSimplexCoordMap i x) * f (stdSimplexCoordMap i x)

theorem DirichletTransform.integral_dirichletChartDensity_mul {ι : Type u_1} [Fintype ι] (i : ι) (b : ι → ℂ) (f : (ι → ℝ) → ℂ) : ∫ (x : { j : ι // j ≠ i } → ℝ), dirichletChartDensity i b x * f (stdSimplexCoordMap i x) = ProbabilityTheory.regDirichletIntegral b f

theorem DirichletTransform.integrable_dirichletChartDensity_mul {ι : Type u_1} [Fintype ι] (i : ι) (b : ι → ℂ) (hb : b ∈ Complex.mvBetaConvergent) {f : (ι → ℝ) → ℂ} (hf : ContinuousOn f (Convexity.StdSimplex.coordinateSet ℝ ι)) : MeasureTheory.Integrable (fun (x : { j : ι // j ≠ i } → ℝ) => dirichletChartDensity i b x * f (stdSimplexCoordMap i x)) MeasureTheory.volume

theorem DirichletTransform.dirichletChartDensity_lower {ι : Type u_1} [Fintype ι] (i k : ι) (b : ι → ℂ) (x : { j : ι // j ≠ i } → ℝ) : dirichletChartDensity i (b - Pi.single k 1) x = positiveGammaPower (b k - 1) (stdSimplexCoordMap i x k) * ∏ l ∈ Finset.univ.erase k, positiveGammaPower (b l) (stdSimplexCoordMap i x l)

theorem DirichletTransform.hasLineDerivAt_dirichletChartDensity {ι : Type u_1} [Fintype ι] (i : ι) (j : { j : ι // j ≠ i }) (b : ι → ℂ) (hb : ∀ (k : ι), 2 < (b k).re) (x : { j : ι // j ≠ i } → ℝ) : HasLineDerivAt ℝ (dirichletChartDensity i b) (dirichletChartDensity i (b - Pi.single (↑j) 1) x - dirichletChartDensity i (b - Pi.single i 1) x) x (Pi.single j 1)

theorem DirichletTransform.regDirichletIntegral_tangent_ibp {ι : Type u_1} [Fintype ι] (i : ι) (j : { j : ι // j ≠ i }) (b : ι → ℂ) (hb : ∀ (k : ι), 2 < (b k).re) {f : (ι → ℝ) → ℂ} (hf : ∀ u ∈ Convexity.StdSimplex.coordinateSet ℝ ι, DifferentiableAt ℝ f u) (hdf : ContinuousOn (fun (u : ι → ℝ) => (fderiv ℝ f u) (Pi.single (↑j) 1 - Pi.single i 1)) (Convexity.StdSimplex.coordinateSet ℝ ι)) : (ProbabilityTheory.regDirichletIntegral b fun (u : ι → ℝ) => (fderiv ℝ f u) (Pi.single (↑j) 1 - Pi.single i 1)) = ProbabilityTheory.regDirichletIntegral (b - Pi.single i 1) f - ProbabilityTheory.regDirichletIntegral (b - Pi.single (↑j) 1) f

Tangential integration by parts, initially with exponents that vanish differentiably at every boundary face. The Gamma normalization removes the usual exponent coefficients.