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 (ℝ × ℝ)) : MeasureTheory.charFun (MeasureTheory.Measure.map (fun (ω : Ω) => WithLp.toLp 2 (X ω, Y ω)) P) ξ = Complex.exp ((↑ξ.fst * ∫ (x : Ω), ↑(X x) ∂P + ↑ξ.snd * ∫ (x : Ω), ↑(Y x) ∂P) * Complex.I - (↑ξ.fst ^ 2 * ↑(variance X P) + 2 * ↑ξ.fst * ↑ξ.snd * ↑(covariance X Y P) + ↑ξ.snd ^ 2 * ↑(variance Y P)) / 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