Definitions/Def_Mathlib_MeasureTheory_Group_Measure.lean

The module records one lemma, Topology.IsOpenEmbedding.isHaarMeasure_comap. The data are two groups G and H, each carrying a topology and a measurable structure for which multiplication is measurable in each variable separately and the \sigma-algebra is the Borel \sigma-algebra, a monoid homomorphism \varphi : G \to H together with the hypothesis that \varphi is an open embedding (injective, continuous, with open image and inducing the subspace topology), and a measure \mu on H that is a Haar measure in Mathlib's sense. The conclusion is that the pullback measure \operatorname{comap} \varphi\, \mu on G — which, \varphi being a measurable embedding, is the measure s \mapsto \mu(\varphi(s)) on measurable sets — is again a Haar measure. Since IsHaarMeasure is a structure whose fields are three theorems, the statement amounts to three assertions about \operatorname{comap}\varphi\,\mu: left invariance under translation by elements of G, finiteness on compact subsets of G, and strict positivity on nonempty open subsets of G. The first comes from the imported lemma MeasurableEmbedding.isMulLeftInvariant_comap, which transports left invariance of a measure along a measurable embedding of a group into a monoid (using that \varphi(g\cdot\,)^{-1}-preimages correspond to \varphi(g)-translates of images); the second from the imported Topology.IsOpenEmbedding.isFiniteMeasureOnCompacts_comap, the point being that \varphi carries compact sets to compact sets; the third from Mathlib's comap lemma for measures positive on open sets, where openness of the embedding is what is needed. The @[to_additive] attribute produces the corresponding statement for additive groups and additive Haar measures.