Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ (fun x ↦ (ENNReal.ofReal (↑x ^ (dim E - 1))).toReal • f ↑x) =ᵐ[Measure.comap Subtype.val volume] fun x ↦
    ↑x ^ (dim E - 1) • f ↑x

pp: case hf
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ Measurable fun r ↦ ENNReal.ofReal (↑r ^ (dim E - 1))

pp: case hflt
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ ∀ᵐ (x : ↑(Ioi 0)) ∂Measure.comap Subtype.val volume, ENNReal.ofReal (↑x ^ (dim E - 1)) < ∞

pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ MeasurableSet (Ioi 0)

pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ μ.toSphere ≠ 0

Tactic:
· refine .of_forall ?_
    rintro ⟨x, hx : 0 < x⟩
    simp (disch := positivity) [ENNReal.toReal_ofReal]

Goal state after:
case hf
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ Measurable fun r ↦ ENNReal.ofReal (↑r ^ (dim E - 1))

case hflt
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ ∀ᵐ (x : ↑(Ioi 0)) ∂Measure.comap Subtype.val volume, ENNReal.ofReal (↑x ^ (dim E - 1)) < ∞

E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ MeasurableSet (Ioi 0)

E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ μ.toSphere ≠ 0