English
If each component group has a left-invariant volume, then the product measure on the function space has left-invariant volume.
Русский
Если каждая компонентная группа имеет левостороннюю инвариантность объема, то произведение меры на пространстве функций имеет левостороннюю инвариантность объема.
LaTeX
$$$\forall i, IsMulLeftInvariant(volume_i) \Rightarrow IsMulLeftInvariant(volume)$$$
Lean4
/-- We intentionally restrict this only to the nondependent function space, since type-class
inference cannot find an instance for `ι → ℝ` when this is stated for dependent function spaces. -/
@[to_additive /-- We intentionally restrict this only to the nondependent function space, since
type-class inference cannot find an instance for `ι → ℝ` when this is stated for dependent function
spaces. -/
]
instance isMulLeftInvariant_volume {α} [Group α] [MeasureSpace α] [SigmaFinite (volume : Measure α)] [MeasurableMul α]
[IsMulLeftInvariant (volume : Measure α)] : IsMulLeftInvariant (volume : Measure (ι → α)) :=
pi.isMulLeftInvariant _
