theorem
ProbabilityTheory.HasGaussianLaw.charFun_toLp_pi
{ι : Type u_1}
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
[Fintype ι]
{X : ι → Ω → ℝ}
(hX : HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P)
(ξ : EuclideanSpace ℝ ι)
:
MeasureTheory.charFun (MeasureTheory.Measure.map (fun (ω : Ω) => WithLp.toLp 2 fun (x : ι) => X x ω) P) ξ = Complex.exp
(∑ i : ι, (↑(ξ.ofLp i) * ∫ (x : Ω), ↑(X i x) ∂P) * Complex.I - ∑ i : ι, ∑ j : ι, ↑(ξ.ofLp i) * ↑(ξ.ofLp j) * (↑(covariance (X i) (X j) P) / 2))
theorem
ProbabilityTheory.HasGaussianLaw.charFun_toLp_prodMk
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X Y : Ω → ℝ}
(hXY : HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P)
(ξ : WithLp 2 (ℝ × ℝ))
:
theorem
ProbabilityTheory.IndepFun.hasLaw_sub_of_gaussian
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X Y : Ω → ℝ}
{μX μY : ℝ}
{vX vY : NNReal}
(hX : HasLaw X (gaussianReal μX vX) P)
(hY : HasLaw Y (gaussianReal μY vY) P)
(h1 : IndepFun X (Y - X) P)
(h2 : vX ≤ vY)
:
HasLaw (Y - X) (gaussianReal (μY - μX) (vY - vX)) P
theorem
ProbabilityTheory.IndepFun.hasLaw_gaussianReal_of_add
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X Y : Ω → ℝ}
{μX μY : ℝ}
{vX vY : NNReal}
(hX : HasLaw X (gaussianReal μX vX) P)
(hY : HasLaw (X + Y) (gaussianReal μY vY) P)
(h : IndepFun X Y P)
:
HasLaw Y (gaussianReal (μY - μX) (vY - vX)) P
theorem
ProbabilityTheory.IndepFun.hasGaussianLaw_of_add_real
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X Y : Ω → ℝ}
(hX : HasGaussianLaw X P)
(hY : HasGaussianLaw (X + Y) P)
(h : IndepFun X Y P)
:
HasGaussianLaw Y P