BrownianMotion.Auxiliary.HasLaw

source

class ProbabilityTheory.HasGaussianLaw {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {E : Type u_2} (X : Ω → E) (P : MeasureTheory.Measure Ω) [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] [mE : MeasurableSpace E] :

Prop

The predicate HasGaussianLaw X P means that under the measure P, X has a Gaussian distribution

isGaussian_map : IsGaussian (MeasureTheory.Measure.map X P)

Instances

source

instance ProbabilityTheory.IsGaussian.hasGaussianLaw {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {E : Type u_2} {X : Ω → E} {P : MeasureTheory.Measure Ω} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] [mE : MeasurableSpace E] [IsGaussian (MeasureTheory.Measure.map X P)] :

HasGaussianLaw X P

source

instance ProbabilityTheory.IsGaussian.hasGaussianLaw_fun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {E : Type u_2} {X : Ω → E} {P : MeasureTheory.Measure Ω} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] [mE : MeasurableSpace E] [IsGaussian (MeasureTheory.Measure.map X P)] :

HasGaussianLaw (fun (ω : Ω) => X ω) P

source

instance ProbabilityTheory.IsGaussian.hasGaussianLaw_id {E : Type u_2} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} [IsGaussian μ] :

HasGaussianLaw id μ

source

theorem ProbabilityTheory.HasGaussianLaw.aemeasurable {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {E : Type u_2} {X : Ω → E} {P : MeasureTheory.Measure Ω} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] [mE : MeasurableSpace E] [hX : HasGaussianLaw X P] :

AEMeasurable X P

source

theorem ProbabilityTheory.HasGaussianLaw.isProbabilityMeasure {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {E : Type u_2} {X : Ω → E} {P : MeasureTheory.Measure Ω} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] [mE : MeasurableSpace E] [HasGaussianLaw X P] :

MeasureTheory.IsProbabilityMeasure P

source

theorem ProbabilityTheory.HasLaw.hasGaussianLaw {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {E : Type u_2} {X : Ω → E} {P : MeasureTheory.Measure Ω} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} (hX : HasLaw X μ P) [IsGaussian μ] :

HasGaussianLaw X P

source

instance ProbabilityTheory.HasGaussianLaw.map {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {E : Type u_2} {X : Ω → E} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] (L : E →L[ℝ ] F) [HasGaussianLaw X P] :

HasGaussianLaw (⇑L ∘ X) P

source

instance ProbabilityTheory.HasGaussianLaw.map_fun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {E : Type u_2} {X : Ω → E} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] (L : E →L[ℝ ] F) [hX : HasGaussianLaw X P] :

HasGaussianLaw (fun (ω : Ω) => L (X ω)) P

source

instance ProbabilityTheory.HasGaussianLaw.map_equiv {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {E : Type u_2} {X : Ω → E} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] (L : E ≃L[ℝ ] F) [HasGaussianLaw X P] :

HasGaussianLaw (⇑L ∘ X) P

source

instance ProbabilityTheory.HasGaussianLaw.map_equiv_fun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {E : Type u_2} {X : Ω → E} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] (L : E ≃L[ℝ ] F) [hX : HasGaussianLaw X P] :

HasGaussianLaw (fun (ω : Ω) => L (X ω)) P

source

instance ProbabilityTheory.HasGaussianLaw.eval {ι : Type u_4} {Ω : Type u_5} {E : ι → Type u_6} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace ℝ (E i)] [(i : ι) → MeasurableSpace (E i)] [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)] {X : (i : ι) → Ω → E i} [h : HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P] (i : ι) :

HasGaussianLaw (X i) P

source

instance ProbabilityTheory.HasGaussianLaw.toLp_comp {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} (p : ENNReal) [Fact (1 ≤ p)] {ι : Type u_4} [Fintype ι] {E : ι → Type u_5} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace ℝ (E i)] [(i : ι) → MeasurableSpace (E i)] [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)] {X : (i : ι) → Ω → E i} [HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P] :

HasGaussianLaw (fun (ω : Ω) => WithLp.toLp p fun (x : ι) => X x ω) P

source

instance ProbabilityTheory.IsGaussian.map_eval {ι : Type u_4} [Fintype ι] {E : ι → Type u_5} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace ℝ (E i)] {mE : (i : ι) → MeasurableSpace (E i)} [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)] {μ : MeasureTheory.Measure ((i : ι) → E i)} [IsGaussian μ] (i : ι) :

HasGaussianLaw (fun (x : (i : ι) → E i) => x i) μ

source

instance ProbabilityTheory.IsGaussian.map_eval_piLp (p : ENNReal) [Fact (1 ≤ p)] {ι : Type u_4} [Fintype ι] {E : ι → Type u_5} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → NormedSpace ℝ (E i)] {mE : (i : ι) → MeasurableSpace (E i)} [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)] {μ : MeasureTheory.Measure (PiLp p E)} [IsGaussian μ] (i : ι) :

HasGaussianLaw (fun (x : PiLp p E) => x i) μ

source

instance ProbabilityTheory.HasGaussianLaw.sub {ι : Type u_4} {Ω : Type u_5} {E : Type u_6} [Fintype ι] {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {X : ι → Ω → E} [h : HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P] (i j : ι) :

HasGaussianLaw (X i - X j) P

source

instance ProbabilityTheory.IsGaussian.map_eval_sub_eval {ι : Type u_4} {E : Type u_5} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure (ι → E)} [IsGaussian μ] (i j : ι) :

HasGaussianLaw (fun (x : ι → E) => x i - x j) μ

source

instance ProbabilityTheory.IsGaussian.map_eval_sub_eval_piLp (p : ENNReal) [Fact (1 ≤ p)] {ι : Type u_4} {E : Type u_5} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure (PiLp p fun (x : ι) => E)} [IsGaussian μ] (i j : ι) :

HasGaussianLaw (fun (x : PiLp p fun (x : ι) => E) => x i - x j) μ