F : Type u_2
inst✝⁶ : NormedAddCommGroup F
E : Type u_1
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)
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
E : Type u_1
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
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]
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
E : Type u_1
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)
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
E : Type u_1
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)
intro g hg S hS
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
E : Type u_1
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)
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
E : Type u_1
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)
let t := ((Homeomorph.smul (isUnit_iff_ne_zero.2 hS).unit).toMeasurableEquiv : E ≃ᵐ E)
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
E : Type u_1
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 (abs (S ^ finrank ℝ E)⁻¹) ≠ 0
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
E : Type u_1
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
rwa [map_add_haar_smul μ hS, integrable_smul_measure _ ENNReal.ofReal_ne_top]
no goals
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
E : Type u_1
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 (abs (S ^ finrank ℝ E)⁻¹) ≠ 0
simpa only [Ne.def, ENNReal.ofReal_eq_zero, not_le, abs_pos] using inv_ne_zero (pow_ne_zero _ hS)
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
E : Type u_1
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
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
E : Type u_1
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
refine' ⟨fun hf => _, fun hf => this hf hR⟩
case h.e'_5.h.h.e'_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
E : Type u_1
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✝
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
E : Type u_1
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
convert this hf (inv_ne_zero hR)
no goals
case h.e'_5.h.h.e'_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
E : Type u_1
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✝
rw [← mul_smul, mul_inv_cancel hR, one_smul]