mathlib

3751ec63 - feat(measure_theory/group/fundamental_domain): ess_sup_measure_restrict (#12603)

feat(measure_theory/group/fundamental_domain): ess_sup_measure_restrict (#12603) If `f` is invariant under the action of a countable group `G`, and `μ` is a `G`-invariant measure with a fundamental domain `s`, then the `ess_sup` of `f` restricted to `s` is the same as that of `f` on all of its domain. Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>