MeasureTheory.wnorm_indicator_const

theorem wnorm_indicator_const {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε]  {a : ε} {s : Set α} {p : ℝ≥0∞}  (h₀ : ¬p = 0) (h₁ : ¬p = ⊤) :    wnorm (s.indicator (Function.const α a)) p μ = μ s ^ p.toReal⁻¹ * ‖a‖ₑ := by  have hp : 0 < p.toReal⁻¹ := by    simp only [inv_pos]    exact ENNReal.toReal_pos h₀ h₁  rw [wnorm_ne_top h₁]  unfold wnorm'  simp_rw [distribution_indicator_const]  apply le_antisymm  · apply iSup_le    intro t    unfold indicator    split_ifs with ht    · rw [mul_comm]      gcongr      exact ht.le    · rw [ENNReal.zero_rpow_of_pos]      · simp      simp only [inv_pos]      apply ENNReal.toReal_pos h₀ h₁  · by_cases h : μ s = 0    · rw [h]      simp only [indicator_zero]      rw [ENNReal.zero_rpow_of_pos hp]      simp    by_cases ha : ‖a‖ₑ = 0    · rw [ha]      simp    by_cases ha' : ‖a‖ₑ = ⊤    · rw [ha']      simp only [mem_Iio, coe_lt_top, indicator_of_mem]      rw [← ENNReal.iSup_mul, mul_comm]      gcongr      simp only [top_le_iff]      exact WithTop.iSup_coe_eq_top'    by_cases h' : μ s = ⊤    · rw [h', ENNReal.top_rpow_of_pos hp, ENNReal.top_mul ha]      simp only [top_le_iff]      rw [iSup_eq_top]      intro b hb      use ‖a‖ₑ.toNNReal / 2      simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, coe_div, coe_ofNat]      rwa [ENNReal.coe_toNNReal ha', indicator, ite_cond_eq_true, ENNReal.top_rpow_of_pos hp, ENNReal.mul_top]      · simpa      · simp only [mem_Iio, eq_iff_iff, iff_true]        apply ENNReal.div_lt_of_lt_mul'        nth_rw 1 [← one_mul ‖a‖ₑ]        gcongr        norm_num    apply le_of_forall_lt_imp_le_of_dense    intro c hc    apply le_iSup_of_le (c / (μ s ^ p.toReal⁻¹)).toNNReal    have hc' : c / μ s ^ p.toReal⁻¹ ≠ ⊤ := by      contrapose! hc      rw [div_eq_top] at hc      rcases hc with ⟨_, hc⟩ | hc      · rw [ENNReal.rpow_eq_zero_iff_of_pos hp] at hc        contradiction      · rw [hc.1]        exact le_top    rw [indicator_apply, ite_cond_eq_true, ENNReal.coe_toNNReal hc', ENNReal.div_mul_cancel]    · simp only [ne_eq, ENNReal.rpow_eq_zero_iff, inv_pos, inv_neg'', not_or, not_and, not_lt,      toReal_nonneg, implies_true, and_true]      intro h      contradiction    · simp only [ne_eq, rpow_eq_top_iff, inv_neg'', inv_pos, not_or, not_and, not_lt,      toReal_nonneg, implies_true, true_and]      intro h      contradiction    · rw [ENNReal.coe_toNNReal hc']      simp only [mem_Iio, eq_iff_iff, iff_true]      apply ENNReal.div_lt_of_lt_mul' hc