[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f
⊢ (fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0) ∅ = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f
s : ℕ → Set α
hs₁ : ∀ (i : ℕ), MeasurableSet (s i)
hs₂ : Pairwise (Disjoint on s)
⊢ HasSum (fun i => (fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0) (s i))
    ((fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0) (⋃ (i : ℕ), s i))
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f
s : ℕ → Set α
hs₁ : ∀ (i : ℕ), MeasurableSet (s i)
hs₂ : Pairwise (Disjoint on s)
⊢ HasSum (fun i => if MeasurableSet (s i) then ∫ (x : α) in s i, f x ∂μ else 0)
    (if MeasurableSet (⋃ (i : ℕ), s i) then ∫ (x : α) in ⋃ (i : ℕ), s i, f x ∂μ else 0)
[PROOFSTEP]
convert hasSum_integral_iUnion hs₁ hs₂ hf.integrableOn with n
[GOAL]
case h.e'_5.h
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f
s : ℕ → Set α
hs₁ : ∀ (i : ℕ), MeasurableSet (s i)
hs₂ : Pairwise (Disjoint on s)
n : ℕ
⊢ (if MeasurableSet (s n) then ∫ (x : α) in s n, f x ∂μ else 0) = ∫ (a : α) in s n, f a ∂μ
[PROOFSTEP]
rw [if_pos (hs₁ n)]
[GOAL]
case h.e'_6
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f
s : ℕ → Set α
hs₁ : ∀ (i : ℕ), MeasurableSet (s i)
hs₂ : Pairwise (Disjoint on s)
⊢ (if MeasurableSet (⋃ (i : ℕ), s i) then ∫ (x : α) in ⋃ (i : ℕ), s i, f x ∂μ else 0) =
    ∫ (a : α) in ⋃ (n : ℕ), s n, f a ∂μ
[PROOFSTEP]
rw [if_pos (MeasurableSet.iUnion hs₁)]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
s : Set α
hs : MeasurableSet s
⊢ ↑(withDensityᵥ μ f) s = ∫ (x : α) in s, f x ∂μ
[PROOFSTEP]
rw [withDensityᵥ, dif_pos hf]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
s : Set α
hs : MeasurableSet s
⊢ ↑{ measureOf' := fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0,
          empty' := (_ : (if MeasurableSet ∅ then ∫ (x : α) in ∅, f x ∂μ else 0) = 0),
          not_measurable' :=
            (_ : ∀ (s : Set α), ¬MeasurableSet s → (if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0) = 0),
          m_iUnion' :=
            (_ :
              ∀ (s : ℕ → Set α),
                (∀ (i : ℕ), MeasurableSet (s i)) →
                  Pairwise (Disjoint on s) →
                    HasSum (fun i => (fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0) (s i))
                      ((fun s => if MeasurableSet s then ∫ (x : α) in s, f x ∂μ else 0) (⋃ (i : ℕ), s i))) }
      s =
    ∫ (x : α) in s, f x ∂μ
[PROOFSTEP]
exact dif_pos hs
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
⊢ withDensityᵥ μ 0 = 0
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
s : Set α
hs : MeasurableSet s
⊢ ↑(withDensityᵥ μ 0) s = ↑0 s
[PROOFSTEP]
erw [withDensityᵥ_apply (integrable_zero α E μ) hs]
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, 0 ∂μ = ↑0 s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
⊢ withDensityᵥ μ (-f) = -withDensityᵥ μ f
[PROOFSTEP]
by_cases hf : Integrable f μ
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
⊢ withDensityᵥ μ (-f) = -withDensityᵥ μ f
[PROOFSTEP]
ext1 i hi
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ (-f)) i = ↑(-withDensityᵥ μ f) i
[PROOFSTEP]
rw [VectorMeasure.neg_apply, withDensityᵥ_apply hf hi, ← integral_neg, withDensityᵥ_apply hf.neg hi]
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, (-f) x ∂μ = ∫ (a : α) in i, -f a ∂μ
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : ¬Integrable f
⊢ withDensityᵥ μ (-f) = -withDensityᵥ μ f
[PROOFSTEP]
rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg, neg_zero]
[GOAL]
case neg.hnc
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : ¬Integrable f
⊢ ¬Integrable (-f)
[PROOFSTEP]
rwa [integrable_neg_iff]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
⊢ withDensityᵥ μ (f + g) = withDensityᵥ μ f + withDensityᵥ μ g
[PROOFSTEP]
ext1 i hi
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ (f + g)) i = ↑(withDensityᵥ μ f + withDensityᵥ μ g) i
[PROOFSTEP]
rw [withDensityᵥ_apply (hf.add hg) hi, VectorMeasure.add_apply, withDensityᵥ_apply hf hi, withDensityᵥ_apply hg hi]
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, (f + g) x ∂μ = ∫ (x : α) in i, f x ∂μ + ∫ (x : α) in i, g x ∂μ
[PROOFSTEP]
simp_rw [Pi.add_apply]
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, f x + g x ∂μ = ∫ (x : α) in i, f x ∂μ + ∫ (x : α) in i, g x ∂μ
[PROOFSTEP]
rw [integral_add]
[GOAL]
case h.hf
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ Integrable fun x => f x
[PROOFSTEP]
rw [← integrableOn_univ]
[GOAL]
case h.hg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ Integrable fun x => g x
[PROOFSTEP]
rw [← integrableOn_univ]
[GOAL]
case h.hf
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ IntegrableOn (fun x => f x) Set.univ
[PROOFSTEP]
exact hf.integrableOn.restrict MeasurableSet.univ
[GOAL]
case h.hg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
i : Set α
hi : MeasurableSet i
⊢ IntegrableOn (fun x => g x) Set.univ
[PROOFSTEP]
exact hg.integrableOn.restrict MeasurableSet.univ
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
hf : Integrable f
hg : Integrable g
⊢ withDensityᵥ μ (f - g) = withDensityᵥ μ f - withDensityᵥ μ g
[PROOFSTEP]
rw [sub_eq_add_neg, sub_eq_add_neg, withDensityᵥ_add hf hg.neg, withDensityᵥ_neg]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_4
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
⊢ withDensityᵥ μ (r • f) = r • withDensityᵥ μ f
[PROOFSTEP]
by_cases hf : Integrable f μ
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_4
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : Integrable f
⊢ withDensityᵥ μ (r • f) = r • withDensityᵥ μ f
[PROOFSTEP]
ext1 i hi
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_4
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ (r • f)) i = ↑(r • withDensityᵥ μ f) i
[PROOFSTEP]
rw [withDensityᵥ_apply (hf.smul r) hi, VectorMeasure.smul_apply, withDensityᵥ_apply hf hi, ← integral_smul r f]
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_4
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, (r • f) x ∂μ = ∫ (a : α) in i, r • f a ∂μ
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_4
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f
⊢ withDensityᵥ μ (r • f) = r • withDensityᵥ μ f
[PROOFSTEP]
by_cases hr : r = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_4
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f
hr : r = 0
⊢ withDensityᵥ μ (r • f) = r • withDensityᵥ μ f
[PROOFSTEP]
rw [hr, zero_smul, zero_smul, withDensityᵥ_zero]
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_4
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f
hr : ¬r = 0
⊢ withDensityᵥ μ (r • f) = r • withDensityᵥ μ f
[PROOFSTEP]
rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg, smul_zero]
[GOAL]
case neg.hnc
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
f✝ g : α → E
𝕜 : Type u_4
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : SMulCommClass ℝ 𝕜 E
f : α → E
r : 𝕜
hf : ¬Integrable f
hr : ¬r = 0
⊢ ¬Integrable (r • f)
[PROOFSTEP]
rwa [integrable_smul_iff hr f]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
⊢ withDensityᵥ μ f ≪ᵥ toENNRealVectorMeasure μ
[PROOFSTEP]
by_cases hf : Integrable f μ
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
hf : Integrable f
⊢ withDensityᵥ μ f ≪ᵥ toENNRealVectorMeasure μ
[PROOFSTEP]
refine' VectorMeasure.AbsolutelyContinuous.mk fun i hi₁ hi₂ => _
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
hf : Integrable f
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑(toENNRealVectorMeasure μ) i = 0
⊢ ↑(withDensityᵥ μ f) i = 0
[PROOFSTEP]
rw [toENNRealVectorMeasure_apply_measurable hi₁] at hi₂
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
hf : Integrable f
i : Set α
hi₁ : MeasurableSet i
hi₂ : ↑↑μ i = 0
⊢ ↑(withDensityᵥ μ f) i = 0
[PROOFSTEP]
rw [withDensityᵥ_apply hf hi₁, Measure.restrict_zero_set hi₂, integral_zero_measure]
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
hf : ¬Integrable f
⊢ withDensityᵥ μ f ≪ᵥ toENNRealVectorMeasure μ
[PROOFSTEP]
rw [withDensityᵥ, dif_neg hf]
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
μ : Measure α
f : α → ℝ
hf : ¬Integrable f
⊢ 0 ≪ᵥ toENNRealVectorMeasure μ
[PROOFSTEP]
exact VectorMeasure.AbsolutelyContinuous.zero _
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
hf : Integrable f
hg : Integrable g
hfg : withDensityᵥ μ f = withDensityᵥ μ g
⊢ f =ᶠ[ae μ] g
[PROOFSTEP]
refine' hf.ae_eq_of_forall_set_integral_eq f g hg fun i hi _ => _
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
hf : Integrable f
hg : Integrable g
hfg : withDensityᵥ μ f = withDensityᵥ μ g
i : Set α
hi : MeasurableSet i
x✝ : ↑↑μ i < ⊤
⊢ ∫ (x : α) in i, f x ∂μ = ∫ (x : α) in i, g x ∂μ
[PROOFSTEP]
rw [← withDensityᵥ_apply hf hi, hfg, withDensityᵥ_apply hg hi]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
⊢ withDensityᵥ μ f = withDensityᵥ μ g
[PROOFSTEP]
by_cases hf : Integrable f μ
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f
⊢ withDensityᵥ μ f = withDensityᵥ μ g
[PROOFSTEP]
ext i hi
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ f) i = ↑(withDensityᵥ μ g) i
[PROOFSTEP]
rw [withDensityᵥ_apply hf hi, withDensityᵥ_apply (hf.congr h) hi]
[GOAL]
case pos.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, f x ∂μ = ∫ (x : α) in i, g x ∂μ
[PROOFSTEP]
exact integral_congr_ae (ae_restrict_of_ae h)
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f
⊢ withDensityᵥ μ f = withDensityᵥ μ g
[PROOFSTEP]
have hg : ¬Integrable g μ := by intro hg; exact hf (hg.congr h.symm)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f
⊢ ¬Integrable g
[PROOFSTEP]
intro hg
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f
hg : Integrable g
⊢ False
[PROOFSTEP]
exact hf (hg.congr h.symm)
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g✝ f g : α → E
h : f =ᶠ[ae μ] g
hf : ¬Integrable f
hg : ¬Integrable g
⊢ withDensityᵥ μ f = withDensityᵥ μ g
[PROOFSTEP]
rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg hg]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
⊢ (withDensityᵥ μ fun x => ENNReal.toReal (f x)) = toSignedMeasure (withDensity μ f)
[PROOFSTEP]
have hfi := integrable_toReal_of_lintegral_ne_top hfm hf
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
⊢ (withDensityᵥ μ fun x => ENNReal.toReal (f x)) = toSignedMeasure (withDensity μ f)
[PROOFSTEP]
haveI := isFiniteMeasure_withDensity hf
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
⊢ (withDensityᵥ μ fun x => ENNReal.toReal (f x)) = toSignedMeasure (withDensity μ f)
[PROOFSTEP]
ext i hi
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ fun x => ENNReal.toReal (f x)) i = ↑(toSignedMeasure (withDensity μ f)) i
[PROOFSTEP]
rw [withDensityᵥ_apply hfi hi, toSignedMeasure_apply_measurable hi, withDensity_apply _ hi,
  integral_toReal hfm.restrict]
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
hi : MeasurableSet i
⊢ ∀ᵐ (x : α) ∂restrict μ i, f x < ⊤
[PROOFSTEP]
refine' ae_lt_top' hfm.restrict (ne_top_of_le_ne_top hf _)
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
[PROOFSTEP]
conv_rhs => rw [← set_lintegral_univ]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
hi : MeasurableSet i
| ∫⁻ (x : α), f x ∂μ
[PROOFSTEP]
rw [← set_lintegral_univ]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
hi : MeasurableSet i
| ∫⁻ (x : α), f x ∂μ
[PROOFSTEP]
rw [← set_lintegral_univ]
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
hi : MeasurableSet i
| ∫⁻ (x : α), f x ∂μ
[PROOFSTEP]
rw [← set_lintegral_univ]
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ≥0∞
hfm : AEMeasurable f
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hfi : Integrable fun x => ENNReal.toReal (f x)
this : IsFiniteMeasure (withDensity μ fun a => f a)
i : Set α
hi : MeasurableSet i
⊢ ∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α) in Set.univ, f x ∂μ
[PROOFSTEP]
exact lintegral_mono_set (Set.subset_univ _)
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ
hfi : Integrable f
⊢ withDensityᵥ μ f =
    toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (f x)) -
      toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (-f x))
