LevelSet
plain-language theorem explainer
LevelSet defines the affine hyperplanes orthogonal to a fixed direction α at constant level c in n-dimensional space. Researchers analyzing the radical distribution of a rank-one log-coordinate Hessian cite this when proving that the distribution is integrable along parallel leaves. The definition is realized directly as the set comprehension collecting all vectors t with weighted dot product α · t equal to c.
Claim. For direction vector α ∈ ℝⁿ and level c ∈ ℝ the level set is the affine hyperplane { t ∈ ℝⁿ | α · t = c }, where α · t denotes the weighted dot product ∑ α_i t_i.
background
The module treats the radical distribution of the rank-one log-coordinate Hessian, which detects only a single active direction α. The radical itself consists of vectors v satisfying dot α v = 0; the parallel affine leaves are the level sets at constant c. Upstream, dot is the weighted dot product used by the logarithmic aggregate and Vec n is the type of n-component real vectors (Fin n → ℝ). The module formalizes the distribution and its integrability via these affine leaves.
proof idea
The definition is a direct set comprehension { t | dot α t = c } using the dot product from Core; no lemmas or tactics are invoked.
why it matters
LevelSet supplies the concrete affine leaves that realize integrability of the radical distribution. It is invoked by affineShift_mem_LevelSet (shifts along radical directions preserve the leaves), mem_LevelSet_iff (membership equivalence), preserves_own_leaf_iff_mem_Radical, and radical_integrable_by_affine_leaves (the distribution integrates exactly over these hyperplanes). In the Recognition framework this supports the cost analysis in N dimensions under the rank-one Hessian structure induced by the logarithmic aggregate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.