MeasureTheory.eLorentzNorm_indicator_const

@[simp]lemma eLorentzNorm_indicator_const {a : ε} {s : Set α} :  eLorentzNorm (s.indicator (Function.const α a)) p q μ    = if p = 0 then 0      else if q = 0 then 0      else if p = ∞ then        (if μ s = 0 then 0 else if q = ∞ then ‖a‖ₑ else ∞ * ‖a‖ₑ)      else if q = ∞ then        μ s ^ p.toReal⁻¹ * ‖a‖ₑ      else        (p / q) ^ q.toReal⁻¹ * μ s ^ p.toReal⁻¹ * ‖a‖ₑ := by  unfold eLorentzNorm  split_ifs with h₀ h₁ h₂ h₃ h₄ h₅ h₆ h₇  all_goals try rfl  · exact eLpNormEssSup_indicator_const_eq' h₄  · unfold Function.const    rw [eLpNormEssSup_indicator_const_eq s a h₄]  · unfold Function.const    rw [eLpNormEssSup_indicator_const_eq' h₅]    exact CommMonoidWithZero.mul_zero ⊤  · congr    exact eLpNormEssSup_indicator_const_eq s a h₅  · simp [h₆]  · rw [← eLorentzNorm_eq_eLorentzNorm' h₀ h₁, h₇, eLorentzNorm_eq_wnorm h₀]    rw [wnorm_indicator_const h₀ h₁]  · exact eLorentzNorm'_indicator_const' h₀ h₁ h₆ h₇