theorem BooleanFourier.lindeberg_per_step_bound {n : ℕ} (f : (Fin n → Bool) → ℝ) (d : ℕ) (hdeg : degree f ≤ d) (Ψ : ℝ → ℝ) (hΨ : IsC3Bounded Ψ) (k : Fin n) : |hybridExpectation f Ψ ↑k - hybridExpectation f Ψ (↑k + 1)| ≤ 1 / 2 * 2 ^ (3 * ↑d / 2) * hΨ.thirdDerivBound * fourierInfluence f k ^ (3 / 2)