Invariant inner products for finite actions

A real inner product can be summed over a finite monoid representation. The resulting positive-definite symmetric bilinear form controls the original norm, and its positive strict sublevel sets are convex, contain the origin and, in finite dimensions, are open neighbourhoods of it; arbitrarily small such sublevel sets fit inside a prescribed open neighbourhood. When the monoid is a group, so that it acts by linear automorphisms, the form is preserved by the action, without any faithfulness assumption, and so are its sublevel sets.

These invariant ellipsoids are the linear-algebraic shrinking device in finite-action charts: an equivariant chart about a fixed point can be restricted to an invariant ball while retaining every group element, including elements acting trivially.

The construction specializes Representation.sumOfConjugatesForm, the undivided form average already used for invariant-form theory. Division by the positive group order would only rescale the form and its sublevel sets. This is the classical construction used in the proof of Bochner linearization; see S. Bochner, Compact groups of differentiable transformations, Ann. of Math. 46 (1945), 372–381.

Main definitions and results

• Representation.posDef_toQuadraticMap_sumOfConjugatesForm_inner: the orbit-sum inner product is positive definite.
• Representation.sumOfConjugatesInnerSublevel: its strict sublevel sets, open in finite dimensions.
• Representation.exists_pos_sumOfConjugatesInnerSublevel_subset: arbitrarily small such sublevel sets exist.
• Representation.convex_sumOfConjugatesInnerSublevel: these sublevel sets are convex.
• Representation.preimage_sumOfConjugatesInnerSublevel: for a group, every element preserves these sublevel sets.

theorem Representation.sumOfConjugatesForm_inner_apply_self {G : Type u_1} {V : Type u_2} [Monoid G] [Fintype G] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (ρ : Representation ℝ G V) (x : V) : ((ρ.sumOfConjugatesForm (innerₗ V)) x) x = ∑ g : G, ‖(ρ g) x‖ ^ 2

The orbit-sum inner product of x with itself is the sum of the squared norms of the points ρ g x.

theorem Representation.posDef_toQuadraticMap_sumOfConjugatesForm_inner {G : Type u_1} {V : Type u_2} [Monoid G] [Fintype G] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (ρ : Representation ℝ G V) : (LinearMap.BilinMap.toQuadraticMap (ρ.sumOfConjugatesForm (innerₗ V))).PosDef

The orbit-sum inner product is positive definite.

theorem Representation.continuous_sumOfConjugatesForm_inner_apply_self {G : Type u_1} {V : Type u_2} [Monoid G] [Fintype G] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (ρ : Representation ℝ G V) : Continuous fun (x : V) => ((ρ.sumOfConjugatesForm (innerₗ V)) x) x

The orbit-sum quadratic value varies continuously in finite dimensions.

theorem Representation.norm_sq_le_sumOfConjugatesForm_inner_apply_self {G : Type u_1} {V : Type u_2} [Monoid G] [Fintype G] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (ρ : Representation ℝ G V) (x : V) : ‖x‖ ^ 2 ≤ ((ρ.sumOfConjugatesForm (innerₗ V)) x) x

The orbit-sum inner product controls the original squared norm through the identity summand.

def Representation.sumOfConjugatesInnerSublevel {G : Type u_1} {V : Type u_2} [Monoid G] [Fintype G] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (ρ : Representation ℝ G V) (c : ℝ) : Set V

The strict sublevel set {x | ∑ g, ‖ρ g x‖ ^ 2 < c} of the orbit-sum inner product; the parameter c is a squared radius, and the set is nonempty exactly when 0 < c. When G is a group the set is ρ-invariant (Representation.preimage_sumOfConjugatesInnerSublevel).

@[simp]

theorem Representation.mem_sumOfConjugatesInnerSublevel {G : Type u_1} {V : Type u_2} [Monoid G] [Fintype G] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (ρ : Representation ℝ G V) {c : ℝ} {x : V} : x ∈ ρ.sumOfConjugatesInnerSublevel c ↔ ((ρ.sumOfConjugatesForm (innerₗ V)) x) x < c

theorem Representation.isOpen_sumOfConjugatesInnerSublevel {G : Type u_1} {V : Type u_2} [Monoid G] [Fintype G] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (ρ : Representation ℝ G V) (c : ℝ) : IsOpen (ρ.sumOfConjugatesInnerSublevel c)

The orbit-sum inner sublevel sets are open in finite dimensions.

theorem Representation.exists_pos_sumOfConjugatesInnerSublevel_subset {G : Type u_1} {V : Type u_2} [Monoid G] [Fintype G] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (ρ : Representation ℝ G V) {U : Set V} (hU : IsOpen U) (h0 : 0 ∈ U) : ∃ c > 0, ρ.sumOfConjugatesInnerSublevel c ⊆ U

Every open neighbourhood of the origin contains a positive orbit-sum inner sublevel set.

theorem Representation.convex_sumOfConjugatesInnerSublevel {G : Type u_1} {V : Type u_2} [Monoid G] [Fintype G] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (ρ : Representation ℝ G V) (c : ℝ) : Convex ℝ (ρ.sumOfConjugatesInnerSublevel c)

The orbit-sum inner sublevel sets are convex.

@[simp]

theorem Representation.preimage_sumOfConjugatesInnerSublevel {G : Type u_1} {V : Type u_2} [Group G] [Fintype G] [NormedAddCommGroup V] [InnerProductSpace ℝ V] (ρ : Representation ℝ G V) (g : G) (c : ℝ) : ⇑(ρ g) ⁻¹' ρ.sumOfConjugatesInnerSublevel c = ρ.sumOfConjugatesInnerSublevel c

Every group element preserves every orbit-sum inner sublevel set.