[PROOFSTEP]
haveI := isFiniteMeasure_withDensity_ofReal hfi.2
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ
hfi : Integrable f
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
⊢ withDensityᵥ μ f =
    toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (f x)) -
      toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (-f x))
[PROOFSTEP]
haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.2
[GOAL]
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ
hfi : Integrable f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
⊢ withDensityᵥ μ f =
    toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (f x)) -
      toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (-f x))
[PROOFSTEP]
ext i hi
[GOAL]
case h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
f : α → ℝ
hfi : Integrable f
this✝ : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal (f x))
this : IsFiniteMeasure (withDensity μ fun x => ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ ↑(withDensityᵥ μ f) i =
    ↑(toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (f x)) -
          toSignedMeasure (withDensity μ fun x => ENNReal.ofReal (-f x)))
      i
[PROOFSTEP]
rw [withDensityᵥ_apply hfi hi, integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi.integrableOn,
  VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi,
  withDensity_apply _ hi, withDensity_apply _ hi]
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f✝ g : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ
hf : Integrable f
i : Set α
hi : MeasurableSet i
⊢ ↑(VectorMeasure.trim (withDensityᵥ μ f) hm) i = ∫ (x : α) in i, f x ∂μ
[PROOFSTEP]
rw [VectorMeasure.trim_measurableSet_eq hm hi, withDensityᵥ_apply hf (hm _ hi)]
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f
⊢ VectorMeasure.trim (withDensityᵥ μ f) hm ≪ᵥ toENNRealVectorMeasure (Measure.trim μ hm)
[PROOFSTEP]
refine' VectorMeasure.AbsolutelyContinuous.mk fun j hj₁ hj₂ => _
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f
j : Set α
hj₁ : MeasurableSet j
hj₂ : ↑(toENNRealVectorMeasure (Measure.trim μ hm)) j = 0
⊢ ↑(VectorMeasure.trim (withDensityᵥ μ f) hm) j = 0
[PROOFSTEP]
rw [Measure.toENNRealVectorMeasure_apply_measurable hj₁, trim_measurableSet_eq hm hj₁] at hj₂
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f
j : Set α
hj₁ : MeasurableSet j
hj₂ : ↑↑μ j = 0
⊢ ↑(VectorMeasure.trim (withDensityᵥ μ f) hm) j = 0
[PROOFSTEP]
rw [VectorMeasure.trim_measurableSet_eq hm hj₁, withDensityᵥ_apply hfi (hm _ hj₁)]
[GOAL]
α : Type u_1
β : Type u_2
m✝ : MeasurableSpace α
μ✝ ν : Measure α
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : α → E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hfi : Integrable f
j : Set α
hj₁ : MeasurableSet j
hj₂ : ↑↑μ j = 0
⊢ ∫ (x : α) in j, f x ∂μ = 0
[PROOFSTEP]
simp only [Measure.restrict_eq_zero.mpr hj₂, integral_zero_measure]


