variance_const_zero
plain-language theorem explainer
The variance of any constant real-valued function on the hypercube {0,1}^n is zero. Researchers analyzing convergence rates for iterative cost reduction on the J-cost landscape cite this fact when treating flat or trivial cases. The proof is a direct algebraic reduction that unfolds the variance definition and simplifies the squared deviation term to zero.
Claim. Let $n$ be a natural number and $c$ a real number. For the constant function $f : (Fin n → Bool) → ℝ$ with $f(x) = c$ for all $x$, the variance of $f$ equals zero, where variance is the sum over all inputs of the squared deviation from the mean value of $f$.
background
The module studies the spectral gap of the J-cost Laplacian, where the gap λ₂ governs the speed of convergence of gradient descent on the J-cost landscape to its minimum. Variance is defined for any real-valued function x on the hypercube as the sum over all a of (x a minus the average of x over all b)^2. This supplies the base case for constant functions, which model flat landscapes with uniform cost.
proof idea
The proof is a one-line wrapper that unfolds the Variance definition and applies simp with the lemmas sub_self and sq to reduce the expression directly to zero.
why it matters
This lemma supplies the zero-variance case needed for convergence-rate arguments in the spectral-gap module. It supports results such as ConvergenceRate and iteration_bound_from_clauses by handling the trivial constant-function input. The module documentation links it to the empty_formula_flat_landscape fact and the overall control of convergence by λ₂ on the J-cost landscape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.