Abs sub const bmo le two

lemma abs_sub_const_bmo_le_two    {M : ℝ} {u : E → ℝ} {c : ℝ} {z : E} {s : ℝ} (hs : 0 < s)    (hu_int : IntegrableOn u (Metric.ball z s) volume)    (hu_bmo : (⨍ x in Metric.ball z s,      ‖u x - ⨍ y in Metric.ball z s, u y ∂volume‖ ∂volume) ≤ M) :    (⨍ x in Metric.ball z s,      ‖ |u x - c| - ⨍ y in Metric.ball z s, |u y - c| ∂volume‖ ∂volume) ≤ 2 * M := by  -- Abbreviations  set B := Metric.ball z s with hB_def  set avg_u := ⨍ y in B, u y ∂volume with havg_u_def  set w : E → ℝ := fun x => |u x - c| with hw_def  set avg_w := ⨍ y in B, w y ∂volume with havg_w_def  -- Measure facts  have hB_vol_pos : 0 < volume B := measure_ball_pos volume z hs  have hB_vol_ne_zero : volume B ≠ 0 := hB_vol_pos.ne'  have hB_vol_ne_top : volume B ≠ ⊤ := measure_ball_lt_top.ne  haveI : IsFiniteMeasure (volume.restrict B) :=    ⟨by rw [Measure.restrict_apply_univ]; exact hB_vol_ne_top.lt_top⟩  have hvolR_pos : 0 < volume.real B :=    ENNReal.toReal_pos hB_vol_ne_zero hB_vol_ne_top  have hvolR_ne_zero : volume.real B ≠ 0 := hvolR_pos.ne'  -- Integrability facts  have hw_int : IntegrableOn w B volume := (hu_int.sub integrableOn_const).norm  have hu_sub_avg_int : IntegrableOn (fun x => u x - avg_u) B volume :=    hu_int.sub integrableOn_const  have hw_sub_avg_int : IntegrableOn (fun x => w x - avg_w) B volume :=    hw_int.sub integrableOn_const  have hnorm_w_sub_avg_int : IntegrableOn (fun x => ‖w x - avg_w‖) B volume :=    hw_sub_avg_int.norm  -- Key constant: a = |avg_u - c|  set a := |avg_u - c| with ha_def  have hrev_tri : ∀ x, ‖w x - a‖ ≤ ‖u x - avg_u‖ := by    intro x    simp only [hw_def, ha_def]    rw [show u x - avg_u = (u x - c) - (avg_u - c) from by ring]    exact norm_abs_sub_abs (u x - c) (avg_u - c)  -- Reverse triangle in the other direction (for Jensen step)  have hrev_tri' : ∀ y, ‖a - w y‖ ≤ ‖u y - avg_u‖ := by    intro y    rw [norm_sub_rev]    exact hrev_tri y  -- Proof: ‖a - avg_w‖ ≤ ⨍ ‖a - w y‖ ≤ ⨍ ‖u y - avg_u‖  have hJensen : ‖a - avg_w‖ ≤ ⨍ y in B, ‖u y - avg_u‖ ∂volume := by    -- First bound: ‖a - avg_w‖ = ‖(volR B)⁻¹ • (volR B • a - ∫ w)‖    -- = (volR B)⁻¹ * ‖∫ (a - w)‖ ≤ (volR B)⁻¹ * ∫ ‖a - w‖ ≤ (volR B)⁻¹ * ∫ ‖u - avg_u‖    rw [havg_w_def, setAverage_eq]    -- ‖a - (volR B)⁻¹ • ∫ w‖    have hsub_eq : a - (volume.real B)⁻¹ • ∫ y in B, w y ∂volume =        (volume.real B)⁻¹ • (∫ y in B, (a - w y) ∂volume) := by      rw [integral_sub (integrable_const a) hw_int, integral_const,        measureReal_restrict_apply_univ, smul_sub]      simp only [smul_eq_mul, measureReal_def]      have hvR : (volume B).toReal ≠ 0 :=        ENNReal.toReal_ne_zero.mpr ⟨hB_vol_ne_zero, hB_vol_ne_top⟩      field_simp [hvR]    rw [hsub_eq, norm_smul, Real.norm_of_nonneg (inv_nonneg.mpr hvolR_pos.le)]    -- Now: (volR B)⁻¹ * ‖∫ (a - w)‖ ≤ (volR B)⁻¹ * ∫ ‖a - w‖ ≤ (volR B)⁻¹ * ∫ ‖u - avg_u‖    rw [setAverage_eq]    apply mul_le_mul_of_nonneg_left _ (inv_nonneg.mpr hvolR_pos.le)    calc ‖∫ y in B, (a - w y) ∂volume‖        ≤ ∫ y in B, ‖a - w y‖ ∂volume := norm_integral_le_integral_norm _      _ ≤ ∫ y in B, ‖u y - avg_u‖ ∂volume := by          apply setIntegral_mono ((integrable_const a).sub hw_int).norm hu_sub_avg_int.norm          exact fun y => hrev_tri' y  -- ‖w x - avg_w‖ ≤ ‖w x - a‖ + ‖a - avg_w‖ ≤ ‖u x - avg_u‖ + ⨍ ‖u - avg_u‖  have hpointwise : ∀ x, ‖w x - avg_w‖ ≤      ‖u x - avg_u‖ + ⨍ y in B, ‖u y - avg_u‖ ∂volume := by    intro x    calc ‖w x - avg_w‖        = ‖(w x - a) + (a - avg_w)‖ := by congr 1; ring      _ ≤ ‖w x - a‖ + ‖a - avg_w‖ := norm_add_le _ _      _ ≤ ‖u x - avg_u‖ + ⨍ y in B, ‖u y - avg_u‖ ∂volume :=          add_le_add (hrev_tri x) hJensen  -- ⨍ ‖w - avg_w‖ ≤ ⨍ (‖u - avg_u‖ + const) = ⨍ ‖u - avg_u‖ + const ≤ M + M = 2M  have hint_le : ∫ x in B, ‖w x - avg_w‖ ∂volume ≤      ∫ x in B, (‖u x - avg_u‖ + ⨍ y in B, ‖u y - avg_u‖ ∂volume) ∂volume :=    setIntegral_mono hnorm_w_sub_avg_int      (hu_sub_avg_int.norm.add integrableOn_const) (fun x => hpointwise x)  have hint_split : ∫ x in B, (‖u x - avg_u‖ + ⨍ y in B, ‖u y - avg_u‖ ∂volume) ∂volume =      (∫ x in B, ‖u x - avg_u‖ ∂volume) +      (⨍ y in B, ‖u y - avg_u‖ ∂volume) * volume.real B := by    rw [integral_add hu_sub_avg_int.norm (integrable_const _),      integral_const, measureReal_restrict_apply_univ,      smul_eq_mul, mul_comm, measureReal_def]  -- Convert to averages: ⨍ ‖w - avg_w‖ ≤ ⨍ ‖u - avg_u‖ + ⨍ ‖u - avg_u‖  set osc_u := ⨍ y in B, ‖u y - avg_u‖ ∂volume with hosc_u_def  have hfinal : ⨍ x in B, ‖w x - avg_w‖ ∂volume ≤ osc_u + osc_u := by    -- All averages are (volR B)⁻¹ • ∫    -- From hint_le + hint_split:    -- ∫ ‖w - avg_w‖ ≤ ∫ ‖u - avg_u‖ + osc_u * volR B    -- So ⨍ ‖w - avg_w‖ = (volR B)⁻¹ * ∫ ‖w - avg_w‖    --    ≤ (volR B)⁻¹ * (∫ ‖u - avg_u‖ + osc_u * volR B)    --    = (volR B)⁻¹ * ∫ ‖u - avg_u‖ + osc_u    --    = ⨍ ‖u - avg_u‖ + osc_u = osc_u + osc_u    have hle_int : ∫ x in B, ‖w x - avg_w‖ ∂volume ≤        (∫ x in B, ‖u x - avg_u‖ ∂volume) + osc_u * volume.real B := by      linarith [hint_le, hint_split]    -- osc_u * volume.real B = ∫ ‖u - avg_u‖    have hosc_vol : osc_u * volume.real B = ∫ x in B, ‖u x - avg_u‖ ∂volume := by      rw [hosc_u_def, setAverage_eq, smul_eq_mul, mul_comm (volume.real B)⁻¹,        mul_assoc, inv_mul_cancel₀ hvolR_ne_zero, mul_one]    -- So ∫ ‖w - avg_w‖ ≤ 2 * ∫ ‖u - avg_u‖    have hle_int2 : ∫ x in B, ‖w x - avg_w‖ ∂volume ≤        2 * ∫ x in B, ‖u x - avg_u‖ ∂volume := by linarith [hosc_vol]    -- Divide by volume.real B    show ⨍ x in B, ‖w x - avg_w‖ ∂volume ≤ osc_u + osc_u    rw [hosc_u_def, setAverage_eq, setAverage_eq, smul_eq_mul, smul_eq_mul]    calc (volume.real B)⁻¹ * ∫ x in B, ‖w x - avg_w‖ ∂volume        ≤ (volume.real B)⁻¹ * (2 * ∫ x in B, ‖u x - avg_u‖ ∂volume) :=          mul_le_mul_of_nonneg_left hle_int2 (inv_nonneg.mpr hvolR_pos.le)      _ = 2 * ((volume.real B)⁻¹ * ∫ x in B, ‖u x - avg_u‖ ∂volume) := by ring      _ = (volume.real B)⁻¹ * ∫ x in B, ‖u x - avg_u‖ ∂volume +          (volume.real B)⁻¹ * ∫ x in B, ‖u x - avg_u‖ ∂volume := by ring  calc ⨍ x in B, ‖w x - avg_w‖ ∂volume      ≤ osc_u + osc_u := hfinal    _ ≤ M + M := by linarith [hu_bmo]    _ = 2 * M := by ring