Ess Sup half Ball le of ae bound

theorem essSup_halfBall_le_of_ae_bound    {u : E → ℝ} {C : ℝ}    (h_nonneg : ∀ᵐ x ∂μhalf, 0 ≤ u x)    (hbound : ∀ᵐ x ∂μhalf, u x ≤ C) :    essSup u μhalf ≤ C := by  rw [essSup_eq_sInf]  refine csInf_le ?_ ?_  · refine ⟨0, ?_⟩    intro b hb    by_contra hb_nonneg    have hb_neg : b < 0 := lt_of_not_ge hb_nonneg    have hs : {x | b < u x} ∈ ae μhalf := by      filter_upwards [h_nonneg] with x hx      linarith    have hs_compl : {x | b < u x}ᶜ ∈ ae μhalf := by      exact compl_mem_ae_iff.mpr hb    have hfalse : ∀ᵐ x ∂μhalf, False := by      filter_upwards [hs, hs_compl] with x hx hx_compl      exact hx_compl hx    rw [ae_iff] at hfalse    have hzero : μhalf Set.univ = 0 := by      simpa using hfalse    exact      (restrict_ball_ne_zero (c := (0 : E)) (r := (1 / 2 : ℝ)) (by norm_num))        (Measure.measure_univ_eq_zero.mp hzero)  · simpa [not_le] using (ae_iff.mp hbound)