[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
⊢ ↑↑(map QuotientGroup.mk (Measure.restrict μ 𝓕)) ((fun x => g • x) ⁻¹' A) =
    ↑↑(map QuotientGroup.mk (Measure.restrict μ 𝓕)) A
[PROOFSTEP]
let π : G → G ⧸ Γ := QuotientGroup.mk
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
⊢ ↑↑(map QuotientGroup.mk (Measure.restrict μ 𝓕)) ((fun x => g • x) ⁻¹' A) =
    ↑↑(map QuotientGroup.mk (Measure.restrict μ 𝓕)) A
[PROOFSTEP]
have meas_π : Measurable π := continuous_quotient_mk'.measurable
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
⊢ ↑↑(map QuotientGroup.mk (Measure.restrict μ 𝓕)) ((fun x => g • x) ⁻¹' A) =
    ↑↑(map QuotientGroup.mk (Measure.restrict μ 𝓕)) A
[PROOFSTEP]
have 𝓕meas : NullMeasurableSet 𝓕 μ := h𝓕.nullMeasurableSet
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
⊢ ↑↑(map QuotientGroup.mk (Measure.restrict μ 𝓕)) ((fun x => g • x) ⁻¹' A) =
    ↑↑(map QuotientGroup.mk (Measure.restrict μ 𝓕)) A
[PROOFSTEP]
have meas_πA : MeasurableSet (π ⁻¹' A) := measurableSet_preimage meas_π hA
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
meas_πA : MeasurableSet (π ⁻¹' A)
⊢ ↑↑(map QuotientGroup.mk (Measure.restrict μ 𝓕)) ((fun x => g • x) ⁻¹' A) =
    ↑↑(map QuotientGroup.mk (Measure.restrict μ 𝓕)) A
[PROOFSTEP]
rw [Measure.map_apply meas_π hA, Measure.map_apply meas_π (measurableSet_preimage (measurable_const_smul g) hA),
  Measure.restrict_apply₀' 𝓕meas, Measure.restrict_apply₀' 𝓕meas]
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
meas_πA : MeasurableSet (π ⁻¹' A)
⊢ ↑↑μ (π ⁻¹' ((fun x x_1 => x • x_1) g ⁻¹' A) ∩ 𝓕) = ↑↑μ (π ⁻¹' A ∩ 𝓕)
[PROOFSTEP]
set π_preA := π ⁻¹' A
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
⊢ ↑↑μ (π ⁻¹' ((fun x x_1 => x • x_1) g ⁻¹' A) ∩ 𝓕) = ↑↑μ (π_preA ∩ 𝓕)
[PROOFSTEP]
have : π ⁻¹' ((fun x : G ⧸ Γ => g • x) ⁻¹' A) = (g * ·) ⁻¹' π_preA := by ext1; simp
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
⊢ π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
[PROOFSTEP]
ext1
[GOAL]
case h
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
x✝ : G
⊢ x✝ ∈ π ⁻¹' ((fun x => g • x) ⁻¹' A) ↔ x✝ ∈ (fun x => g * x) ⁻¹' π_preA
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
⊢ ↑↑μ (π ⁻¹' ((fun x x_1 => x • x_1) g ⁻¹' A) ∩ 𝓕) = ↑↑μ (π_preA ∩ 𝓕)
[PROOFSTEP]
rw [this]
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
⊢ ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ↑↑μ (π_preA ∩ 𝓕)
[PROOFSTEP]
have : μ ((g * ·) ⁻¹' π_preA ∩ 𝓕) = μ (π_preA ∩ (g⁻¹ * ·) ⁻¹' 𝓕) :=
  by
  trans μ ((g * ·) ⁻¹' (π_preA ∩ (g⁻¹ * ·) ⁻¹' 𝓕))
  · rw [preimage_inter]
    congr 2
    simp [Set.preimage]
  rw [measure_preimage_mul]
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
⊢ ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)
[PROOFSTEP]
trans μ ((g * ·) ⁻¹' (π_preA ∩ (g⁻¹ * ·) ⁻¹' 𝓕))
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
⊢ ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ↑↑μ ((fun x => g * x) ⁻¹' (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕))
[PROOFSTEP]
rw [preimage_inter]
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
⊢ ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) =
    ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ (fun x => g * x) ⁻¹' ((fun x => g⁻¹ * x) ⁻¹' 𝓕))
