English
Euclidean spaces indexed by a finite set admit a canonical Borel structure; hence they are standard Borel spaces.
Русский
Евклидовмы пространства, индексируемые по конечному множеству, обладают канонической Борелевской структурой; это стандартные Борелевы пространства.
LaTeX
$$$[Finite\;\iota]\Rightarrow BorelSpace(\mathbb{R}^{\iota})$$$
Lean4
/-- If a measure `μ` on the quotient `G ⧸ Γ` of a group `G` by a discrete normal subgroup `Γ` having
fundamental domain, satisfies `QuotientMeasureEqMeasurePreimage` relative to a standardized choice
of Haar measure on `G`, and assuming `μ` is finite, then `μ` is itself Haar.
TODO: Is it possible to drop the assumption that `μ` is finite? -/
@[to_additive /-- If a measure `μ` on the quotient `G ⧸ Γ` of an additive group `G` by a discrete
normal subgroup `Γ` having fundamental domain, satisfies `AddQuotientMeasureEqMeasurePreimage`
relative to a standardized choice of Haar measure on `G`, and assuming `μ` is finite, then `μ` is
itself Haar. -/
]
theorem haarMeasure_quotient [LocallyCompactSpace G] [QuotientMeasureEqMeasurePreimage ν μ]
[i : HasFundamentalDomain Γ.op G ν] [IsFiniteMeasure μ] : IsHaarMeasure μ :=
by
obtain ⟨K⟩ := PositiveCompacts.nonempty' (α := G)
let K' : PositiveCompacts (G ⧸ Γ) := K.map π QuotientGroup.continuous_mk QuotientGroup.isOpenMap_coe
haveI : IsMulLeftInvariant μ := MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient ν
rw [haarMeasure_unique μ K']
have finiteCovol : covolume Γ.op G ν ≠ ⊤ :=
ne_top_of_lt <| QuotientMeasureEqMeasurePreimage.covolume_ne_top μ (ν := ν)
obtain ⟨s, fund_dom_s⟩ := i
rw [fund_dom_s.covolume_eq_volume] at finiteCovol
erw [fund_dom_s.projection_respects_measure_apply μ K'.isCompact.measurableSet]
apply IsHaarMeasure.smul
· intro h
haveI i' : IsOpenPosMeasure (ν : Measure G) := inferInstance
apply IsOpenPosMeasure.open_pos (interior K) (μ := ν) (self := i')
· exact isOpen_interior
· exact K.interior_nonempty
rw [← le_zero_iff, ← fund_dom_s.measure_zero_of_invariant _ (fun g ↦ QuotientGroup.sound _ _ g) h]
apply measure_mono
refine interior_subset.trans ?_
rw [QuotientGroup.coe_mk']
change (K : Set G) ⊆ π ⁻¹' (π '' K)
exact subset_preimage_image π K
· change ν (π ⁻¹' (π '' K) ∩ s) ≠ ⊤
apply ne_of_lt
refine lt_of_le_of_lt ?_ finiteCovol.lt_top
apply measure_mono
exact inter_subset_right
