[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ✝ : Measure G
f✝ : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableInv G
f : G → E
μ : Measure G
inst✝ : IsInvInvariant μ
⊢ ∫ (x : G), f x⁻¹ ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
have h : MeasurableEmbedding fun x : G => x⁻¹ := (MeasurableEquiv.inv G).measurableEmbedding
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ✝ : Measure G
f✝ : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableInv G
f : G → E
μ : Measure G
inst✝ : IsInvInvariant μ
h : MeasurableEmbedding fun x => x⁻¹
⊢ ∫ (x : G), f x⁻¹ ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
rw [← h.integral_map, map_inv_eq_self]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulLeftInvariant μ
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (g * x) ∂μ = ∫⁻ (x : G), f x ∂μ
[PROOFSTEP]
convert (lintegral_map_equiv f <| MeasurableEquiv.mulLeft g).symm
[GOAL]
case h.e'_3.h.e'_3
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulLeftInvariant μ
f : G → ℝ≥0∞
g : G
⊢ μ = map (↑(MeasurableEquiv.mulLeft g)) μ
[PROOFSTEP]
simp [map_mul_left_eq_self μ g]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x * g) ∂μ = ∫⁻ (x : G), f x ∂μ
[PROOFSTEP]
convert (lintegral_map_equiv f <| MeasurableEquiv.mulRight g).symm using 1
[GOAL]
case h.e'_3
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f x ∂μ = ∫⁻ (a : G), f a ∂map (↑(MeasurableEquiv.mulRight g)) μ
[PROOFSTEP]
simp [map_mul_right_eq_self μ g]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x / g) ∂μ = ∫⁻ (x : G), f x ∂μ
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
  -- Porting note: was `simp_rw`
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → ℝ≥0∞
g : G
⊢ ∫⁻ (x : G), f (x * g⁻¹) ∂μ = ∫⁻ (x : G), f x ∂μ
[PROOFSTEP]
rw [lintegral_mul_right_eq_self f g⁻¹]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulLeftInvariant μ
f : G → E
g : G
⊢ ∫ (x : G), f (g * x) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
have h_mul : MeasurableEmbedding fun x => g * x := (MeasurableEquiv.mulLeft g).measurableEmbedding
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulLeftInvariant μ
f : G → E
g : G
h_mul : MeasurableEmbedding fun x => g * x
⊢ ∫ (x : G), f (g * x) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
rw [← h_mul.integral_map, map_mul_left_eq_self]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → E
g : G
⊢ ∫ (x : G), f (x * g) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
have h_mul : MeasurableEmbedding fun x => x * g := (MeasurableEquiv.mulRight g).measurableEmbedding
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → E
g : G
h_mul : MeasurableEmbedding fun x => x * g
⊢ ∫ (x : G), f (x * g) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
rw [← h_mul.integral_map, map_mul_right_eq_self]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → E
g : G
⊢ ∫ (x : G), f (x / g) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
  -- Porting note: was `simp_rw`
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
f : G → E
g : G
⊢ ∫ (x : G), f (x * g⁻¹) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
rw [integral_mul_right_eq_self f g⁻¹]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulLeftInvariant μ
hf' : ∀ (x : G), f (g * x) = -f x
⊢ ∫ (x : G), f x ∂μ = 0
[PROOFSTEP]
simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_left_eq_self]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : IsMulRightInvariant μ
hf' : ∀ (x : G), f (x * g) = -f x
⊢ ∫ (x : G), f x ∂μ = 0
[PROOFSTEP]
simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_right_eq_self]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
f : G → F
inst✝ : IsMulRightInvariant μ
hf : Integrable f
g : G
⊢ Integrable fun t => f (t / g)
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
f : G → F
inst✝ : IsMulRightInvariant μ
hf : Integrable f
g : G
⊢ Integrable fun t => f (t * g⁻¹)
[PROOFSTEP]
exact hf.comp_mul_right g⁻¹
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
g : G
⊢ (Integrable fun t => f (g / t)) ↔ Integrable f
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.comp_div_left g⟩
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
g : G
h : Integrable fun t => f (g / t)
⊢ Integrable f
[PROOFSTEP]
convert h.comp_inv.comp_mul_left g⁻¹
[GOAL]
case h.e'_5.h.h.e'_1
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → F
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
g : G
h : Integrable fun t => f (g / t)
x✝ : G
⊢ x✝ = g / (g⁻¹ * x✝)⁻¹
[PROOFSTEP]
simp_rw [div_inv_eq_mul, mul_inv_cancel_left]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ✝ : Measure G
f✝ : G → E
g : G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → E
μ : Measure G
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
x' : G
⊢ ∫ (x : G), f (x' / x) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
simp_rw [div_eq_mul_inv]
  -- Porting note: was `simp_rw`
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ✝ : Measure G
f✝ : G → E
g : G
inst✝⁴ : Group G
inst✝³ : MeasurableMul G
inst✝² : MeasurableInv G
f : G → E
μ : Measure G
inst✝¹ : IsInvInvariant μ
inst✝ : IsMulLeftInvariant μ
x' : G
⊢ ∫ (x : G), f (x' * x⁻¹) ∂μ = ∫ (x : G), f x ∂μ
[PROOFSTEP]
rw [integral_inv_eq_self (fun x => f (x' * x)) μ, integral_mul_left_eq_self f x']
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ✝ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableSpace α
inst✝² : MulAction G α
inst✝¹ : MeasurableSMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
f : α → E
g : G
⊢ ∫ (x : α), f (g • x) ∂μ = ∫ (x : α), f x ∂μ
[PROOFSTEP]
have h : MeasurableEmbedding fun x : α => g • x := (MeasurableEquiv.smul g).measurableEmbedding
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝⁹ : MeasurableSpace G
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NormedAddCommGroup F
μ✝ : Measure G
f✝ : G → E
g✝ : G
inst✝⁴ : Group G
inst✝³ : MeasurableSpace α
inst✝² : MulAction G α
inst✝¹ : MeasurableSMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
f : α → E
g : G
h : MeasurableEmbedding fun x => g • x
⊢ ∫ (x : α), f (g • x) ∂μ = ∫ (x : α), f x ∂μ
[PROOFSTEP]
rw [← h.integral_map, map_smul]
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
inst✝⁶ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g : G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalGroup G
inst✝² : BorelSpace G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : Regular μ
hμ : μ ≠ 0
f : G → ℝ≥0∞
hf : Continuous f
⊢ ∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0
[PROOFSTEP]
haveI := isOpenPosMeasure_of_mulLeftInvariant_of_regular hμ
[GOAL]
𝕜 : Type u_1
M : Type u_2
α : Type u_3
G : Type u_4
E : Type u_5
F : Type u_6
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
inst✝⁶ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g : G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalGroup G
inst✝² : BorelSpace G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : Regular μ
hμ : μ ≠ 0
f : G → ℝ≥0∞
hf : Continuous f
this : IsOpenPosMeasure μ
⊢ ∫⁻ (x : G), f x ∂μ = 0 ↔ f = 0
[PROOFSTEP]
rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero]
