English
The map of Haar measure under a linear isomorphism aligns with the corresponding mapped Haar measure on the target space.
Русский
Образ меры Хаара через линейное изоморфизм согласуется с соответствующей образованной мерой Хаара на целевом пространстве.
LaTeX
$$$\text{map } f \ b.addHaar = (b.map f.toLinearEquiv).addHaar$$$
Lean4
theorem map_addHaar {ι E F : Type*} [Fintype ι] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E]
[NormedSpace ℝ F] [MeasurableSpace E] [MeasurableSpace F] [BorelSpace E] [BorelSpace F] [SecondCountableTopology F]
[SigmaCompactSpace F] (b : Basis ι ℝ E) (f : E ≃L[ℝ] F) : map f b.addHaar = (b.map f.toLinearEquiv).addHaar :=
by
rw [eq_comm, Basis.addHaar_eq_iff,
Measure.map_apply f.continuous.measurable (PositiveCompacts.isCompact _).measurableSet, Basis.coe_parallelepiped,
Basis.coe_map]
erw [← image_parallelepiped, f.toEquiv.preimage_image, addHaar_self]
