theorem BooleanFourier.noiseSensitivity_majority_tendsto (δ : ℝ) (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 * δ)))