case inl
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
⊢ (∫ (x : E), f (0 • x) ∂μ) = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ

case inr
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
R : ℝ
hR : R ≠ 0
⊢ (∫ (x : E), f (R • x) ∂μ) = abs (R ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
R : ℝ
⊢ (∫ (x : E), f (R • x) ∂μ) = abs (R ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
rcases eq_or_ne R 0 with (rfl | hR)
case inl
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
⊢ ENNReal.toReal (↑↑μ univ) • f 0 = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
case inl
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
⊢ (∫ (x : E), f (0 • x) ∂μ) = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
simp only [zero_smul, integral_const]
case inl.inl
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
hE : finrank ℝ E = 0
⊢ ENNReal.toReal (↑↑μ univ) • f 0 = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ

case inl.inr
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
hE : finrank ℝ E > 0
⊢ ENNReal.toReal (↑↑μ univ) • f 0 = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
case inl
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
⊢ ENNReal.toReal (↑↑μ univ) • f 0 = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
rcases Nat.eq_zero_or_pos (finrank ℝ E) with (hE | hE)
case inl.inl
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
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 = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
case inl.inl
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
hE : finrank ℝ E = 0
⊢ ENNReal.toReal (↑↑μ univ) • f 0 = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
have : Subsingleton E := finrank_zero_iff.1 hE
case inl.inl
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
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 = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
case inl.inl
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
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 = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
have : f = fun _ => f 0 := by ext x; rw [Subsingleton.elim x 0]
case inl.inl
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
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 = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), (fun x => f 0) x ∂μ
case inl.inl
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
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 = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
conv_rhs => rw [this]
no goals
case inl.inl
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
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 = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), (fun x => f 0) x ∂μ
simp only [hE, pow_zero, inv_one, abs_one, one_smul, integral_const]
case h
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
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
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
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
ext x
no goals
case h
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
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
rw [Subsingleton.elim x 0]
case inl.inr
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
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 = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
case inl.inr
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
hE : finrank ℝ E > 0
⊢ ENNReal.toReal (↑↑μ univ) • f 0 = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
have : Nontrivial E := finrank_pos_iff.1 hE
no goals
case inl.inr
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
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 = abs (0 ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
simp only [zero_pow hE, measure_univ_of_isAddLeftInvariant, ENNReal.top_toReal, zero_smul,
  inv_zero, abs_zero]
no goals
case inr
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
f : E → F
R : ℝ
hR : R ≠ 0
⊢ (∫ (x : E), f (R • x) ∂μ) = abs (R ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
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_add_haar_smul μ hR, integral_smul_measure, ENNReal.toReal_ofReal, abs_nonneg]
no goals
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type u_1
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) μ) = abs (R ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
simp only [map_add_haar_smul μ hR, integral_smul_measure, ENNReal.toReal_ofReal, abs_nonneg]