MeasureTheory.eLorentzNorm'_indicator_const

lemma eLorentzNorm'_indicator_const {a : ε} (ha : ‖a‖ₑ ≠ ⊤)  {s : Set α} (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤) :    eLorentzNorm' (s.indicator (Function.const α a)) p 1 μ = p * (‖a‖ₑ * μ s ^ p⁻¹.toReal) := by  rw [eLorentzNorm'_eq_integral_distribution_rpow]  congr  simp_rw [distribution_indicator_const (ε := ε) (μ := μ) (s := s) (a := a)]  unfold Set.indicator  simp only [ENNReal.toReal_inv, ite_pow]  symm  calc ‖a‖ₑ * μ s ^ p.toReal⁻¹    _ = (∫⁻ (t : ℝ≥0), (Set.Iio ‖a‖ₑ.toNNReal).indicator (fun x ↦ μ s ^ p.toReal⁻¹) t) := by      rw [lintegral_indicator_const measurableSet_Iio, mul_comm]      congr 1      rw [NNReal.volume_Iio, ENNReal.coe_toNNReal ha]  congr with t  unfold Set.indicator  rw [ENNReal.zero_rpow_of_pos (by simp only [inv_pos]; exact ENNReal.toReal_pos p_ne_zero p_ne_top)]  congr 1  simp only [Set.mem_Iio, eq_iff_iff]  exact (ENNReal.coe_lt_iff_lt_toNNReal ha).symm