theorem GaussianStability.integral_stdGaussian_comp_coord {n : ℕ} (i : Fin n) (f : ℝ → ℝ) (hf : MeasureTheory.AEStronglyMeasurable f (ProbabilityTheory.gaussianReal 0 1)) : ∫ (x : EuclideanSpace ℝ (Fin n)), f (x.ofLp i) ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n)) = ∫ (t : ℝ), f t ∂ProbabilityTheory.gaussianReal 0 1

theorem GaussianStability.sheppard_halfspace_stability_local {n : ℕ} (hn : 0 < n) (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) : (gaussianNoiseStability ρ hρ₀ hρ₁ fun (x : EuclideanSpace ℝ (Fin n)) => if 0 ≤ x.ofLp ⟨0, hn⟩ then 1 else -1) = 2 / Real.pi * Real.arcsin ρ

def GaussianStability.iterateSymmetrize {n : ℕ} (hn : 0 < n) : ℕ → (EuclideanSpace ℝ (Fin n) → ℝ) → EuclideanSpace ℝ (Fin n) → ℝ

theorem GaussianStability.symmetrize_coord_range {n : ℕ} (i : Fin n) (f : EuclideanSpace ℝ (Fin n) → ℝ) (x : EuclideanSpace ℝ (Fin n)) : symmetrize_coord i f x ∈ Set.Icc (-1) 1

theorem GaussianStability.iterateSymmetrize_range {n : ℕ} (hn : 0 < n) (k : ℕ) (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf_range : ∀ (x : EuclideanSpace ℝ (Fin n)), f x ∈ Set.Icc (-1) 1) (x : EuclideanSpace ℝ (Fin n)) : iterateSymmetrize hn k f x ∈ Set.Icc (-1) 1

theorem GaussianStability.iterateSymmetrize_mono_stability {n : ℕ} (hn : 0 < n) (k : ℕ) (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ρ₁ (iterateSymmetrize hn k f)

theorem GaussianStability.iterateSymmetrize_balanced_eq_halfspace_stability {n : ℕ} (hn : 0 < n) (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf_range : ∀ (x : EuclideanSpace ℝ (Fin n)), f x ∈ Set.Icc (-1) 1) (hf_balanced : ∫ (x : EuclideanSpace ℝ (Fin n)), f x ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n)) = 0) (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) : gaussianNoiseStability ρ hρ₀ hρ₁ (iterateSymmetrize hn n f) ≤ gaussianNoiseStability ρ hρ₀ hρ₁ fun (x : EuclideanSpace ℝ (Fin n)) => if 0 ≤ x.ofLp ⟨0, hn⟩ then 1 else -1

theorem GaussianStability.noise_stability_le_balanced_halfspace {n : ℕ} (hn : 0 < n) (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf_range : ∀ (x : EuclideanSpace ℝ (Fin n)), f x ∈ Set.Icc (-1) 1) (hf_balanced : ∫ (x : EuclideanSpace ℝ (Fin n)), f x ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n)) = 0) (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) : gaussianNoiseStability ρ hρ₀ hρ₁ f ≤ gaussianNoiseStability ρ hρ₀ hρ₁ fun (x : EuclideanSpace ℝ (Fin n)) => if 0 ≤ x.ofLp ⟨0, hn⟩ then 1 else -1

theorem GaussianStability.borel_isoperimetric_core {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf_range : ∀ (x : EuclideanSpace ℝ (Fin n)), f x ∈ Set.Icc (-1) 1) (hf_balanced : ∫ (x : EuclideanSpace ℝ (Fin n)), f x ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n)) = 0) (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) : gaussianNoiseStability ρ hρ₀ hρ₁ f ≤ 2 / Real.pi * Real.arcsin ρ

theorem GaussianStability.borel_isoperimetric_theorem {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf_range : ∀ (x : EuclideanSpace ℝ (Fin n)), f x ∈ Set.Icc (-1) 1) (hf_balanced : ∫ (x : EuclideanSpace ℝ (Fin n)), f x ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin n)) = 0) (ρ : ℝ) (hρ₀ : 0 ≤ ρ) (hρ₁ : ρ ≤ 1) : gaussianNoiseStability ρ hρ₀ hρ₁ f ≤ 1 - 2 / Real.pi * Real.arccos ρ