[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
