noncomputable def GaussianStability.gaussianSpace (n : ℕ) : MeasureTheory.Measure (Fin n → ℝ)

structure GaussianStability.IsRhoCorrelated {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X Y : Ω → ℝ) (ρ : ℝ) : Prop

• rho_mem : ρ ∈ Set.Icc (-1) 1
• hX_meas : Measurable X
• hY_meas : Measurable Y
• hX_dist : MeasureTheory.Measure.map X μ = ProbabilityTheory.gaussianReal 0 1
• hY_dist : MeasureTheory.Measure.map Y μ = ProbabilityTheory.gaussianReal 0 1
• hXY_corr : ∫ (ω : Ω), X ω * Y ω ∂μ = ρ

noncomputable def GaussianStability.rhoCorrelatedGaussian (ρ : ℝ) : MeasureTheory.Measure (ℝ × ℝ)

noncomputable def GaussianStability.gaussianNoiseOperator {n : ℕ} (ρ : ℝ) (f : EuclideanSpace ℝ (Fin n) → ℝ) (z : EuclideanSpace ℝ (Fin n)) : ℝ

noncomputable def GaussianStability.gaussianNoiseStability {n : ℕ} (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) (f : EuclideanSpace ℝ (Fin n) → ℝ) : ℝ