Abs subball Average sub ball Average le

lemma abs_subballAverage_sub_ballAverage_le    {u : E → ℝ} {x c : E} {r s : ℝ}    (hr : 0 < r) (hs : 0 < s)    (hsub : Metric.ball c s ⊆ Metric.ball x r)    (hu_int : IntegrableOn u (Metric.ball x r) volume) :    |⨍ z in Metric.ball c s, u z ∂volume - ⨍ z in Metric.ball x r, u z ∂volume| ≤      (r / s) ^ d * (⨍ z in Metric.ball x r, ‖u z - ⨍ w in Metric.ball x r, u w ∂volume‖ ∂volume) := by  let S : Set E := Metric.ball c s  let B : Set E := Metric.ball x r  let avg : ℝ := ⨍ w in B, u w ∂volume  have hSfin : volume S ≠ ∞ := measure_ball_lt_top.ne  have hBfin : volume B ≠ ∞ := measure_ball_lt_top.ne  have hS0 : volume S ≠ 0 := (measure_ball_pos volume c hs).ne'  have hB0 : volume B ≠ 0 := (measure_ball_pos volume x hr).ne'  have hSreal0 : volume.real S ≠ 0 := (MeasureTheory.measureReal_ne_zero_iff hSfin).2 hS0  have hBreal0 : volume.real B ≠ 0 := (MeasureTheory.measureReal_ne_zero_iff hBfin).2 hB0  have hSreal_pos : 0 < volume.real S := by    rwa [lt_iff_le_and_ne, and_iff_right MeasureTheory.measureReal_nonneg, ne_eq, eq_comm]  have huS_int : IntegrableOn u S volume := hu_int.mono_set hsub  have hdiff :      (⨍ z in S, u z ∂volume) - avg = ⨍ z in S, (u z - avg) ∂volume := by    rw [MeasureTheory.setAverage_eq (μ := volume) (f := u) (s := S),      MeasureTheory.setAverage_eq (μ := volume) (f := fun z => u z - avg) (s := S)]    rw [integral_sub huS_int (integrableOn_const hSfin),      MeasureTheory.setIntegral_const avg]    simp [smul_eq_mul]    field_simp [hSreal0]  have hnorm :      |⨍ z in S, (u z - avg) ∂volume|        ≤ ⨍ z in S, |u z - avg| ∂volume := by    have hnorm' :        |∫ z in S, (u z - avg) ∂volume| ≤ ∫ z in S, |u z - avg| ∂volume := by      simpa [Real.norm_eq_abs, avg] using        (norm_integral_le_integral_norm (fun z => u z - avg) :          ‖∫ z in S, (u z - avg) ∂volume‖ ≤ ∫ z in S, ‖u z - avg‖ ∂volume)    have hSreal_inv_nonneg : 0 ≤ (volume.real S)⁻¹ := by positivity    have hnorm'' := mul_le_mul_of_nonneg_left hnorm' hSreal_inv_nonneg    calc      |⨍ z in S, (u z - avg) ∂volume|          = (volume.real S)⁻¹ * |∫ z in S, (u z - avg) ∂volume| := by              rw [MeasureTheory.setAverage_eq, smul_eq_mul, abs_mul, abs_inv,                abs_of_nonneg MeasureTheory.measureReal_nonneg]      _ ≤ (volume.real S)⁻¹ * ∫ z in S, |u z - avg| ∂volume := hnorm''      _ = ⨍ z in S, |u z - avg| ∂volume := by            rw [MeasureTheory.setAverage_eq, smul_eq_mul]  have habsB_int : IntegrableOn (fun z => |u z - avg|) B volume := by    simpa [Real.norm_eq_abs, avg] using (hu_int.sub (integrableOn_const hBfin)).norm  have hmono :      ∫ z in S, |u z - avg| ∂volume ≤ ∫ z in B, |u z - avg| ∂volume := by    exact MeasureTheory.setIntegral_mono_set habsB_int      (Filter.Eventually.of_forall fun z => abs_nonneg (u z - avg))      (Filter.Eventually.of_forall hsub)  have hvol :      volume.real B = (r / s) ^ d * volume.real S := by    rw [show B = Metric.ball x r by rfl, show S = Metric.ball c s by rfl]    rw [volumeReal_ball_eq x hr, volumeReal_ball_eq c hs]    rw [div_pow]    field_simp [pow_ne_zero _ (ne_of_gt hs)]  calc    |⨍ z in S, u z ∂volume - avg|        = |⨍ z in S, (u z - avg) ∂volume| := by rw [hdiff]    _ ≤ ⨍ z in S, |u z - avg| ∂volume := hnorm    _ = (volume.real S)⁻¹ * ∫ z in S, |u z - avg| ∂volume := by      rw [MeasureTheory.setAverage_eq (μ := volume) (f := fun z => |u z - avg|) (s := S), smul_eq_mul]    _ ≤ (volume.real S)⁻¹ * ∫ z in B, |u z - avg| ∂volume := by      gcongr    _ = (r / s) ^ d * ⨍ z in Metric.ball x r, ‖u z - ⨍ w in Metric.ball x r, u w ∂volume‖ ∂volume := by      have havg_eq : ⨍ z in Metric.ball x r, ‖u z - ⨍ w in Metric.ball x r, u w ∂volume‖ ∂volume =        (volume.real B)⁻¹ * ∫ z in B, |u z - avg| ∂volume := by        rw [MeasureTheory.setAverage_eq, smul_eq_mul]        congr 1 with z      rw [havg_eq, hvol, mul_inv]      have hrs : (r / s) ^ d ≠ 0 := pow_ne_zero d (div_ne_zero (ne_of_gt hr) (ne_of_gt hs))      field_simp [hSreal0, hrs]