map_rotation_eq_self — Mathlib

English

Under zero-mean dual hypothesis, the rotation of μ × μ leaves μ × μ unchanged.

Русский

При нулевой средней двойственности вращение μ × μ не изменяет распределение μ × μ.

LaTeX

$$$(\\forall L, μ[L] = 0) \\Rightarrow (μ.prod μ).map(R_{\\theta}) = μ.prod μ$$$

Lean4

/-- For a centered Gaussian measure `μ`, the product measure `μ.prod μ` is invariant under
rotation. -/
theorem map_rotation_eq_self (hμ : μ[id] = 0) (θ : ℝ) : (μ.prod μ).map (ContinuousLinearMap.rotation θ) = μ.prod μ :=
  by
  refine map_rotation_eq_self_of_forall_strongDual_eq_zero (fun L ↦ ?_) θ
  simp only [id_eq] at hμ
  simp [integral_dual, hμ]

Похожие утверждения