[PROOFSTEP]
congr 2
[GOAL]
case e_a.e_a
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
⊢ 𝓕 = (fun x => g * x) ⁻¹' ((fun x => g⁻¹ * x) ⁻¹' 𝓕)
[PROOFSTEP]
simp [Set.preimage]
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
⊢ ↑↑μ ((fun x => g * x) ⁻¹' (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)) = ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)
[PROOFSTEP]
rw [measure_preimage_mul]
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this✝ : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
this : ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)
⊢ ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ↑↑μ (π_preA ∩ 𝓕)
[PROOFSTEP]
rw [this]
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this✝ : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
this : ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)
⊢ ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕) = ↑↑μ (π_preA ∩ 𝓕)
[PROOFSTEP]
have h𝓕_translate_fundom : IsFundamentalDomain (Subgroup.opposite Γ) (g • 𝓕) μ := h𝓕.smul_of_comm g
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this✝ : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
this : ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)
h𝓕_translate_fundom : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } (g • 𝓕)
⊢ ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕) = ↑↑μ (π_preA ∩ 𝓕)
[PROOFSTEP]
rw [h𝓕.measure_set_eq h𝓕_translate_fundom meas_πA, ← preimage_smul_inv]
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this✝ : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
this : ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)
h𝓕_translate_fundom : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } (g • 𝓕)
⊢ ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕) = ↑↑μ (π_preA ∩ (fun x => g⁻¹ • x) ⁻¹' 𝓕)
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this✝ : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
this : ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)
h𝓕_translate_fundom : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } (g • 𝓕)
⊢ ∀ (g : { x // x ∈ ↑Subgroup.opposite Γ }), (fun x => g • x) ⁻¹' π_preA = π_preA
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this✝ : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
this : ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)
h𝓕_translate_fundom : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } (g • 𝓕)
⊢ ∀ (g : { x // x ∈ ↑Subgroup.opposite Γ }), (fun x => g • x) ⁻¹' π_preA = π_preA
[PROOFSTEP]
rintro ⟨γ, γ_in_Γ⟩
[GOAL]
case mk
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this✝ : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
this : ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)
h𝓕_translate_fundom : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } (g • 𝓕)
γ : Gᵐᵒᵖ
γ_in_Γ : γ ∈ ↑Subgroup.opposite Γ
⊢ (fun x => { val := γ, property := γ_in_Γ } • x) ⁻¹' π_preA = π_preA
[PROOFSTEP]
ext x
[GOAL]
case mk.h
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this✝ : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
this : ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)
h𝓕_translate_fundom : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } (g • 𝓕)
γ : Gᵐᵒᵖ
γ_in_Γ : γ ∈ ↑Subgroup.opposite Γ
x : G
⊢ x ∈ (fun x => { val := γ, property := γ_in_Γ } • x) ⁻¹' π_preA ↔ x ∈ π_preA
[PROOFSTEP]
have : π (x * MulOpposite.unop γ) = π x := by simpa [QuotientGroup.eq'] using γ_in_Γ
[GOAL]
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this✝ : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
this : ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)
h𝓕_translate_fundom : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } (g • 𝓕)
γ : Gᵐᵒᵖ
γ_in_Γ : γ ∈ ↑Subgroup.opposite Γ
x : G
⊢ π (x * MulOpposite.unop γ) = π x
[PROOFSTEP]
simpa [QuotientGroup.eq'] using γ_in_Γ
[GOAL]
case mk.h
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this✝¹ : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
this✝ : ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)
h𝓕_translate_fundom : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } (g • 𝓕)
γ : Gᵐᵒᵖ
γ_in_Γ : γ ∈ ↑Subgroup.opposite Γ
x : G
this : π (x * MulOpposite.unop γ) = π x
⊢ x ∈ (fun x => { val := γ, property := γ_in_Γ } • x) ⁻¹' π_preA ↔ x ∈ π_preA
[PROOFSTEP]
simp only [(· • ·), ← this, mem_preimage]
[GOAL]
case mk.h
G : Type u_1
inst✝⁹ : Group G
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalGroup G
inst✝⁵ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁴ : Countable { x // x ∈ Γ }
inst✝³ : MeasurableSpace (G ⧸ Γ)
inst✝² : BorelSpace (G ⧸ Γ)
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
π : G → G ⧸ Γ := QuotientGroup.mk
meas_π : Measurable π
𝓕meas : NullMeasurableSet 𝓕
π_preA : Set G := π ⁻¹' A
meas_πA : MeasurableSet π_preA
this✝¹ : π ⁻¹' ((fun x => g • x) ⁻¹' A) = (fun x => g * x) ⁻¹' π_preA
this✝ : ↑↑μ ((fun x => g * x) ⁻¹' π_preA ∩ 𝓕) = ↑↑μ (π_preA ∩ (fun x => g⁻¹ * x) ⁻¹' 𝓕)
h𝓕_translate_fundom : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } (g • 𝓕)
γ : Gᵐᵒᵖ
γ_in_Γ : γ ∈ ↑Subgroup.opposite Γ
x : G
this : π (x * MulOpposite.unop γ) = π x
⊢ ↑(SMul.smul { val := γ, property := γ_in_Γ } x) ∈ A ↔ ↑(x * MulOpposite.unop γ) ∈ A
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁵ : Countable { x // x ∈ Γ }
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
x : G ⧸ Γ
⊢ map (fun x_1 => x * x_1) (map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕)) =
    map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕)
