Theorems · Theorem · measure theory

essSup_comp_quotientAddGroup_mk

∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G]
  [IsTopologicalAddGroup G] [BorelSpace G] {μ : MeasureTheory.Measure G} {Γ : AddSubgroup G} {𝓕 : Set G},
  MeasureTheory.IsAddFundamentalDomain (↥Γ.op) 𝓕 μ →
    ∀ [Countable ↥Γ] [inst_6 : MeasurableSpace (G ⧸ Γ)] [BorelSpace (G ⧸ Γ)] [μ.IsAddRightInvariant]
      {g : G ⧸ Γ → ENNReal},
      AEMeasurable g (MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)) →
        essSup g (MeasureTheory.Measure.map QuotientAddGroup.mk (μ.restrict 𝓕)) = essSup (fun x => g ↑x) μ

The essSup of a function g on the additive quotient space G ⧸ Γ with respect to the pushforward of the restriction, μ_𝓕, of a right-invariant measure μ to a fundamental domain 𝓕, is the same as the essSup of g's lift to the universal cover G with respect to μ.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Quotient

Cited by

1 results in Mathlib

Foundations

Depth 214 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupMeasurableSpaceTopologicalSpaceIsTopologicalAddGroupBorelSpaceCountableMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddRightInvariant