Representation Values Depend Only on the Image of a Block

This is a group-theoretic auxiliary lemma for partial symmetrization.

Let $\Omega$ be a finite type, let $V$ be a real inner-product space, and let $\rho$ be a monoid homomorphism from permutations of $\Omega$ to linear isometric equivalences of $V$. Let $A,B\subseteq\Omega$ be finite subsets, let $v\in V$, and suppose:

1. $\rho(\sigma)v=v$ for every permutation $\sigma$ fixing every point outside $A$.
2. $\rho(\sigma)v=v$ for every permutation $\sigma$ fixing every point outside $B$.
3. $\sigma$ and $\tau$ both fix every point outside $A\cup B$.
4. $\sigma(A)=\tau(A)$.

Then

The lemma shows that, under the two invariance assumptions, the represented vector depends only on the image of $A$.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.Tensor. Shown in its original module context. Proof omitted.

theorem apply_eq_of_image_eq (ρ : Equiv.Perm Ω →* (V ≃ₗᵢ[ℝ] V)) {A B : Finset Ω} (v : V)
    (hvA : ∀ σ ∈ fixingOutside A, ρ σ v = v) (hvB : ∀ σ ∈ fixingOutside B, ρ σ v = v)
    {σ τ : Equiv.Perm Ω} (hσ : σ ∈ fixingOutside (A ∪ B)) (hτ : τ ∈ fixingOutside (A ∪ B))
    (h : A.image σ = A.image τ) : ρ σ v = ρ τ v

Module navigation

Module: Analysis/Tensor/Symmetrization.

Previous: exists_mem_fixingOutside_image_eq · Next: image_mem_powersetCard_of_mem_fixingOutside.

Source excerpt, lines 606–609 · Frozen source 408915f.