[PROOFSTEP]
apply Measure.ext
[GOAL]
case h
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁵ : Countable { x // x ∈ Γ }
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
x : G ⧸ Γ
⊢ ∀ (s : Set (G ⧸ Γ)),
    MeasurableSet s →
      ↑↑(map (fun x_1 => x * x_1) (map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕))) s =
        ↑↑(map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕)) s
[PROOFSTEP]
intro A hA
[GOAL]
case h
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁵ : Countable { x // x ∈ Γ }
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
⊢ ↑↑(map (fun x_1 => x * x_1) (map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕))) A =
    ↑↑(map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕)) A
[PROOFSTEP]
obtain ⟨x₁, h⟩ := @Quotient.exists_rep _ (QuotientGroup.leftRel Γ) x
[GOAL]
case h.intro
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁵ : Countable { x // x ∈ Γ }
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : Quotient.mk (QuotientGroup.leftRel Γ) x₁ = x
⊢ ↑↑(map (fun x_1 => x * x_1) (map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕))) A =
    ↑↑(map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕)) A
[PROOFSTEP]
haveI := h𝓕.smulInvariantMeasure_map
[GOAL]
case h.intro
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁵ : Countable { x // x ∈ Γ }
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : Quotient.mk (QuotientGroup.leftRel Γ) x₁ = x
this : SMulInvariantMeasure G (G ⧸ Γ) (map QuotientGroup.mk (Measure.restrict μ 𝓕))
⊢ ↑↑(map (fun x_1 => x * x_1) (map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕))) A =
    ↑↑(map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕)) A
