Rotation in product space

Stream: Is there code for X?

[Rémy Degenne]

I want to prove results about probability measures μ on a normed space E such that the product μ.prod μ on E × E is invariant by rotation. For that I need a rotation as a continuous linear map.
I wrote this, which works for my purpose:

import Mathlib
variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace ℝ E]

/-- The rotation in `E × E` with angle `θ`, as a continuous linear map. -/
noncomputable
def ContinuousLinearMap.rotation (θ : ℝ) : E × E →L[ℝ] E × E where
  toFun := fun x ↦ (Real.cos θ • x.1 + Real.sin θ • x.2, - Real.sin θ • x.1 + Real.cos θ • x.2)
  map_add' x y := by
    simp only [Prod.fst_add, smul_add, Prod.snd_add, neg_smul, Prod.mk_add_mk]
    abel_nf
  map_smul' c x := by simp [smul_comm c]
  cont := by fun_prop

My questions are:

• is there a definition in Mathlib that I should be using instead of defining something new?
• if not, does the def above look good? Where should it go?

[Kenny Lau]

why is what you wrote the right thing to consider?

[Rémy Degenne]

The main hypothesis for Fernique's theorem corresponds to (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) = μ.prod μ with the definition above. That's the only reason I introduce this. See #26291.

[Kenny Lau]

@Rémy Degenne Orientation.rotation is what you need

[Kenny Lau]

oh wait

[Kenny Lau]

that one still assumes dimension 2, sorry

[Joseph Myers]

When you're working with rotations as linear isometries in inner product spaces, I think the natural way to produce rotations in more than two dimensions is via constructing isometries for the whole space out of isometries on orthogonal subspaces (note: I'm not sure what if any API we have for such constructions of isometries at present).

[Eric Wieser]

Should this be using WithLp to make the rotation an isometry?

[Heather Macbeth]

Morally we are considering E × E as the tensor product of E and $\mathbb{R}^2$, and constructing the tensor product of the identity rotation of E with the $(\cos \theta, \sin \theta)$ rotation of $\mathbb{R}^2$. Since none of this has available API in mathlib, I would personally say that Remy's way is fine!

[Heather Macbeth]

I guess another abstract point of view which applies here is that, given a complex vector space, there is a family of rotations $z \mapsto e^{i\theta}\cdot z$. Here the complex vector space is the complexification of E, which can be identified (as a real vector space) with E × E.