oscillation_control

lemma oscillation_control {x : ℝ} {r : ℝ} {f g : Θ ℝ} :    localOscillation (ball x r) (coeΘ f) (coeΘ g) ≤ ENNReal.ofReal (dist_{x, r} f g) := by  by_cases! r_pos : r ≤ 0  · rw [ball_eq_empty.mpr r_pos]    simp [localOscillation]  simp_rw [dist_integer_linear_eq]  calc ⨆ z ∈ ball x r ×ˢ ball x r, ENNReal.ofReal ‖↑f * z.1 - ↑g * z.1 - ↑f * z.2 + ↑g * z.2‖    _ = ⨆ z ∈ ball x r ×ˢ ball x r, ENNReal.ofReal |(f - g) * (z.1 - x) - (f - g) * (z.2 - x)| := by      congr with z      congr with h      rw [Real.norm_eq_abs]      ring_nf    _ ≤ ENNReal.ofReal (2 * r * |↑f - ↑g|) := by      refine iSup₂_le (fun z hz ↦ ?_)      apply ENNReal.ofReal_le_of_le_toReal      rw [ENNReal.toReal_ofReal (by positivity)]      simp_rw [Set.mem_prod, mem_ball, Real.dist_eq] at hz      calc |(f - g) * (z.1 - x) - (f - g) * (z.2 - x)|        _ ≤ |(f - g) * (z.1 - x)| + |(f - g) * (z.2 - x)| := abs_sub ..        _ = |↑f - ↑g| * |z.1 - x| + |↑f - ↑g| * |z.2 - x| := by congr <;> apply abs_mul        _ ≤ |↑f - ↑g| * r + |↑f - ↑g| * r := by          gcongr          · linarith [hz.1]          · linarith [hz.2]        _ = 2 * r * |↑f - ↑g| := by ring    _ ≤ ENNReal.ofReal (2 * max r 0 * |↑f - ↑g|) := by      gcongr      apply le_max_left