theorem
ProbabilityTheory.HasGaussianLaw.charFun_toLp_pi
{ι : Type u_1}
{Ω : Type u_2}
[Fintype ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{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 : ι, (↑(ξ i) * ∫ (x : Ω), ↑(X i x) ∂P) * Complex.I - ∑ i : ι, ∑ j : ι, ↑(ξ i) * ↑(ξ 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.iIndepFun.hasGaussianLaw
{ι : Type u_1}
{Ω : Type u_2}
[Fintype ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace ℝ (E i)]
[(i : ι) → MeasurableSpace (E i)]
[∀ (i : ι), CompleteSpace (E i)]
[∀ (i : ι), BorelSpace (E i)]
[∀ (i : ι), SecondCountableTopology (E i)]
{X : (i : ι) → Ω → E i}
(h : ∀ (i : ι), HasGaussianLaw (X i) P)
(hX : iIndepFun X P)
:
HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P
theorem
ProbabilityTheory.HasGaussianLaw.iIndepFun_of_cov
{ι : Type u_1}
{Ω : Type u_2}
[Fintype ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace ℝ (E i)]
[(i : ι) → MeasurableSpace (E i)]
[∀ (i : ι), CompleteSpace (E i)]
[∀ (i : ι), BorelSpace (E i)]
[∀ (i : ι), SecondCountableTopology (E i)]
{X : (i : ι) → Ω → E i}
(h : HasGaussianLaw (fun (ω : Ω) (i : ι) => X i ω) P)
(h' :
∀ (i j : ι), i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), covariance (⇑L₁ ∘ X i) (⇑L₂ ∘ X j) P = 0)
:
iIndepFun X P
theorem
ProbabilityTheory.HasGaussianLaw.indepFun_of_cov
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[CompleteSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[MeasurableSpace F]
[CompleteSpace F]
[BorelSpace F]
[SecondCountableTopology F]
{X : Ω → E}
{Y : Ω → F}
(h : HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P)
(h' : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), covariance (⇑L₁ ∘ X) (⇑L₂ ∘ Y) P = 0)
:
IndepFun X Y P
theorem
ProbabilityTheory.HasGaussianLaw.iIndepFun_of_cov'
{ι : Type u_1}
{Ω : Type u_2}
[Fintype ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → InnerProductSpace ℝ (E i)]
[(i : ι) → MeasurableSpace (E i)]
[∀ (i : ι), CompleteSpace (E i)]
[∀ (i : ι), BorelSpace (E i)]
[∀ (i : ι), SecondCountableTopology (E i)]
{X : (i : ι) → Ω → E i}
(h : HasGaussianLaw (fun (ω : Ω) (i : ι) => X i ω) P)
(h' :
∀ (i j : ι),
i ≠ j →
∀ (x : E i) (y : E j), covariance (fun (ω : Ω) => inner ℝ x (X i ω)) (fun (ω : Ω) => inner ℝ y (X j ω)) P = 0)
:
iIndepFun X P
theorem
ProbabilityTheory.HasGaussianLaw.indepFun_of_cov'
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_3}
{F : Type u_4}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[MeasurableSpace E]
[CompleteSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[NormedAddCommGroup F]
[InnerProductSpace ℝ F]
[MeasurableSpace F]
[CompleteSpace F]
[BorelSpace F]
[SecondCountableTopology F]
{X : Ω → E}
{Y : Ω → F}
(h : HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P)
(h' : ∀ (x : E) (y : F), covariance (fun (ω : Ω) => inner ℝ x (X ω)) (fun (ω : Ω) => inner ℝ y (Y ω)) P = 0)
:
IndepFun X Y P
theorem
ProbabilityTheory.HasGaussianLaw.iIndepFun_of_cov''
{ι : Type u_1}
{Ω : Type u_2}
[Fintype ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{κ : ι → Type u_3}
[(i : ι) → Fintype (κ i)]
{X : (i : ι) → κ i → Ω → ℝ}
(h : HasGaussianLaw (fun (ω : Ω) (i : ι) (j : κ i) => X i j ω) P)
(h' : ∀ (i j : ι), i ≠ j → ∀ (k : κ i) (l : κ j), covariance (X i k) (X j l) P = 0)
:
iIndepFun (fun (i : ι) (ω : Ω) (j : κ i) => X i j ω) P
theorem
ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_eq_zero
{ι : Type u_1}
{Ω : Type u_2}
[Fintype ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X : ι → Ω → ℝ}
[h1 : HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P]
(h2 : ∀ (i j : ι), i ≠ j → covariance (X i) (X j) P = 0)
:
iIndepFun X P
theorem
ProbabilityTheory.HasGaussianLaw.indepFun_of_cov''
{ι : Type u_1}
{Ω : Type u_2}
[Fintype ι]
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{κ : Type u_3}
[Fintype κ]
{X : ι → Ω → ℝ}
{Y : κ → Ω → ℝ}
(h : HasGaussianLaw (fun (ω : Ω) => (fun (i : ι) => X i ω, fun (j : κ) => Y j ω)) P)
(h' : ∀ (i : ι) (j : κ), covariance (X i) (Y j) P = 0)
:
IndepFun (fun (ω : Ω) (i : ι) => X i ω) (fun (ω : Ω) (j : κ) => Y j ω) P
theorem
ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_eq_zero
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X Y : Ω → ℝ}
[h1 : HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P]
(h2 : covariance X Y P = 0)
:
IndepFun X Y P
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
theorem
ProbabilityTheory.IndepFun.hasGaussianLaw_sub
{Ω : Type u_2}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
{X Y : Ω → E}
(hX : HasGaussianLaw X P)
(hY : HasGaussianLaw Y P)
(h : IndepFun X (Y - X) P)
:
HasGaussianLaw (Y - X) P