Carlson's Dirichlet average with real positive parameters #
This file provides the probability-theoretic form of Carlson's average. Its parameters are
strictly positive real numbers and integration is against dirichletMeasure.
noncomputable def
DirichletTransform.realCarlsonDirichletAverage
{ι : Type u_1}
[Fintype ι]
(b : ι → ℝ)
(z : ι → ℂ)
(f : ℂ → ℂ)
:
Carlson's probability average for positive real Dirichlet parameters.
Equations
- DirichletTransform.realCarlsonDirichletAverage b z f = ∫ (u : ι → ℝ), f (DirichletTransform.carlsonAffineForm z u) ∂ProbabilityTheory.dirichletMeasure b
Instances For
theorem
DirichletTransform.realCarlsonDirichletAverage_eq_integral
{ι : Type u_1}
[Fintype ι]
[Nonempty ι]
{b : ι → ℝ}
(hb : b ∈ ProbabilityTheory.mvRealBetaDomain)
(z : ι → ℂ)
(f : ℂ → ℂ)
:
realCarlsonDirichletAverage b z f = ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, ↑(ProbabilityTheory.dirichletPdfReal b u) * f (carlsonAffineForm z u) ∂MeasureTheory.Measure.stdSimplexMeasure
The probability-theoretic Carlson average has the expected density representation.