English
Under the assumption of zero mean duals, the Gaussian product is invariant under rotation θ on the dual space.
Русский
При условии нулевых двойственных сред гауссова продукта инвариантна относительно вращения θ в двойственном пространстве.
LaTeX
$$$(\\mu \\otimes \\mu) \\circ (\\text{rotation }\\theta) = \\mu \\otimes \\mu$ under appropriate conditions on L$$
Lean4
/-- For a centered Gaussian measure `μ`, the product measure `μ.prod μ` is invariant under rotation.
The hypothesis `∀ L : StrongDual ℝ E, μ[L] = 0` is equivalent to the simpler
`μ[id] = 0`, but at this point we don't know yet that `μ` has a first moment so we can't use it.
See `map_rotation_eq_self`. -/
theorem map_rotation_eq_self_of_forall_strongDual_eq_zero [SecondCountableTopology E] [CompleteSpace E]
(hμ : ∀ L : StrongDual ℝ E, μ[L] = 0) (θ : ℝ) : (μ.prod μ).map (ContinuousLinearMap.rotation θ) = μ.prod μ :=
by
refine Measure.ext_of_charFunDual ?_
ext L
simp_rw [charFunDual_map, charFunDual_prod, charFunDual_eq_of_forall_strongDual_eq_zero hμ, ← Complex.exp_add]
rw [← add_div, ← add_div, ← neg_add, ← neg_add]
congr 3
norm_cast
have h1 :
(L.comp (.rotation θ)).comp (.inl ℝ E E) = Real.cos θ • L.comp (.inl ℝ E E) - Real.sin θ • L.comp (.inr ℝ E E) :=
by
ext x
simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.inl_apply,
ContinuousLinearMap.rotation_apply, smul_zero, add_zero]
rw [← L.comp_inl_add_comp_inr]
simp [-neg_smul, sub_eq_add_neg]
have h2 :
(L.comp (.rotation θ)).comp (.inr ℝ E E) = Real.sin θ • L.comp (.inl ℝ E E) + Real.cos θ • L.comp (.inr ℝ E E) :=
by
ext x
simp only [ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.inr_apply,
ContinuousLinearMap.rotation_apply, smul_zero, zero_add, ContinuousLinearMap.add_apply,
ContinuousLinearMap.coe_smul', Pi.smul_apply, ContinuousLinearMap.inl_apply, smul_eq_mul]
rw [← L.comp_inl_add_comp_inr]
simp
rw [h1, h2]
simp only [ContinuousLinearMap.coe_sub', ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_add']
rw [variance_sub, variance_smul, variance_add, variance_smul, variance_smul, covariance_smul_left,
covariance_smul_right, variance_smul, covariance_smul_left, covariance_smul_right]
· have h := Real.cos_sq_add_sin_sq θ
grind
all_goals exact (memLp_dual _ _ _ (by simp)).const_smul _
