class IsSymmetricFunction {ι : Type u} [Fintype ι] [DecidableEq ι] (𝒜 : Set ↥(Matrix.orthogonalGroup ι ℝ)) (f : (ι → ℝ) → EReal) extends IsProperExtendedRealFunction f : Prop

Definition 7.1: a proper extended-real-valued function on ι → ℝ is symmetric with respect to a family 𝒜 of orthogonal matrices if it is invariant under the action of every element of 𝒜.

• ne_bot (x : ι → ℝ) : f x ≠ ⊥
• effective_domain_nonempty : (effective_domain f).Nonempty
• map_smul (A : ↥(Matrix.orthogonalGroup ι ℝ)) (hA : A ∈ 𝒜) (x : ι → ℝ) : f (A • x) = f x

instance instIsSymmetricFunctionOfNatEReal {ι : Type u} [Fintype ι] [DecidableEq ι] (𝒜 : Set ↥(Matrix.orthogonalGroup ι ℝ)) : IsSymmetricFunction 𝒜 fun (x : ι → ℝ) => 0

The constant zero extended-real-valued function is symmetric with respect to any family of orthogonal matrices.