English
For a Gaussian μ, the dual evaluation of μ convolved with its negated pushforward vanishes: (μ ∗ μ.map(−id))[L] = 0 for all L.
Русский
Для гауссовой μ двойная конволюция с её отображением по отрицанию имеет нулевое значение на любой линейной функциональной величине L.
LaTeX
$$$(\\mu \\ast (\\mu\\circ(-\\mathrm{Id})))[L] = 0 \\quad \\forall L.$$
Lean4
/-- The convolution of a Gaussian measure `μ` and its map by `x ↦ -x` is centered. -/
theorem integral_dual_conv_map_neg_eq_zero (L : StrongDual ℝ E) : (μ ∗ (μ.map (ContinuousLinearEquiv.neg ℝ)))[L] = 0 :=
by
rw [integral_conv (by fun_prop)]
simp only [map_add]
calc
∫ x, ∫ y, L x + L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) ∂μ
_ = ∫ x, L x + ∫ y, L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) ∂μ :=
by
congr with x
rw [integral_add (by fun_prop) (by fun_prop)]
simp [-ContinuousLinearEquiv.coe_neg, integral_const, smul_eq_mul]
_ = ∫ x, L x ∂μ + ∫ y, L y ∂μ.map (ContinuousLinearEquiv.neg ℝ) :=
by
rw [integral_add (by fun_prop) (by fun_prop)]
simp
_ = 0 := by
rw [integral_map (by fun_prop) (by fun_prop)]
simp [integral_neg]
