def GaussianStability.EuclideanSpace.updateCoord {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) (i : Fin n) (t : ℝ) : EuclideanSpace ℝ (Fin n)

@[simp]

theorem GaussianStability.EuclideanSpace.updateCoord_same {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) (i : Fin n) (t : ℝ) : (updateCoord x i t).ofLp i = t

@[simp]

theorem GaussianStability.EuclideanSpace.updateCoord_ne {n : ℕ} (x : EuclideanSpace ℝ (Fin n)) (i j : Fin n) (t : ℝ) (hij : j ≠ i) : (updateCoord x i t).ofLp j = x.ofLp j

noncomputable def GaussianStability.conditionalMean {n : ℕ} (i : Fin n) (f : EuclideanSpace ℝ (Fin n) → ℝ) (x : EuclideanSpace ℝ (Fin n)) : ℝ

noncomputable def GaussianStability.symmetrize_coord {n : ℕ} (i : Fin n) (f : EuclideanSpace ℝ (Fin n) → ℝ) : EuclideanSpace ℝ (Fin n) → ℝ

noncomputable def GaussianStability.fiberNoiseStability1D {n : ℕ} (i : Fin n) (f : EuclideanSpace ℝ (Fin n) → ℝ) (ρ : ℝ) (x : EuclideanSpace ℝ (Fin n)) : ℝ

noncomputable def GaussianStability.fiberNoiseStability1D_symmetrized {n : ℕ} (i : Fin n) (f : EuclideanSpace ℝ (Fin n) → ℝ) (ρ : ℝ) (x : EuclideanSpace ℝ (Fin n)) : ℝ

theorem GaussianStability.fiber_stability_le_symmetrized {n : ℕ} (i : Fin n) (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf_range : ∀ (x : EuclideanSpace ℝ (Fin n)), f x ∈ Set.Icc (-1) 1) (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) (x : EuclideanSpace ℝ (Fin n)) : fiberNoiseStability1D i f ρ x ≤ fiberNoiseStability1D_symmetrized i f ρ x

theorem GaussianStability.gaussianNoiseStability_eq_integral_fiber {n : ℕ} (i : Fin n) (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf_range : ∀ (x : EuclideanSpace ℝ (Fin n)), f x ∈ Set.Icc (-1) 1) (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) : gaussianNoiseStability ρ hρ₀ hρ₁ f = ∫ (x : EuclideanSpace ℝ (Fin n)), fiberNoiseStability1D i f ρ x ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n))

theorem GaussianStability.gaussianNoiseStability_symmetrized_eq_integral_fiber {n : ℕ} (i : Fin n) (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf_range : ∀ (x : EuclideanSpace ℝ (Fin n)), f x ∈ Set.Icc (-1) 1) (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) : gaussianNoiseStability ρ hρ₀ hρ₁ (symmetrize_coord i f) = ∫ (x : EuclideanSpace ℝ (Fin n)), fiberNoiseStability1D_symmetrized i f ρ x ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n))

theorem GaussianStability.integrable_fiberNoiseStability1D {n : ℕ} (i : Fin n) (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf_range : ∀ (x : EuclideanSpace ℝ (Fin n)), f x ∈ Set.Icc (-1) 1) (ρ : ℝ) : MeasureTheory.Integrable (fiberNoiseStability1D i f ρ) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n)))

theorem GaussianStability.integrable_fiberNoiseStability1D_symmetrized {n : ℕ} (i : Fin n) (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf_range : ∀ (x : EuclideanSpace ℝ (Fin n)), f x ∈ Set.Icc (-1) 1) (ρ : ℝ) : MeasureTheory.Integrable (fiberNoiseStability1D_symmetrized i f ρ) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n)))

theorem GaussianStability.coordinate_symmetrization_increases_stability {n : ℕ} (i : Fin n) (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf_range : ∀ (x : EuclideanSpace ℝ (Fin n)), f x ∈ Set.Icc (-1) 1) (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) : gaussianNoiseStability ρ hρ₀ hρ₁ f ≤ gaussianNoiseStability ρ hρ₀ hρ₁ (symmetrize_coord i f)