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

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