Moment-generating functions of sums of coordinates under a product measure

A statistic of the form x ↦ ∑ j, f j (x j) under a finite product measure Measure.pi μ has exponential ∏ j, exp (t * f j (x j)), so Fubini's theorem turns its moment-generating function into the product of the coordinate ones. For a product of probability measures each factor is positive exactly on its exponential-integrability domain, so the domain of the sum is then the intersection of the domains of the coordinates. That step genuinely needs the coordinates to be probability measures: under the zero measure, for instance, the moment-generating function vanishes everywhere while the integrability domain is all of ℝ.

These are the facts that turn a quadratic statistic of a Gaussian vector, written in eigen-coordinates, into a product of one-dimensional moment-generating functions.

The variance of a sum of coordinates is simpler still: the coordinates are independent, so their variances add (ProbabilityTheory.variance_sum_pi). For the average of n independent copies of one square integrable statistic this gives variance Var[f] / n, and Chebyshev's inequality turns that into the weak law of large numbers with an explicit rate: the average deviates from the mean by at least t with probability at most Var[f] / (n t²).

Main results

• TauCeti.mgf_sum_pi — the moment-generating function of a sum of coordinate statistics factors over the coordinates, for every argument;
• TauCeti.integrableExpSet_sum_pi — for a product of probability measures, its exponential-integrability domain is the intersection of the coordinate domains;
• TauCeti.meas_ge_le_variance_div_card_mul_sq_pi — the weak law of large numbers in Chebyshev's form, for the average of independent copies of a square-integrable statistic.

theorem TauCeti.mgf_sum_pi {ι : Type u_1} [Fintype ι] {E : ι → Type u_2} [(i : ι) → MeasurableSpace (E i)] {μ : (i : ι) → MeasureTheory.Measure (E i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (f : (i : ι) → E i → ℝ) (t : ℝ) : ProbabilityTheory.mgf (fun (x : (i : ι) → E i) => ∑ j : ι, f j (x j)) (MeasureTheory.Measure.pi μ) t = ∏ j : ι, ProbabilityTheory.mgf (f j) (μ j) t

Under a product measure the exponential of a sum of coordinate statistics factors over the coordinates, so Fubini's theorem turns its integral into a product of one-dimensional moment-generating functions. No integrability hypothesis is needed: off the common domain both sides are zero.

theorem TauCeti.integrableExpSet_sum_pi {ι : Type u_1} [Fintype ι] {E : ι → Type u_2} [(i : ι) → MeasurableSpace (E i)] {μ : (i : ι) → MeasureTheory.Measure (E i)} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (f : (i : ι) → E i → ℝ) : ProbabilityTheory.integrableExpSet (fun (x : (i : ι) → E i) => ∑ j : ι, f j (x j)) (MeasureTheory.Measure.pi μ) = ⋂ (j : ι), ProbabilityTheory.integrableExpSet (f j) (μ j)

Under a product of probability measures, a sum of coordinate statistics has finite exponential moments of order t exactly when every coordinate does.

theorem TauCeti.meas_ge_le_variance_div_card_mul_sq_pi {ι : Type u_1} [Fintype ι] {Ω : Type u_3} [MeasurableSpace Ω] {ν : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure ν] [Nonempty ι] {f : Ω → ℝ} (hf : MeasureTheory.MemLp f 2 ν) {t : ℝ} (ht : 0 < t) : (MeasureTheory.Measure.pi fun (x : ι) => ν) {x : ι → Ω | t ≤ |(∑ j : ι, f (x j)) / ↑(Fintype.card ι) - ∫ (a : Ω), f a ∂ν|} ≤ ENNReal.ofReal (ProbabilityTheory.variance f ν / (↑(Fintype.card ι) * t ^ 2))

The weak law of large numbers, in Chebyshev's form. Under the product of |ι| copies of a probability measure ν, the average of a square-integrable statistic f over the coordinates deviates from its mean ∫ f dν by at least t with probability at most Var[f] / (|ι| t²).