[PROOFSTEP]
convert measure_preimage_smul x₁ ((Measure.map QuotientGroup.mk) (μ.restrict 𝓕)) A using 1
[GOAL]
case h.e'_2
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁵ : Countable { x // x ∈ Γ }
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : Quotient.mk (QuotientGroup.leftRel Γ) x₁ = x
this : SMulInvariantMeasure G (G ⧸ Γ) (map QuotientGroup.mk (Measure.restrict μ 𝓕))
⊢ ↑↑(map (fun x_1 => x * x_1) (map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕))) A =
    ↑↑(map QuotientGroup.mk (Measure.restrict μ 𝓕)) ((fun x => x₁ • x) ⁻¹' A)
[PROOFSTEP]
rw [← h, Measure.map_apply]
[GOAL]
case h.e'_2
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁵ : Countable { x // x ∈ Γ }
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : Quotient.mk (QuotientGroup.leftRel Γ) x₁ = x
this : SMulInvariantMeasure G (G ⧸ Γ) (map QuotientGroup.mk (Measure.restrict μ 𝓕))
⊢ ↑↑(map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕))
      ((fun x => Quotient.mk (QuotientGroup.leftRel Γ) x₁ * x) ⁻¹' A) =
    ↑↑(map QuotientGroup.mk (Measure.restrict μ 𝓕)) ((fun x => x₁ • x) ⁻¹' A)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2.hf
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁵ : Countable { x // x ∈ Γ }
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : Quotient.mk (QuotientGroup.leftRel Γ) x₁ = x
this : SMulInvariantMeasure G (G ⧸ Γ) (map QuotientGroup.mk (Measure.restrict μ 𝓕))
⊢ Measurable fun x => Quotient.mk (QuotientGroup.leftRel Γ) x₁ * x
[PROOFSTEP]
exact measurable_const_mul _
[GOAL]
case h.e'_2.hs
G : Type u_1
inst✝¹⁰ : Group G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : TopologicalGroup G
inst✝⁶ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁵ : Countable { x // x ∈ Γ }
inst✝⁴ : MeasurableSpace (G ⧸ Γ)
inst✝³ : BorelSpace (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsMulLeftInvariant μ
inst✝ : IsMulRightInvariant μ
x : G ⧸ Γ
A : Set (G ⧸ Γ)
hA : MeasurableSet A
x₁ : G
h : Quotient.mk (QuotientGroup.leftRel Γ) x₁ = x
this : SMulInvariantMeasure G (G ⧸ Γ) (map QuotientGroup.mk (Measure.restrict μ 𝓕))
⊢ MeasurableSet A
[PROOFSTEP]
exact hA
[GOAL]
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : TopologicalGroup G
inst✝⁸ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁷ : Countable { x // x ∈ Γ }
inst✝⁶ : MeasurableSpace (G ⧸ Γ)
inst✝⁵ : BorelSpace (G ⧸ Γ)
inst✝⁴ : T2Space (G ⧸ Γ)
inst✝³ : SecondCountableTopology (G ⧸ Γ)
K : PositiveCompacts (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsHaarMeasure μ
inst✝ : IsMulRightInvariant μ
h𝓕_finite : ↑↑μ 𝓕 < ⊤
⊢ map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕) = ↑↑μ (𝓕 ∩ ↑(QuotientGroup.mk' Γ) ⁻¹' ↑K) • haarMeasure K
[PROOFSTEP]
let π : G →* G ⧸ Γ := QuotientGroup.mk' Γ
[GOAL]
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : TopologicalGroup G
inst✝⁸ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁷ : Countable { x // x ∈ Γ }
inst✝⁶ : MeasurableSpace (G ⧸ Γ)
inst✝⁵ : BorelSpace (G ⧸ Γ)
inst✝⁴ : T2Space (G ⧸ Γ)
inst✝³ : SecondCountableTopology (G ⧸ Γ)
K : PositiveCompacts (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsHaarMeasure μ
inst✝ : IsMulRightInvariant μ
h𝓕_finite : ↑↑μ 𝓕 < ⊤
π : G →* G ⧸ Γ := QuotientGroup.mk' Γ
⊢ map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕) = ↑↑μ (𝓕 ∩ ↑(QuotientGroup.mk' Γ) ⁻¹' ↑K) • haarMeasure K
[PROOFSTEP]
have meas_π : Measurable π := continuous_quotient_mk'.measurable
[GOAL]
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : TopologicalGroup G
inst✝⁸ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁷ : Countable { x // x ∈ Γ }
inst✝⁶ : MeasurableSpace (G ⧸ Γ)
inst✝⁵ : BorelSpace (G ⧸ Γ)
inst✝⁴ : T2Space (G ⧸ Γ)
inst✝³ : SecondCountableTopology (G ⧸ Γ)
K : PositiveCompacts (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsHaarMeasure μ
inst✝ : IsMulRightInvariant μ
h𝓕_finite : ↑↑μ 𝓕 < ⊤
π : G →* G ⧸ Γ := QuotientGroup.mk' Γ
meas_π : Measurable ↑π
⊢ map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕) = ↑↑μ (𝓕 ∩ ↑(QuotientGroup.mk' Γ) ⁻¹' ↑K) • haarMeasure K
[PROOFSTEP]
have 𝓕meas : NullMeasurableSet 𝓕 μ := h𝓕.nullMeasurableSet
[GOAL]
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : TopologicalGroup G
inst✝⁸ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁷ : Countable { x // x ∈ Γ }
inst✝⁶ : MeasurableSpace (G ⧸ Γ)
inst✝⁵ : BorelSpace (G ⧸ Γ)
inst✝⁴ : T2Space (G ⧸ Γ)
inst✝³ : SecondCountableTopology (G ⧸ Γ)
K : PositiveCompacts (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsHaarMeasure μ
inst✝ : IsMulRightInvariant μ
h𝓕_finite : ↑↑μ 𝓕 < ⊤
π : G →* G ⧸ Γ := QuotientGroup.mk' Γ
meas_π : Measurable ↑π
𝓕meas : NullMeasurableSet 𝓕
⊢ map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕) = ↑↑μ (𝓕 ∩ ↑(QuotientGroup.mk' Γ) ⁻¹' ↑K) • haarMeasure K
[PROOFSTEP]
haveI := Fact.mk h𝓕_finite
[GOAL]
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : TopologicalGroup G
inst✝⁸ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁷ : Countable { x // x ∈ Γ }
inst✝⁶ : MeasurableSpace (G ⧸ Γ)
inst✝⁵ : BorelSpace (G ⧸ Γ)
inst✝⁴ : T2Space (G ⧸ Γ)
inst✝³ : SecondCountableTopology (G ⧸ Γ)
K : PositiveCompacts (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsHaarMeasure μ
inst✝ : IsMulRightInvariant μ
h𝓕_finite : ↑↑μ 𝓕 < ⊤
π : G →* G ⧸ Γ := QuotientGroup.mk' Γ
meas_π : Measurable ↑π
𝓕meas : NullMeasurableSet 𝓕
this : Fact (↑↑μ 𝓕 < ⊤)
⊢ map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕) = ↑↑μ (𝓕 ∩ ↑(QuotientGroup.mk' Γ) ⁻¹' ↑K) • haarMeasure K
[PROOFSTEP]
haveI : (Measure.map (QuotientGroup.mk' Γ) (μ.restrict 𝓕)).IsMulLeftInvariant := h𝓕.isMulLeftInvariant_map
[GOAL]
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : TopologicalGroup G
inst✝⁸ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁷ : Countable { x // x ∈ Γ }
inst✝⁶ : MeasurableSpace (G ⧸ Γ)
inst✝⁵ : BorelSpace (G ⧸ Γ)
inst✝⁴ : T2Space (G ⧸ Γ)
inst✝³ : SecondCountableTopology (G ⧸ Γ)
K : PositiveCompacts (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsHaarMeasure μ
inst✝ : IsMulRightInvariant μ
h𝓕_finite : ↑↑μ 𝓕 < ⊤
π : G →* G ⧸ Γ := QuotientGroup.mk' Γ
meas_π : Measurable ↑π
𝓕meas : NullMeasurableSet 𝓕
this✝ : Fact (↑↑μ 𝓕 < ⊤)
this : IsMulLeftInvariant (map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕))
⊢ map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕) = ↑↑μ (𝓕 ∩ ↑(QuotientGroup.mk' Γ) ⁻¹' ↑K) • haarMeasure K
[PROOFSTEP]
rw [Measure.haarMeasure_unique (Measure.map (QuotientGroup.mk' Γ) (μ.restrict 𝓕)) K, Measure.map_apply meas_π,
  Measure.restrict_apply₀' 𝓕meas, inter_comm]
[GOAL]
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : TopologicalGroup G
inst✝⁸ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁷ : Countable { x // x ∈ Γ }
inst✝⁶ : MeasurableSpace (G ⧸ Γ)
inst✝⁵ : BorelSpace (G ⧸ Γ)
inst✝⁴ : T2Space (G ⧸ Γ)
inst✝³ : SecondCountableTopology (G ⧸ Γ)
K : PositiveCompacts (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsHaarMeasure μ
inst✝ : IsMulRightInvariant μ
h𝓕_finite : ↑↑μ 𝓕 < ⊤
π : G →* G ⧸ Γ := QuotientGroup.mk' Γ
meas_π : Measurable ↑π
𝓕meas : NullMeasurableSet 𝓕
this✝ : Fact (↑↑μ 𝓕 < ⊤)
this : IsMulLeftInvariant (map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕))
⊢ MeasurableSet ↑K
[PROOFSTEP]
exact K.isCompact.measurableSet
[GOAL]
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : TopologicalGroup G
inst✝⁸ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁷ : Countable { x // x ∈ Γ }
inst✝⁶ : MeasurableSpace (G ⧸ Γ)
inst✝⁵ : BorelSpace (G ⧸ Γ)
inst✝⁴ : T2Space (G ⧸ Γ)
inst✝³ : SecondCountableTopology (G ⧸ Γ)
K : PositiveCompacts (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsHaarMeasure μ
inst✝ : IsMulRightInvariant μ
h𝓕_finite : ↑↑μ 𝓕 < ⊤
c : ℝ≥0
h : ↑↑μ (𝓕 ∩ ↑(QuotientGroup.mk' Γ) ⁻¹' ↑K) = ↑c
⊢ map (↑(QuotientGroup.mk' Γ)) (Measure.restrict μ 𝓕) = c • haarMeasure K
[PROOFSTEP]
rw [h𝓕.map_restrict_quotient K h𝓕_finite, h]
[GOAL]
G : Type u_1
inst✝¹² : Group G
inst✝¹¹ : MeasurableSpace G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : TopologicalGroup G
inst✝⁸ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain { x // x ∈ ↑Subgroup.opposite Γ } 𝓕
inst✝⁷ : Countable { x // x ∈ Γ }
inst✝⁶ : MeasurableSpace (G ⧸ Γ)
inst✝⁵ : BorelSpace (G ⧸ Γ)
inst✝⁴ : T2Space (G ⧸ Γ)
inst✝³ : SecondCountableTopology (G ⧸ Γ)
K : PositiveCompacts (G ⧸ Γ)
inst✝² : Subgroup.Normal Γ
inst✝¹ : IsHaarMeasure μ
inst✝ : IsMulRightInvariant μ
h𝓕_finite : ↑↑μ 𝓕 < ⊤
c : ℝ≥0
h : ↑↑μ (𝓕 ∩ ↑(QuotientGroup.mk' Γ) ⁻¹' ↑K) = ↑c
⊢ ↑c • haarMeasure K = c • haarMeasure K
[PROOFSTEP]
rfl


[GOAL]
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : Nontrivial E
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
⊢ NoAtoms μ
[PROOFSTEP]
infer_instance
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
R : ℝ
⊢ ∫ (x : E), f (R • x) ∂μ = |(R ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
[PROOFSTEP]
rcases eq_or_ne R 0 with (rfl | hR)
[GOAL]
case inl
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
⊢ ∫ (x : E), f (0 • x) ∂μ = |(0 ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
[PROOFSTEP]
simp only [zero_smul, integral_const]
[GOAL]
case inl
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
⊢ ENNReal.toReal (↑↑μ univ) • f 0 = |(0 ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
[PROOFSTEP]
rcases Nat.eq_zero_or_pos (finrank ℝ E) with (hE | hE)
[GOAL]
case inl.inl
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
hE : finrank ℝ E = 0
⊢ ENNReal.toReal (↑↑μ univ) • f 0 = |(0 ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
[PROOFSTEP]
have : Subsingleton E := finrank_zero_iff.1 hE
[GOAL]
case inl.inl
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
hE : finrank ℝ E = 0
this : Subsingleton E
⊢ ENNReal.toReal (↑↑μ univ) • f 0 = |(0 ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
[PROOFSTEP]
have : f = fun _ => f 0 := by ext x; rw [Subsingleton.elim x 0]
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
hE : finrank ℝ E = 0
this : Subsingleton E
⊢ f = fun x => f 0
[PROOFSTEP]
ext x
[GOAL]
case h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
hE : finrank ℝ E = 0
this : Subsingleton E
x : E
⊢ f x = f 0
[PROOFSTEP]
rw [Subsingleton.elim x 0]
[GOAL]
case inl.inl
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
hE : finrank ℝ E = 0
this✝ : Subsingleton E
this : f = fun x => f 0
⊢ ENNReal.toReal (↑↑μ univ) • f 0 = |(0 ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
[PROOFSTEP]
conv_rhs => rw [this]
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
hE : finrank ℝ E = 0
this✝ : Subsingleton E
this : f = fun x => f 0
| |(0 ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
[PROOFSTEP]
rw [this]
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
hE : finrank ℝ E = 0
this✝ : Subsingleton E
this : f = fun x => f 0
| |(0 ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
[PROOFSTEP]
rw [this]
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
hE : finrank ℝ E = 0
this✝ : Subsingleton E
this : f = fun x => f 0
| |(0 ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
[PROOFSTEP]
rw [this]
[GOAL]
case inl.inl
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
hE : finrank ℝ E = 0
this✝ : Subsingleton E
this : f = fun x => f 0
⊢ ENNReal.toReal (↑↑μ univ) • f 0 = |(0 ^ finrank ℝ E)⁻¹| • ∫ (x : E), (fun x => f 0) x ∂μ
[PROOFSTEP]
simp only [hE, pow_zero, inv_one, abs_one, one_smul, integral_const]
[GOAL]
case inl.inr
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
hE : finrank ℝ E > 0
⊢ ENNReal.toReal (↑↑μ univ) • f 0 = |(0 ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
[PROOFSTEP]
have : Nontrivial E := finrank_pos_iff.1 hE
[GOAL]
case inl.inr
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
hE : finrank ℝ E > 0
this : Nontrivial E
⊢ ENNReal.toReal (↑↑μ univ) • f 0 = |(0 ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
[PROOFSTEP]
simp only [zero_pow hE, measure_univ_of_isAddLeftInvariant, ENNReal.top_toReal, zero_smul, inv_zero, abs_zero]
[GOAL]
case inr
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
R : ℝ
hR : R ≠ 0
⊢ ∫ (x : E), f (R • x) ∂μ = |(R ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
[PROOFSTEP]
calc
  (∫ x, f (R • x) ∂μ) = ∫ y, f y ∂Measure.map (fun x => R • x) μ :=
    (integral_map_equiv (Homeomorph.smul (isUnit_iff_ne_zero.2 hR).unit).toMeasurableEquiv f).symm
  _ = |(R ^ finrank ℝ E)⁻¹| • ∫ x, f x ∂μ := by
    simp only [map_addHaar_smul μ hR, integral_smul_measure, ENNReal.toReal_ofReal, abs_nonneg]
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
R : ℝ
hR : R ≠ 0
⊢ ∫ (y : E), f y ∂map (fun x => R • x) μ = |(R ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
[PROOFSTEP]
simp only [map_addHaar_smul μ hR, integral_smul_measure, ENNReal.toReal_ofReal, abs_nonneg]
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
R : ℝ
hR : 0 ≤ R
⊢ ∫ (x : E), f (R • x) ∂μ = (R ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
[PROOFSTEP]
rw [integral_comp_smul μ f R, abs_of_nonneg (inv_nonneg.2 (pow_nonneg hR _))]
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
R : ℝ
⊢ ∫ (x : E), f (R⁻¹ • x) ∂μ = |R ^ finrank ℝ E| • ∫ (x : E), f x ∂μ
[PROOFSTEP]
rw [integral_comp_smul μ f R⁻¹, inv_pow, inv_inv]
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
R : ℝ
hR : 0 ≤ R
⊢ ∫ (x : E), f (R⁻¹ • x) ∂μ = R ^ finrank ℝ E • ∫ (x : E), f x ∂μ
[PROOFSTEP]
rw [integral_comp_inv_smul μ f R, abs_of_nonneg (pow_nonneg hR _)]
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
g : ℝ → F
a : ℝ
⊢ ∫ (x : ℝ), g (a * x) = |a⁻¹| • ∫ (y : ℝ), g y
[PROOFSTEP]
simp_rw [← smul_eq_mul, Measure.integral_comp_smul, FiniteDimensional.finrank_self, pow_one]
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
g : ℝ → F
a : ℝ
⊢ ∫ (x : ℝ), g (a⁻¹ * x) = |a| • ∫ (y : ℝ), g y
[PROOFSTEP]
simp_rw [← smul_eq_mul, Measure.integral_comp_inv_smul, FiniteDimensional.finrank_self, pow_one]
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
g : ℝ → F
a : ℝ
⊢ ∫ (x : ℝ), g (x * a) = |a⁻¹| • ∫ (y : ℝ), g y
[PROOFSTEP]
simpa only [mul_comm] using integral_comp_mul_left g a
[GOAL]
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
g : ℝ → F
a : ℝ
⊢ ∫ (x : ℝ), g (x * a⁻¹) = |a| • ∫ (y : ℝ), g y
[PROOFSTEP]
simpa only [mul_comm] using integral_comp_inv_mul_left g a
[GOAL]
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
f : E → F
R : ℝ
hR : R ≠ 0
⊢ (Integrable fun x => f (R • x)) ↔ Integrable f
[PROOFSTEP]
suffices ∀ {g : E → F} (hg : Integrable g μ) {S : ℝ} (hS : S ≠ 0), Integrable (fun x => g (S • x)) μ
  by
  refine' ⟨fun hf => _, fun hf => this hf hR⟩
  convert this hf (inv_ne_zero hR)
  rw [← mul_smul, mul_inv_cancel hR, one_smul]
    -- now prove
[GOAL]
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
f : E → F
R : ℝ
hR : R ≠ 0
this : ∀ {g : E → F}, Integrable g → ∀ {S : ℝ}, S ≠ 0 → Integrable fun x => g (S • x)
⊢ (Integrable fun x => f (R • x)) ↔ Integrable f
[PROOFSTEP]
refine' ⟨fun hf => _, fun hf => this hf hR⟩
[GOAL]
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
f : E → F
R : ℝ
hR : R ≠ 0
this : ∀ {g : E → F}, Integrable g → ∀ {S : ℝ}, S ≠ 0 → Integrable fun x => g (S • x)
hf : Integrable fun x => f (R • x)
⊢ Integrable f
[PROOFSTEP]
convert this hf (inv_ne_zero hR)
[GOAL]
case h.e'_5.h.h.e'_1
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
f : E → F
R : ℝ
hR : R ≠ 0
this : ∀ {g : E → F}, Integrable g → ∀ {S : ℝ}, S ≠ 0 → Integrable fun x => g (S • x)
hf : Integrable fun x => f (R • x)
x✝ : E
⊢ x✝ = R • R⁻¹ • x✝
[PROOFSTEP]
rw [← mul_smul, mul_inv_cancel hR, one_smul]
  -- now prove
[GOAL]
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
f : E → F
R : ℝ
hR : R ≠ 0
⊢ ∀ {g : E → F}, Integrable g → ∀ {S : ℝ}, S ≠ 0 → Integrable fun x => g (S • x)
[PROOFSTEP]
intro g hg S hS
[GOAL]
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g
S : ℝ
hS : S ≠ 0
⊢ Integrable fun x => g (S • x)
[PROOFSTEP]
let t := ((Homeomorph.smul (isUnit_iff_ne_zero.2 hS).unit).toMeasurableEquiv : E ≃ᵐ E)
[GOAL]
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul (IsUnit.unit (_ : IsUnit S)))
⊢ Integrable fun x => g (S • x)
[PROOFSTEP]
refine' (integrable_map_equiv t g).mp (_ : Integrable g (map (S • ·) μ))
[GOAL]
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul (IsUnit.unit (_ : IsUnit S)))
⊢ Integrable g
[PROOFSTEP]
rwa [map_addHaar_smul μ hS, integrable_smul_measure _ ENNReal.ofReal_ne_top]
[GOAL]
F : Type u_1
inst✝⁶ : NormedAddCommGroup F
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul (IsUnit.unit (_ : IsUnit S)))
⊢ ENNReal.ofReal |(S ^ finrank ℝ E)⁻¹| ≠ 0
[PROOFSTEP]
simpa only [Ne.def, ENNReal.ofReal_eq_zero, not_le, abs_pos] using inv_ne_zero (pow_ne_zero _ hS)
[GOAL]
F : Type u_1
inst✝ : NormedAddCommGroup F
g : ℝ → F
R : ℝ
hR : R ≠ 0
⊢ (Integrable fun x => g (R * x)) ↔ Integrable g
[PROOFSTEP]
simpa only [smul_eq_mul] using integrable_comp_smul_iff volume g hR
[GOAL]
F : Type u_1
inst✝ : NormedAddCommGroup F
g : ℝ → F
R : ℝ
hR : R ≠ 0
⊢ (Integrable fun x => g (x * R)) ↔ Integrable g
[PROOFSTEP]
simpa only [mul_comm] using integrable_comp_mul_left_iff g hR