variance_const_zero
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove variance positivity for non-constant functions.
- Does not compute or bound the spectral gap λ₂ itself.
- Does not address iteration counts or convergence rates directly.
formal statement (Lean)
42theorem variance_const_zero {n : ℕ} (c : ℝ) :
43 Variance (fun _ : Fin n → Bool => c) = 0 := by
proof body
Term-mode proof.
44 unfold Variance; simp [sub_self, sq]
45
46/-! ## Convergence Rate -/
47
48/-- A convergence rate for iterative cost reduction on the J-cost landscape. -/