quotientMeasureEqMeasurePreimage_quotientMeasure

English

Given a fundamental domain s, the quotient measure preimage of ν along π is μ = (ν|s).map π.

Русский

Пусть s — фундаментальная область; тогда mера на факторпространстве задаётся как перевод меры ν, ограниченной на s, по отображению π: μ = (ν|s).map π.

LaTeX

$$$IsFundamentalDomain(G,s,\\nu) \\Rightarrow \\ QuotientMeasureEqMeasurePreimage\\nu\\left((\\nu|_{s}).map \\pi\\right).$$$

Lean4

/-- Given a measure upstairs (i.e., on `α`), and a choice `s` of fundamental domain, there's always
an artificial way to generate a measure downstairs such that the pair satisfies the
`QuotientMeasureEqMeasurePreimage` typeclass. -/
@[to_additive]
theorem quotientMeasureEqMeasurePreimage_quotientMeasure {s : Set α} (fund_dom_s : IsFundamentalDomain G s ν) :
    QuotientMeasureEqMeasurePreimage ν ((ν.restrict s).map π) where
  projection_respects_measure' t fund_dom_t := by rw [fund_dom_s.quotientMeasure_eq _ fund_dom_t]

Похожие утверждения