Le ess Inf half Ball of ae bound

theorem le_essInf_halfBall_of_ae_bound    {u : E → ℝ} {c C : ℝ}    (hlow : ∀ᵐ x ∂μhalf, c ≤ u x)    (hupp : ∀ᵐ x ∂μhalf, u x ≤ C) :    c ≤ essInf u μhalf := by  rw [essInf_eq_sSup]  refine le_csSup ?_ ?_  · refine ⟨C, ?_⟩    intro a ha    have ha_ae : ∀ᵐ x ∂μhalf, a ≤ u x := by      rw [ae_iff]      simpa [not_le] using ha    have hconst : ∀ᵐ x ∂μhalf, a ≤ C := by      filter_upwards [ha_ae, hupp] with x hax hxu      linarith    by_contra hAC    have hfalse : ∀ᵐ x ∂μhalf, False := by      filter_upwards [hconst] with x hx      linarith    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)  · have hlow' := hlow    rw [ae_iff] at hlow'    simpa [not_le] using hlow'