theorem BooleanFourier.noiseSensitivity_majority_limit_pos (δ : ℝ) (hδ_pos : 0 < δ) : 0 < 1 / Real.pi * Real.arccos (1 - 2 * δ)

theorem BooleanFourier.majority_noiseSensitive (δ : ℝ) (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1 / 2) : Filter.Tendsto (fun (k : ℕ) => noiseSensitivityReal δ (majorityFn (2 * k + 1))) Filter.atTop (nhds (1 / Real.pi * Real.arccos (1 - 2 * δ))) ∧ 0 < 1 / Real.pi * Real.arccos (1 - 2 * δ)

theorem BooleanFourier.majority_noiseSensitivity_eventually_pos (δ : ℝ) (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1 / 2) : ∀ᶠ (k : ℕ) in Filter.atTop, 0 < noiseSensitivityReal δ (majorityFn (2 * k + 1))