UniformWeights
plain-language theorem explainer
UniformWeights defines the predicate that an n-dimensional real vector has every component equal to one fixed real scalar. Researchers calibrating symmetric cost functions or proving norm identities under isotropy cite it to encode the uniform case. The definition is a direct existential statement over that common scalar with no further computation or lemmas required.
Claim. A vector $α : ℝ^n$ has uniform weights when there exists a real number $a$ such that $α_i = a$ for all indices $i$.
background
The module supplies calibration identities that relate uniform weight vectors to their squared norms and sums. Vec is the abbreviation for n-component real vectors, written as maps from Fin n to ℝ. The local setting is the study of calibration relations for uniform weights, which supply the isotropy assumption used by all downstream results in the same file and in the Symmetry sibling module.
proof idea
The declaration is a direct definition. It encodes the uniform condition by quantifying existentially over the common scalar value a and asserting equality for every coordinate.
why it matters
UniformWeights is the hypothesis that feeds sqNorm_uniform, weightSum_uniform, uniform_sqNorm_one, uniform_weight_of_sum_one, coeff_perm_invariant_of_uniform and uniform_of_coeff_perm_invariant. These results establish the concrete arithmetic consequences of isotropy for norms and sums, and the symmetry module uses the predicate to link uniformity with permutation invariance. The definition therefore closes the calibration layer before higher-dimensional or phi-ladder arguments are invoked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.