Documentation

Mathlib.MeasureTheory.Group.Measure

Measures on Groups #

We develop some properties of measures on (topological) groups

We also give analogues of all these notions in the additive world.

A measure μ on a measurable additive group is left invariant if the measure of left translations of a set are equal to the measure of the set itself.

Instances
    theorem MeasureTheory.Measure.IsAddLeftInvariant.map_add_left_eq_self {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [self : μ.IsAddLeftInvariant] (g : G) :
    MeasureTheory.Measure.map (fun (x : G) => g + x) μ = μ

    A measure μ on a measurable group is left invariant if the measure of left translations of a set are equal to the measure of the set itself.

    Instances
      theorem MeasureTheory.Measure.IsMulLeftInvariant.map_mul_left_eq_self {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [self : μ.IsMulLeftInvariant] (g : G) :
      MeasureTheory.Measure.map (fun (x : G) => g * x) μ = μ

      A measure μ on a measurable additive group is right invariant if the measure of right translations of a set are equal to the measure of the set itself.

      Instances
        theorem MeasureTheory.Measure.IsAddRightInvariant.map_add_right_eq_self {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [self : μ.IsAddRightInvariant] (g : G) :
        MeasureTheory.Measure.map (fun (x : G) => x + g) μ = μ

        A measure μ on a measurable group is right invariant if the measure of right translations of a set are equal to the measure of the set itself.

        Instances
          theorem MeasureTheory.Measure.IsMulRightInvariant.map_mul_right_eq_self {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [self : μ.IsMulRightInvariant] (g : G) :
          MeasureTheory.Measure.map (fun (x : G) => x * g) μ = μ
          theorem MeasureTheory.map_add_left_eq_self {G : Type u_2} [MeasurableSpace G] [Add G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] (g : G) :
          MeasureTheory.Measure.map (fun (x : G) => g + x) μ = μ
          theorem MeasureTheory.map_mul_left_eq_self {G : Type u_2} [MeasurableSpace G] [Mul G] (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] (g : G) :
          MeasureTheory.Measure.map (fun (x : G) => g * x) μ = μ
          theorem MeasureTheory.map_add_right_eq_self {G : Type u_2} [MeasurableSpace G] [Add G] (μ : MeasureTheory.Measure G) [μ.IsAddRightInvariant] (g : G) :
          MeasureTheory.Measure.map (fun (x : G) => x + g) μ = μ
          theorem MeasureTheory.map_mul_right_eq_self {G : Type u_2} [MeasurableSpace G] [Mul G] (μ : MeasureTheory.Measure G) [μ.IsMulRightInvariant] (g : G) :
          MeasureTheory.Measure.map (fun (x : G) => x * g) μ = μ
          instance MeasureTheory.isAddLeftInvariant_smul {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] (c : ENNReal) :
          (c μ).IsAddLeftInvariant
          Equations
          • =
          instance MeasureTheory.isMulLeftInvariant_smul {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] (c : ENNReal) :
          (c μ).IsMulLeftInvariant
          Equations
          • =
          instance MeasureTheory.isAddRightInvariant_smul {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [μ.IsAddRightInvariant] (c : ENNReal) :
          (c μ).IsAddRightInvariant
          Equations
          • =
          instance MeasureTheory.isMulRightInvariant_smul {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [μ.IsMulRightInvariant] (c : ENNReal) :
          (c μ).IsMulRightInvariant
          Equations
          • =
          instance MeasureTheory.isAddLeftInvariant_smul_nnreal {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] (c : NNReal) :
          (c μ).IsAddLeftInvariant
          Equations
          • =
          instance MeasureTheory.isMulLeftInvariant_smul_nnreal {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] (c : NNReal) :
          (c μ).IsMulLeftInvariant
          Equations
          • =
          instance MeasureTheory.isAddRightInvariant_smul_nnreal {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [μ.IsAddRightInvariant] (c : NNReal) :
          (c μ).IsAddRightInvariant
          Equations
          • =
          instance MeasureTheory.isMulRightInvariant_smul_nnreal {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [μ.IsMulRightInvariant] (c : NNReal) :
          (c μ).IsMulRightInvariant
          Equations
          • =
          theorem MeasureTheory.measurePreserving_add_left {G : Type u_2} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] (g : G) :
          MeasureTheory.MeasurePreserving (fun (x : G) => g + x) μ μ
          theorem MeasureTheory.measurePreserving_mul_left {G : Type u_2} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] (g : G) :
          MeasureTheory.MeasurePreserving (fun (x : G) => g * x) μ μ
          theorem MeasureTheory.MeasurePreserving.add_left {G : Type u_2} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] (g : G) {X : Type u_4} [MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : XG} (hf : MeasureTheory.MeasurePreserving f μ' μ) :
          MeasureTheory.MeasurePreserving (fun (x : X) => g + f x) μ' μ
          theorem MeasureTheory.MeasurePreserving.mul_left {G : Type u_2} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] (g : G) {X : Type u_4} [MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : XG} (hf : MeasureTheory.MeasurePreserving f μ' μ) :
          MeasureTheory.MeasurePreserving (fun (x : X) => g * f x) μ' μ
          theorem MeasureTheory.measurePreserving_add_right {G : Type u_2} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddRightInvariant] (g : G) :
          MeasureTheory.MeasurePreserving (fun (x : G) => x + g) μ μ
          theorem MeasureTheory.measurePreserving_mul_right {G : Type u_2} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [μ.IsMulRightInvariant] (g : G) :
          MeasureTheory.MeasurePreserving (fun (x : G) => x * g) μ μ
          theorem MeasureTheory.MeasurePreserving.add_right {G : Type u_2} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddRightInvariant] (g : G) {X : Type u_4} [MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : XG} (hf : MeasureTheory.MeasurePreserving f μ' μ) :
          MeasureTheory.MeasurePreserving (fun (x : X) => f x + g) μ' μ
          theorem MeasureTheory.MeasurePreserving.mul_right {G : Type u_2} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [μ.IsMulRightInvariant] (g : G) {X : Type u_4} [MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : XG} (hf : MeasureTheory.MeasurePreserving f μ' μ) :
          MeasureTheory.MeasurePreserving (fun (x : X) => f x * g) μ' μ
          theorem MeasureTheory.forall_measure_preimage_add_iff {G : Type u_2} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) :
          (∀ (g : G) (A : Set G), MeasurableSet Aμ ((fun (h : G) => g + h) ⁻¹' A) = μ A) μ.IsAddLeftInvariant

          An alternative way to prove that μ is left invariant under addition.

          theorem MeasureTheory.forall_measure_preimage_mul_iff {G : Type u_2} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G) :
          (∀ (g : G) (A : Set G), MeasurableSet Aμ ((fun (h : G) => g * h) ⁻¹' A) = μ A) μ.IsMulLeftInvariant

          An alternative way to prove that μ is left invariant under multiplication.

          theorem MeasureTheory.forall_measure_preimage_add_right_iff {G : Type u_2} [MeasurableSpace G] [Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) :
          (∀ (g : G) (A : Set G), MeasurableSet Aμ ((fun (h : G) => h + g) ⁻¹' A) = μ A) μ.IsAddRightInvariant

          An alternative way to prove that μ is right invariant under addition.

          theorem MeasureTheory.forall_measure_preimage_mul_right_iff {G : Type u_2} [MeasurableSpace G] [Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G) :
          (∀ (g : G) (A : Set G), MeasurableSet Aμ ((fun (h : G) => h * g) ⁻¹' A) = μ A) μ.IsMulRightInvariant

          An alternative way to prove that μ is right invariant under multiplication.

          instance MeasureTheory.Measure.prod.instIsAddLeftInvariant {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasurableAdd G] [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] {H : Type u_4} [Add H] {mH : MeasurableSpace H} {ν : MeasureTheory.Measure H} [MeasurableAdd H] [ν.IsAddLeftInvariant] [MeasureTheory.SFinite ν] :
          (μ.prod ν).IsAddLeftInvariant
          Equations
          • =
          instance MeasureTheory.Measure.prod.instIsMulLeftInvariant {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [MeasurableMul G] [μ.IsMulLeftInvariant] [MeasureTheory.SFinite μ] {H : Type u_4} [Mul H] {mH : MeasurableSpace H} {ν : MeasureTheory.Measure H} [MeasurableMul H] [ν.IsMulLeftInvariant] [MeasureTheory.SFinite ν] :
          (μ.prod ν).IsMulLeftInvariant
          Equations
          • =
          instance MeasureTheory.Measure.prod.instIsAddRightInvariant {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasurableAdd G] [μ.IsAddRightInvariant] [MeasureTheory.SFinite μ] {H : Type u_4} [Add H] {mH : MeasurableSpace H} {ν : MeasureTheory.Measure H} [MeasurableAdd H] [ν.IsAddRightInvariant] [MeasureTheory.SFinite ν] :
          (μ.prod ν).IsAddRightInvariant
          Equations
          • =
          instance MeasureTheory.Measure.prod.instIsMulRightInvariant {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [MeasurableMul G] [μ.IsMulRightInvariant] [MeasureTheory.SFinite μ] {H : Type u_4} [Mul H] {mH : MeasurableSpace H} {ν : MeasureTheory.Measure H} [MeasurableMul H] [ν.IsMulRightInvariant] [MeasureTheory.SFinite ν] :
          (μ.prod ν).IsMulRightInvariant
          Equations
          • =
          theorem MeasureTheory.isAddLeftInvariant_map {G : Type u_2} [MeasurableSpace G] [Add G] {μ : MeasureTheory.Measure G} [MeasurableAdd G] {H : Type u_4} [MeasurableSpace H] [Add H] [MeasurableAdd H] [μ.IsAddLeftInvariant] (f : AddHom G H) (hf : Measurable f) (h_surj : Function.Surjective f) :
          (MeasureTheory.Measure.map (f) μ).IsAddLeftInvariant
          theorem MeasureTheory.isMulLeftInvariant_map {G : Type u_2} [MeasurableSpace G] [Mul G] {μ : MeasureTheory.Measure G} [MeasurableMul G] {H : Type u_4} [MeasurableSpace H] [Mul H] [MeasurableMul H] [μ.IsMulLeftInvariant] (f : G →ₙ* H) (hf : Measurable f) (h_surj : Function.Surjective f) :
          (MeasureTheory.Measure.map (f) μ).IsMulLeftInvariant
          theorem MeasureTheory.isAddLeftInvariant_map_vadd {G : Type u_2} [MeasurableSpace G] [AddSemigroup G] [MeasurableAdd G] {μ : MeasureTheory.Measure G} {α : Type u_4} [VAdd α G] [VAddCommClass α G G] [MeasurableSpace α] [MeasurableVAdd α G] [μ.IsAddLeftInvariant] (a : α) :
          (MeasureTheory.Measure.map (fun (x : G) => a +ᵥ x) μ).IsAddLeftInvariant

          The image of a left invariant measure under a left additive action is left invariant, assuming that the action preserves addition.

          theorem MeasureTheory.isMulLeftInvariant_map_smul {G : Type u_2} [MeasurableSpace G] [Semigroup G] [MeasurableMul G] {μ : MeasureTheory.Measure G} {α : Type u_4} [SMul α G] [SMulCommClass α G G] [MeasurableSpace α] [MeasurableSMul α G] [μ.IsMulLeftInvariant] (a : α) :
          (MeasureTheory.Measure.map (fun (x : G) => a x) μ).IsMulLeftInvariant

          The image of a left invariant measure under a left action is left invariant, assuming that the action preserves multiplication.

          theorem MeasureTheory.isAddRightInvariant_map_vadd {G : Type u_2} [MeasurableSpace G] [AddSemigroup G] [MeasurableAdd G] {μ : MeasureTheory.Measure G} {α : Type u_4} [VAdd α G] [VAddCommClass α Gᵃᵒᵖ G] [MeasurableSpace α] [MeasurableVAdd α G] [μ.IsAddRightInvariant] (a : α) :
          (MeasureTheory.Measure.map (fun (x : G) => a +ᵥ x) μ).IsAddRightInvariant

          The image of a right invariant measure under a left additive action is right invariant, assuming that the action preserves addition.

          theorem MeasureTheory.isMulRightInvariant_map_smul {G : Type u_2} [MeasurableSpace G] [Semigroup G] [MeasurableMul G] {μ : MeasureTheory.Measure G} {α : Type u_4} [SMul α G] [SMulCommClass α Gᵐᵒᵖ G] [MeasurableSpace α] [MeasurableSMul α G] [μ.IsMulRightInvariant] (a : α) :
          (MeasureTheory.Measure.map (fun (x : G) => a x) μ).IsMulRightInvariant

          The image of a right invariant measure under a left action is right invariant, assuming that the action preserves multiplication.

          instance MeasureTheory.isMulLeftInvariant_map_add_right {G : Type u_2} [MeasurableSpace G] [AddSemigroup G] [MeasurableAdd G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] (g : G) :
          (MeasureTheory.Measure.map (fun (x : G) => x + g) μ).IsAddLeftInvariant

          The image of a left invariant measure under right addition is left invariant.

          Equations
          • =
          instance MeasureTheory.isMulLeftInvariant_map_mul_right {G : Type u_2} [MeasurableSpace G] [Semigroup G] [MeasurableMul G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] (g : G) :
          (MeasureTheory.Measure.map (fun (x : G) => x * g) μ).IsMulLeftInvariant

          The image of a left invariant measure under right multiplication is left invariant.

          Equations
          • =
          instance MeasureTheory.isMulRightInvariant_map_add_left {G : Type u_2} [MeasurableSpace G] [AddSemigroup G] [MeasurableAdd G] {μ : MeasureTheory.Measure G} [μ.IsAddRightInvariant] (g : G) :
          (MeasureTheory.Measure.map (fun (x : G) => g + x) μ).IsAddRightInvariant

          The image of a right invariant measure under left addition is right invariant.

          Equations
          • =
          instance MeasureTheory.isMulRightInvariant_map_mul_left {G : Type u_2} [MeasurableSpace G] [Semigroup G] [MeasurableMul G] {μ : MeasureTheory.Measure G} [μ.IsMulRightInvariant] (g : G) :
          (MeasureTheory.Measure.map (fun (x : G) => g * x) μ).IsMulRightInvariant

          The image of a right invariant measure under left multiplication is right invariant.

          Equations
          • =
          theorem MeasureTheory.map_sub_right_eq_self {G : Type u_2} [MeasurableSpace G] [SubNegMonoid G] (μ : MeasureTheory.Measure G) [μ.IsAddRightInvariant] (g : G) :
          MeasureTheory.Measure.map (fun (x : G) => x - g) μ = μ
          theorem MeasureTheory.map_div_right_eq_self {G : Type u_2} [MeasurableSpace G] [DivInvMonoid G] (μ : MeasureTheory.Measure G) [μ.IsMulRightInvariant] (g : G) :
          MeasureTheory.Measure.map (fun (x : G) => x / g) μ = μ
          theorem MeasureTheory.measurePreserving_sub_right {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddRightInvariant] (g : G) :
          MeasureTheory.MeasurePreserving (fun (x : G) => x - g) μ μ
          theorem MeasureTheory.measurePreserving_div_right {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [μ.IsMulRightInvariant] (g : G) :
          MeasureTheory.MeasurePreserving (fun (x : G) => x / g) μ μ
          @[simp]
          theorem MeasureTheory.measure_preimage_add {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] (g : G) (A : Set G) :
          μ ((fun (h : G) => g + h) ⁻¹' A) = μ A

          We shorten this from measure_preimage_add_left, since left invariant is the preferred option for measures in this formalization.

          @[simp]
          theorem MeasureTheory.measure_preimage_mul {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] (g : G) (A : Set G) :
          μ ((fun (h : G) => g * h) ⁻¹' A) = μ A

          We shorten this from measure_preimage_mul_left, since left invariant is the preferred option for measures in this formalization.

          @[simp]
          theorem MeasureTheory.measure_preimage_add_right {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddRightInvariant] (g : G) (A : Set G) :
          μ ((fun (h : G) => h + g) ⁻¹' A) = μ A
          @[simp]
          theorem MeasureTheory.measure_preimage_mul_right {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [μ.IsMulRightInvariant] (g : G) (A : Set G) :
          μ ((fun (h : G) => h * g) ⁻¹' A) = μ A
          theorem MeasureTheory.map_add_left_ae {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] (x : G) :
          Filter.map (fun (h : G) => x + h) (MeasureTheory.ae μ) = MeasureTheory.ae μ
          theorem MeasureTheory.map_mul_left_ae {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] (x : G) :
          Filter.map (fun (h : G) => x * h) (MeasureTheory.ae μ) = MeasureTheory.ae μ
          theorem MeasureTheory.map_add_right_ae {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddRightInvariant] (x : G) :
          Filter.map (fun (h : G) => h + x) (MeasureTheory.ae μ) = MeasureTheory.ae μ
          theorem MeasureTheory.map_mul_right_ae {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [μ.IsMulRightInvariant] (x : G) :
          Filter.map (fun (h : G) => h * x) (MeasureTheory.ae μ) = MeasureTheory.ae μ
          theorem MeasureTheory.map_sub_right_ae {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddRightInvariant] (x : G) :
          Filter.map (fun (t : G) => t - x) (MeasureTheory.ae μ) = MeasureTheory.ae μ
          theorem MeasureTheory.map_div_right_ae {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [μ.IsMulRightInvariant] (x : G) :
          Filter.map (fun (t : G) => t / x) (MeasureTheory.ae μ) = MeasureTheory.ae μ
          theorem MeasureTheory.eventually_add_left_iff {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] (t : G) {p : GProp} :
          (∀ᵐ (x : G) ∂μ, p (t + x)) ∀ᵐ (x : G) ∂μ, p x
          theorem MeasureTheory.eventually_mul_left_iff {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] (t : G) {p : GProp} :
          (∀ᵐ (x : G) ∂μ, p (t * x)) ∀ᵐ (x : G) ∂μ, p x
          theorem MeasureTheory.eventually_add_right_iff {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddRightInvariant] (t : G) {p : GProp} :
          (∀ᵐ (x : G) ∂μ, p (x + t)) ∀ᵐ (x : G) ∂μ, p x
          theorem MeasureTheory.eventually_mul_right_iff {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [μ.IsMulRightInvariant] (t : G) {p : GProp} :
          (∀ᵐ (x : G) ∂μ, p (x * t)) ∀ᵐ (x : G) ∂μ, p x
          theorem MeasureTheory.eventually_sub_right_iff {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G) [μ.IsAddRightInvariant] (t : G) {p : GProp} :
          (∀ᵐ (x : G) ∂μ, p (x - t)) ∀ᵐ (x : G) ∂μ, p x
          theorem MeasureTheory.eventually_div_right_iff {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G) [μ.IsMulRightInvariant] (t : G) {p : GProp} :
          (∀ᵐ (x : G) ∂μ, p (x / t)) ∀ᵐ (x : G) ∂μ, p x

          The measure A ↦ μ (- A), where - A is the pointwise negation of A.

          Equations
          Instances For

            The measure A ↦ μ (A⁻¹), where A⁻¹ is the pointwise inverse of A.

            Equations
            Instances For

              A measure is invariant under negation if - μ = μ. Equivalently, this means that for all measurable A we have μ (- A) = μ A, where - A is the pointwise negation of A.

              • neg_eq_self : μ.neg = μ
              Instances
                theorem MeasureTheory.Measure.IsNegInvariant.neg_eq_self {G : Type u_2} [MeasurableSpace G] [Neg G] {μ : MeasureTheory.Measure G} [self : μ.IsNegInvariant] :
                μ.neg = μ

                A measure is invariant under inversion if μ⁻¹ = μ. Equivalently, this means that for all measurable A we have μ (A⁻¹) = μ A, where A⁻¹ is the pointwise inverse of A.

                • inv_eq_self : μ.inv = μ
                Instances
                  theorem MeasureTheory.Measure.IsInvInvariant.inv_eq_self {G : Type u_2} [MeasurableSpace G] [Inv G] {μ : MeasureTheory.Measure G} [self : μ.IsInvInvariant] :
                  μ.inv = μ
                  @[simp]
                  theorem MeasureTheory.Measure.neg_eq_self {G : Type u_2} [MeasurableSpace G] [Neg G] (μ : MeasureTheory.Measure G) [μ.IsNegInvariant] :
                  μ.neg = μ
                  @[simp]
                  theorem MeasureTheory.Measure.inv_eq_self {G : Type u_2} [MeasurableSpace G] [Inv G] (μ : MeasureTheory.Measure G) [μ.IsInvInvariant] :
                  μ.inv = μ
                  @[simp]
                  theorem MeasureTheory.Measure.map_neg_eq_self {G : Type u_2} [MeasurableSpace G] [Neg G] (μ : MeasureTheory.Measure G) [μ.IsNegInvariant] :
                  @[simp]
                  theorem MeasureTheory.Measure.map_inv_eq_self {G : Type u_2} [MeasurableSpace G] [Inv G] (μ : MeasureTheory.Measure G) [μ.IsInvInvariant] :
                  @[simp]
                  theorem MeasureTheory.Measure.neg_apply {G : Type u_2} [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) (s : Set G) :
                  μ.neg s = μ (-s)
                  @[simp]
                  @[simp]
                  @[simp]
                  @[simp]
                  theorem MeasureTheory.Measure.measure_neg {G : Type u_2} [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [μ.IsNegInvariant] (A : Set G) :
                  μ (-A) = μ A
                  @[simp]
                  theorem MeasureTheory.Measure.measure_inv {G : Type u_2} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [μ.IsInvInvariant] (A : Set G) :
                  μ A⁻¹ = μ A
                  theorem MeasureTheory.Measure.measure_preimage_neg {G : Type u_2} [MeasurableSpace G] [InvolutiveNeg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [μ.IsNegInvariant] (A : Set G) :
                  μ (Neg.neg ⁻¹' A) = μ A
                  theorem MeasureTheory.Measure.measure_preimage_inv {G : Type u_2} [MeasurableSpace G] [InvolutiveInv G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [μ.IsInvInvariant] (A : Set G) :
                  μ (Inv.inv ⁻¹' A) = μ A
                  instance MeasureTheory.Measure.neg.instIsAddRightInvariant {G : Type u_2} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] :
                  μ.neg.IsAddRightInvariant
                  Equations
                  • =
                  instance MeasureTheory.Measure.inv.instIsMulRightInvariant {G : Type u_2} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] :
                  μ.inv.IsMulRightInvariant
                  Equations
                  • =
                  instance MeasureTheory.Measure.neg.instIsAddLeftInvariant {G : Type u_2} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [μ.IsAddRightInvariant] :
                  μ.neg.IsAddLeftInvariant
                  Equations
                  • =
                  instance MeasureTheory.Measure.inv.instIsMulLeftInvariant {G : Type u_2} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] {μ : MeasureTheory.Measure G} [μ.IsMulRightInvariant] :
                  μ.inv.IsMulLeftInvariant
                  Equations
                  • =
                  theorem MeasureTheory.Measure.measurePreserving_sub_left {G : Type u_2} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [μ.IsNegInvariant] [μ.IsAddLeftInvariant] (g : G) :
                  MeasureTheory.MeasurePreserving (fun (t : G) => g - t) μ μ
                  theorem MeasureTheory.Measure.measurePreserving_div_left {G : Type u_2} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (g : G) :
                  MeasureTheory.MeasurePreserving (fun (t : G) => g / t) μ μ
                  theorem MeasureTheory.Measure.map_sub_left_eq_self {G : Type u_2} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [μ.IsNegInvariant] [μ.IsAddLeftInvariant] (g : G) :
                  MeasureTheory.Measure.map (fun (t : G) => g - t) μ = μ
                  theorem MeasureTheory.Measure.map_div_left_eq_self {G : Type u_2} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (g : G) :
                  MeasureTheory.Measure.map (fun (t : G) => g / t) μ = μ
                  theorem MeasureTheory.Measure.measurePreserving_add_right_neg {G : Type u_2} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [μ.IsNegInvariant] [μ.IsAddLeftInvariant] (g : G) :
                  MeasureTheory.MeasurePreserving (fun (t : G) => -(g + t)) μ μ
                  theorem MeasureTheory.Measure.measurePreserving_mul_right_inv {G : Type u_2} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (g : G) :
                  MeasureTheory.MeasurePreserving (fun (t : G) => (g * t)⁻¹) μ μ
                  theorem MeasureTheory.Measure.map_add_right_neg_eq_self {G : Type u_2} [MeasurableSpace G] [SubtractionMonoid G] [MeasurableAdd G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [μ.IsNegInvariant] [μ.IsAddLeftInvariant] (g : G) :
                  MeasureTheory.Measure.map (fun (t : G) => -(g + t)) μ = μ
                  theorem MeasureTheory.Measure.map_mul_right_inv_eq_self {G : Type u_2} [MeasurableSpace G] [DivisionMonoid G] [MeasurableMul G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [μ.IsInvInvariant] [μ.IsMulLeftInvariant] (g : G) :
                  MeasureTheory.Measure.map (fun (t : G) => (g * t)⁻¹) μ = μ
                  theorem MeasureTheory.Measure.map_sub_left_ae {G : Type u_2} [MeasurableSpace G] [AddGroup G] [MeasurableAdd G] [MeasurableNeg G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] [μ.IsNegInvariant] (x : G) :
                  Filter.map (fun (t : G) => x - t) (MeasureTheory.ae μ) = MeasureTheory.ae μ
                  theorem MeasureTheory.Measure.map_div_left_ae {G : Type u_2} [MeasurableSpace G] [Group G] [MeasurableMul G] [MeasurableInv G] (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] [μ.IsInvInvariant] (x : G) :
                  Filter.map (fun (t : G) => x / t) (MeasureTheory.ae μ) = MeasureTheory.ae μ
                  instance MeasureTheory.Measure.IsOpenPosMeasure.neg {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [ContinuousNeg G] [μ.IsOpenPosMeasure] :
                  μ.neg.IsOpenPosMeasure
                  Equations
                  • =
                  instance MeasureTheory.Measure.IsOpenPosMeasure.inv {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [ContinuousInv G] [μ.IsOpenPosMeasure] :
                  μ.inv.IsOpenPosMeasure
                  Equations
                  • =
                  instance MeasureTheory.Measure.Regular.neg {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [ContinuousNeg G] [μ.Regular] :
                  μ.neg.Regular
                  Equations
                  • =
                  instance MeasureTheory.Measure.Regular.inv {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [ContinuousInv G] [μ.Regular] :
                  μ.inv.Regular
                  Equations
                  • =
                  instance MeasureTheory.Measure.InnerRegular.neg {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [ContinuousNeg G] [μ.InnerRegular] :
                  μ.neg.InnerRegular
                  Equations
                  • =
                  instance MeasureTheory.Measure.InnerRegular.inv {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [ContinuousInv G] [μ.InnerRegular] :
                  μ.inv.InnerRegular
                  Equations
                  • =
                  instance MeasureTheory.innerRegular_map_vadd {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} {α : Type u_4} [AddMonoid α] [AddAction α G] [ContinuousConstVAdd α G] [μ.InnerRegular] (a : α) :
                  (MeasureTheory.Measure.map (fun (x : G) => a +ᵥ x) μ).InnerRegular

                  The image of a inner regular measure under map of a left additive action is again inner regular

                  Equations
                  • =
                  instance MeasureTheory.innerRegular_map_smul {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} {α : Type u_4} [Monoid α] [MulAction α G] [ContinuousConstSMul α G] [μ.InnerRegular] (a : α) :
                  (MeasureTheory.Measure.map (fun (x : G) => a x) μ).InnerRegular

                  The image of an inner regular measure under map of a left action is again inner regular.

                  Equations
                  • =
                  instance MeasureTheory.innerRegular_map_add_left {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [μ.InnerRegular] (g : G) :
                  (MeasureTheory.Measure.map (fun (x : G) => g + x) μ).InnerRegular

                  The image of an inner regular measure under left addition is again inner regular.

                  Equations
                  • =
                  instance MeasureTheory.innerRegular_map_mul_left {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [μ.InnerRegular] (g : G) :
                  (MeasureTheory.Measure.map (fun (x : G) => g * x) μ).InnerRegular

                  The image of an inner regular measure under left multiplication is again inner regular.

                  Equations
                  • =
                  instance MeasureTheory.innerRegular_map_add_right {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [μ.InnerRegular] (g : G) :
                  (MeasureTheory.Measure.map (fun (x : G) => x + g) μ).InnerRegular

                  The image of an inner regular measure under right addition is again inner regular.

                  Equations
                  • =
                  instance MeasureTheory.innerRegular_map_mul_right {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [μ.InnerRegular] (g : G) :
                  (MeasureTheory.Measure.map (fun (x : G) => x * g) μ).InnerRegular

                  The image of an inner regular measure under right multiplication is again inner regular.

                  Equations
                  • =
                  theorem MeasureTheory.innerRegular_neg_iff {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] :
                  μ.neg.InnerRegular μ.InnerRegular
                  theorem MeasureTheory.innerRegular_inv_iff {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] :
                  μ.inv.InnerRegular μ.InnerRegular
                  theorem MeasureTheory.eventually_nhds_zero_measure_vadd_diff_lt {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [LocallyCompactSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G} (hk : IsCompact k) (h'k : IsClosed k) {ε : ENNReal} (hε : ε 0) :
                  ∀ᶠ (g : G) in nhds 0, μ ((g +ᵥ k) \ k) < ε
                  theorem MeasureTheory.eventually_nhds_one_measure_smul_diff_lt {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [LocallyCompactSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G} (hk : IsCompact k) (h'k : IsClosed k) {ε : ENNReal} (hε : ε 0) :
                  ∀ᶠ (g : G) in nhds 1, μ (g k \ k) < ε

                  Continuity of the measure of translates of a compact set: Given a compact set k in a topological group, for g close enough to the origin, μ (g • k \ k) is arbitrarily small.

                  theorem MeasureTheory.tendsto_measure_smul_diff_isCompact_isClosed {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [LocallyCompactSpace G] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G} (hk : IsCompact k) (h'k : IsClosed k) :
                  Filter.Tendsto (fun (g : G) => μ (g k \ k)) (nhds 1) (nhds 0)

                  Continuity of the measure of translates of a compact set: Given a closed compact set k in a topological group, the measure of g • k \ k tends to zero as g tends to 1.

                  theorem MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_compact {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [μ.IsAddLeftInvariant] (K : Set G) (hK : IsCompact K) (h : μ K 0) :
                  μ.IsOpenPosMeasure

                  If a left-invariant measure gives positive mass to a compact set, then it gives positive mass to any open set.

                  theorem MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_compact {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [μ.IsMulLeftInvariant] (K : Set G) (hK : IsCompact K) (h : μ K 0) :
                  μ.IsOpenPosMeasure

                  If a left-invariant measure gives positive mass to a compact set, then it gives positive mass to any open set.

                  @[instance 80]
                  instance MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_regular {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [μ.IsAddLeftInvariant] [μ.Regular] [NeZero μ] :
                  μ.IsOpenPosMeasure

                  A nonzero left-invariant regular measure gives positive mass to any open set.

                  Equations
                  • =
                  abbrev MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_regular.match_1 {G : Type u_1} [MeasurableSpace G] [TopologicalSpace G] {μ : MeasureTheory.Measure G} (motive : (∃ (K : Set G), IsCompact K μ K 0)Prop) :
                  ∀ (x : ∃ (K : Set G), IsCompact K μ K 0), (∀ (K : Set G) (hK : IsCompact K) (h2K : μ K 0), motive )motive x
                  Equations
                  • =
                  Instances For
                    @[instance 80]
                    instance MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_regular {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [μ.IsMulLeftInvariant] [μ.Regular] [NeZero μ] :
                    μ.IsOpenPosMeasure

                    A nonzero left-invariant regular measure gives positive mass to any open set.

                    Equations
                    • =
                    @[instance 80]
                    instance MeasureTheory.isOpenPosMeasure_of_addLeftInvariant_of_innerRegular {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [μ.IsAddLeftInvariant] [μ.InnerRegular] [NeZero μ] :
                    μ.IsOpenPosMeasure

                    A nonzero left-invariant inner regular measure gives positive mass to any open set.

                    Equations
                    • =
                    @[instance 80]
                    instance MeasureTheory.isOpenPosMeasure_of_mulLeftInvariant_of_innerRegular {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [μ.IsMulLeftInvariant] [μ.InnerRegular] [NeZero μ] :
                    μ.IsOpenPosMeasure

                    A nonzero left-invariant inner regular measure gives positive mass to any open set.

                    Equations
                    • =
                    theorem MeasureTheory.null_iff_of_isAddLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [μ.IsAddLeftInvariant] [μ.Regular] {s : Set G} (hs : IsOpen s) :
                    μ s = 0 s = μ = 0
                    theorem MeasureTheory.null_iff_of_isMulLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [μ.IsMulLeftInvariant] [μ.Regular] {s : Set G} (hs : IsOpen s) :
                    μ s = 0 s = μ = 0
                    theorem MeasureTheory.measure_ne_zero_iff_nonempty_of_isAddLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [μ.IsAddLeftInvariant] [μ.Regular] (hμ : μ 0) {s : Set G} (hs : IsOpen s) :
                    μ s 0 s.Nonempty
                    theorem MeasureTheory.measure_ne_zero_iff_nonempty_of_isMulLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [μ.IsMulLeftInvariant] [μ.Regular] (hμ : μ 0) {s : Set G} (hs : IsOpen s) :
                    μ s 0 s.Nonempty
                    theorem MeasureTheory.measure_pos_iff_nonempty_of_isAddLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [μ.IsAddLeftInvariant] [μ.Regular] (h3μ : μ 0) {s : Set G} (hs : IsOpen s) :
                    0 < μ s s.Nonempty
                    theorem MeasureTheory.measure_pos_iff_nonempty_of_isMulLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [μ.IsMulLeftInvariant] [μ.Regular] (h3μ : μ 0) {s : Set G} (hs : IsOpen s) :
                    0 < μ s s.Nonempty
                    theorem MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [μ.IsAddLeftInvariant] (U : Set G) (hU : IsOpen U) (h'U : U.Nonempty) (h : μ U ) {K : Set G} (hK : IsCompact K) :
                    μ K <

                    If a left-invariant measure gives finite mass to a nonempty open set, then it gives finite mass to any compact set.

                    theorem MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [μ.IsMulLeftInvariant] (U : Set G) (hU : IsOpen U) (h'U : U.Nonempty) (h : μ U ) {K : Set G} (hK : IsCompact K) :
                    μ K <

                    If a left-invariant measure gives finite mass to a nonempty open set, then it gives finite mass to any compact set.

                    theorem MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant' {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [μ.IsAddLeftInvariant] {U : Set G} (hU : (interior U).Nonempty) (h : μ U ) {K : Set G} (hK : IsCompact K) :
                    μ K <

                    If a left-invariant measure gives finite mass to a set with nonempty interior, then it gives finite mass to any compact set.

                    theorem MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant' {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [μ.IsMulLeftInvariant] {U : Set G} (hU : (interior U).Nonempty) (h : μ U ) {K : Set G} (hK : IsCompact K) :
                    μ K <

                    If a left-invariant measure gives finite mass to a set with nonempty interior, then it gives finite mass to any compact set.

                    @[simp]
                    theorem MeasureTheory.measure_univ_of_isAddLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] [AddGroup G] [TopologicalAddGroup G] [WeaklyLocallyCompactSpace G] [NoncompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsOpenPosMeasure] [μ.IsAddLeftInvariant] :
                    μ Set.univ =

                    In a noncompact locally compact additive group, a left-invariant measure which is positive on open sets has infinite mass.

                    @[simp]
                    theorem MeasureTheory.measure_univ_of_isMulLeftInvariant {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] [Group G] [TopologicalGroup G] [WeaklyLocallyCompactSpace G] [NoncompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsOpenPosMeasure] [μ.IsMulLeftInvariant] :
                    μ Set.univ =

                    In a noncompact locally compact group, a left-invariant measure which is positive on open sets has infinite mass.

                    @[deprecated IsCompact.closure_subset_measurableSet]
                    @[deprecated IsCompact.closure_subset_measurableSet]

                    If a compact set is included in a measurable set, then so is its closure.

                    @[deprecated IsCompact.measure_closure]
                    @[deprecated IsCompact.measure_closure]
                    abbrev MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_addGroup.match_1 {G : Type u_1} [MeasurableSpace G] {μ : MeasureTheory.Measure G} ⦃s : Set G (motive : MeasurableSet s μ s Prop) :
                    ∀ (h : MeasurableSet s μ s ), (∀ (s_meas : MeasurableSet s) (μs : μ s ), motive )motive h
                    Equations
                    • =
                    Instances For
                      theorem MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_addGroup {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [AddGroup G] [TopologicalAddGroup G] [h : μ.InnerRegularCompactLTTop] :
                      μ.InnerRegularWRT (fun (s : Set G) => IsCompact s IsClosed s) fun (s : Set G) => MeasurableSet s μ s
                      theorem MeasureTheory.innerRegularWRT_isCompact_isClosed_measure_ne_top_of_group {G : Type u_2} [MeasurableSpace G] [TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [Group G] [TopologicalGroup G] [h : μ.InnerRegularCompactLTTop] :
                      μ.InnerRegularWRT (fun (s : Set G) => IsCompact s IsClosed s) fun (s : Set G) => MeasurableSet s μ s
                      @[instance 100]
                      instance MeasureTheory.IsAddLeftInvariant.isAddRightInvariant {G : Type u_2} [MeasurableSpace G] [AddCommSemigroup G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] :
                      μ.IsAddRightInvariant

                      In an abelian additive group every left invariant measure is also right-invariant. We don't declare the converse as an instance, since that would loop type-class inference, and we use IsAddLeftInvariant as the default hypothesis in abelian groups.

                      Equations
                      • =
                      @[instance 100]
                      instance MeasureTheory.IsMulLeftInvariant.isMulRightInvariant {G : Type u_2} [MeasurableSpace G] [CommSemigroup G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] :
                      μ.IsMulRightInvariant

                      In an abelian group every left invariant measure is also right-invariant. We don't declare the converse as an instance, since that would loop type-class inference, and we use IsMulLeftInvariant as the default hypothesis in abelian groups.

                      Equations
                      • =

                      A measure on an additive group is an additive Haar measure if it is left-invariant, and gives finite mass to compact sets and positive mass to open sets.

                      Textbooks generally require an additional regularity assumption to ensure nice behavior on arbitrary locally compact groups. Use [IsAddHaarMeasure μ] [Regular μ] or [IsAddHaarMeasure μ] [InnerRegular μ] in these situations. Note that a Haar measure in our sense is automatically regular and inner regular on second countable locally compact groups, as checked just below this definition.

                        Instances

                          A measure on a group is a Haar measure if it is left-invariant, and gives finite mass to compact sets and positive mass to open sets.

                          Textbooks generally require an additional regularity assumption to ensure nice behavior on arbitrary locally compact groups. Use [IsHaarMeasure μ] [Regular μ] or [IsHaarMeasure μ] [InnerRegular μ] in these situations. Note that a Haar measure in our sense is automatically regular and inner regular on second countable locally compact groups, as checked just below this definition.

                            Instances
                              @[simp]
                              theorem MeasureTheory.Measure.addHaar_singleton {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [TopologicalAddGroup G] [BorelSpace G] (g : G) :
                              μ {g} = μ {0}
                              @[simp]
                              theorem MeasureTheory.Measure.haar_singleton {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [TopologicalGroup G] [BorelSpace G] (g : G) :
                              μ {g} = μ {1}
                              theorem MeasureTheory.Measure.IsAddHaarMeasure.smul {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] {c : ENNReal} (cpos : c 0) (ctop : c ) :
                              (c μ).IsAddHaarMeasure
                              theorem MeasureTheory.Measure.IsHaarMeasure.smul {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] {c : ENNReal} (cpos : c 0) (ctop : c ) :
                              (c μ).IsHaarMeasure
                              theorem MeasureTheory.Measure.isAddHaarMeasure_of_isCompact_nonempty_interior {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] (K : Set G) (hK : IsCompact K) (h'K : (interior K).Nonempty) (h : μ K 0) (h' : μ K ) :
                              μ.IsAddHaarMeasure

                              If a left-invariant measure gives positive mass to some compact set with nonempty interior, then it is an additive Haar measure.

                              theorem MeasureTheory.Measure.isHaarMeasure_of_isCompact_nonempty_interior {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] [TopologicalGroup G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] (K : Set G) (hK : IsCompact K) (h'K : (interior K).Nonempty) (h : μ K 0) (h' : μ K ) :
                              μ.IsHaarMeasure

                              If a left-invariant measure gives positive mass to some compact set with nonempty interior, then it is a Haar measure.

                              theorem MeasureTheory.Measure.isAddHaarMeasure_map {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [BorelSpace G] [TopologicalAddGroup G] {H : Type u_4} [AddGroup H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [T2Space H] [TopologicalAddGroup H] (f : G →+ H) (hf : Continuous f) (h_surj : Function.Surjective f) (h_prop : Filter.Tendsto (f) (Filter.cocompact G) (Filter.cocompact H)) :
                              (MeasureTheory.Measure.map (f) μ).IsAddHaarMeasure

                              The image of an additive Haar measure under a continuous surjective proper additive group homomorphism is again an additive Haar measure. See also AddEquiv.isAddHaarMeasure_map.

                              theorem MeasureTheory.Measure.isHaarMeasure_map {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [BorelSpace G] [TopologicalGroup G] {H : Type u_4} [Group H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [T2Space H] [TopologicalGroup H] (f : G →* H) (hf : Continuous f) (h_surj : Function.Surjective f) (h_prop : Filter.Tendsto (f) (Filter.cocompact G) (Filter.cocompact H)) :
                              (MeasureTheory.Measure.map (f) μ).IsHaarMeasure

                              The image of a Haar measure under a continuous surjective proper group homomorphism is again a Haar measure. See also MulEquiv.isHaarMeasure_map.

                              The image of a finite additive Haar measure under a continuous surjective additive group homomorphism is again an additive Haar measure. See also isAddHaarMeasure_map.

                              The image of a finite Haar measure under a continuous surjective group homomorphism is again a Haar measure. See also isHaarMeasure_map.

                              instance MeasureTheory.Measure.isAddHaarMeasure_map_vadd {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] {α : Type u_4} [BorelSpace G] [TopologicalAddGroup G] [AddGroup α] [AddAction α G] [VAddCommClass α G G] [MeasurableSpace α] [MeasurableVAdd α G] [ContinuousConstVAdd α G] (a : α) :
                              (MeasureTheory.Measure.map (fun (x : G) => a +ᵥ x) μ).IsAddHaarMeasure

                              The image of a Haar measure under map of a left additive action is again a Haar measure

                              Equations
                              • =
                              instance MeasureTheory.Measure.isHaarMeasure_map_smul {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] {α : Type u_4} [BorelSpace G] [TopologicalGroup G] [Group α] [MulAction α G] [SMulCommClass α G G] [MeasurableSpace α] [MeasurableSMul α G] [ContinuousConstSMul α G] (a : α) :
                              (MeasureTheory.Measure.map (fun (x : G) => a x) μ).IsHaarMeasure

                              The image of a Haar measure under map of a left action is again a Haar measure.

                              Equations
                              • =
                              instance MeasureTheory.Measure.isHaarMeasure_map_add_right {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [BorelSpace G] [TopologicalAddGroup G] (g : G) :
                              (MeasureTheory.Measure.map (fun (x : G) => x + g) μ).IsAddHaarMeasure

                              The image of a Haar measure under right addition is again a Haar measure.

                              Equations
                              • =
                              instance MeasureTheory.Measure.isHaarMeasure_map_mul_right {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [BorelSpace G] [TopologicalGroup G] (g : G) :
                              (MeasureTheory.Measure.map (fun (x : G) => x * g) μ).IsHaarMeasure

                              The image of a Haar measure under right multiplication is again a Haar measure.

                              Equations
                              • =
                              theorem AddEquiv.isAddHaarMeasure_map {G : Type u_2} [MeasurableSpace G] [AddGroup G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddHaarMeasure] [BorelSpace G] [TopologicalAddGroup G] {H : Type u_4} [AddGroup H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [TopologicalAddGroup H] (e : G ≃+ H) (he : Continuous e) (hesymm : Continuous e.symm) :
                              (MeasureTheory.Measure.map (e) μ).IsAddHaarMeasure

                              A convenience wrapper for MeasureTheory.Measure.isAddHaarMeasure_map.

                              theorem MulEquiv.isHaarMeasure_map {G : Type u_2} [MeasurableSpace G] [Group G] [TopologicalSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [BorelSpace G] [TopologicalGroup G] {H : Type u_4} [Group H] [TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [TopologicalGroup H] (e : G ≃* H) (he : Continuous e) (hesymm : Continuous e.symm) :
                              (MeasureTheory.Measure.map (e) μ).IsHaarMeasure

                              A convenience wrapper for MeasureTheory.Measure.isHaarMeasure_map.

                              theorem ContinuousLinearEquiv.isAddHaarMeasure_map {E : Type u_4} {F : Type u_5} {R : Type u_6} {S : Type u_7} [Semiring R] [Semiring S] [AddCommGroup E] [Module R E] [AddCommGroup F] [Module S F] [TopologicalSpace E] [TopologicalAddGroup E] [TopologicalSpace F] [TopologicalAddGroup F] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F] (L : E ≃SL[σ] F) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] :
                              (MeasureTheory.Measure.map (L) μ).IsAddHaarMeasure

                              A convenience wrapper for MeasureTheory.Measure.isAddHaarMeasure_map`.

                              @[instance 100]

                              A Haar measure on a σ-compact space is σ-finite.

                              See Note [lower instance priority]

                              Equations
                              • =
                              @[instance 100]

                              A Haar measure on a σ-compact space is σ-finite.

                              See Note [lower instance priority]

                              Equations
                              • =
                              instance MeasureTheory.Measure.prod.instIsAddHaarMeasure {G : Type u_4} [AddGroup G] [TopologicalSpace G] :
                              ∀ {x : MeasurableSpace G} {H : Type u_5} [inst : AddGroup H] [inst_1 : TopologicalSpace H] {x_1 : MeasurableSpace H} (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure H) [inst_2 : μ.IsAddHaarMeasure] [inst_3 : ν.IsAddHaarMeasure] [inst_4 : MeasureTheory.SFinite μ] [inst_5 : MeasureTheory.SFinite ν] [inst_6 : MeasurableAdd G] [inst_7 : MeasurableAdd H], (μ.prod ν).IsAddHaarMeasure
                              Equations
                              • =
                              instance MeasureTheory.Measure.prod.instIsHaarMeasure {G : Type u_4} [Group G] [TopologicalSpace G] :
                              ∀ {x : MeasurableSpace G} {H : Type u_5} [inst : Group H] [inst_1 : TopologicalSpace H] {x_1 : MeasurableSpace H} (μ : MeasureTheory.Measure G) (ν : MeasureTheory.Measure H) [inst_2 : μ.IsHaarMeasure] [inst_3 : ν.IsHaarMeasure] [inst_4 : MeasureTheory.SFinite μ] [inst_5 : MeasureTheory.SFinite ν] [inst_6 : MeasurableMul G] [inst_7 : MeasurableMul H], (μ.prod ν).IsHaarMeasure
                              Equations
                              • =
                              @[instance 100]

                              If the zero element of an additive group is not isolated, then an additive Haar measure on this group has no atoms.

                              This applies in particular to show that an additive Haar measure on a nontrivial finite-dimensional real vector space has no atom.

                              Equations
                              • =
                              @[instance 100]

                              If the neutral element of a group is not isolated, then a Haar measure on this group has no atoms.

                              The additive version of this instance applies in particular to show that an additive Haar measure on a nontrivial finite-dimensional real vector space has no atom.

                              Equations
                              • =