Campanato implies holder

theorem campanato_implies_holder    {u : E → ℝ} {x₀ : E} {R α C_camp : ℝ}    (hα : 0 < α) (hα_le : α ≤ 1) (hR : 0 < R)    (hcamp : HasCampanatoBound u x₀ R α C_camp) :    ∃ v : E → ℝ,      (∀ᵐ x ∂volume.restrict (Metric.ball x₀ R), v x = u x) ∧      ∀ x ∈ Metric.ball x₀ (R / 2), ∀ y ∈ Metric.ball x₀ (R / 2),        |v x - v y| ≤ C_campanato_holder d α * C_camp * ‖x - y‖ ^ α := by  classical  let outer : Set E := Metric.ball x₀ R  let inner : Set E := Metric.ball x₀ (R / 2)  let ρ : ℝ := R / 2  let q : ℝ := (2 : ℝ) ^ (-α)  let invDen : ℝ := (1 - q)⁻¹  let v : E → ℝ := fun x =>    if x ∈ inner then dyadicBallAverageLimit u x ρ else u x  have hρ : 0 < ρ := by    dsimp [ρ]    positivity  have hρR : ρ ≤ R := by    dsimp [ρ]    linarith  have hC_nonneg : 0 ≤ C_camp := hcamp.nonneg hα hR  have hq_lt : q < 1 := by    dsimp [q]    rw [Real.rpow_neg (by positivity)]    have h2a : 1 < (2 : ℝ) ^ α := Real.one_lt_rpow (by norm_num) hα    exact inv_lt_one_of_one_lt₀ h2a  have hden_pos : 0 < 1 - q := sub_pos.mpr hq_lt  have hinvDen_nonneg : 0 ≤ invDen := by    dsimp [invDen]    positivity  have h2a_le : (2 : ℝ) ^ α ≤ 2 := by    simpa using      (Real.rpow_le_rpow_of_exponent_le (by norm_num : 1 ≤ (2 : ℝ)) hα_le)  have hq_ge_half : (1 / 2 : ℝ) ≤ q := by    dsimp [q]    rw [Real.rpow_neg (by positivity)]    have h2a_pos : 0 < (2 : ℝ) ^ α := Real.rpow_pos_of_pos (by norm_num) α    simpa [one_div] using (one_div_le_one_div_of_le h2a_pos h2a_le)  have hinvDen_ge_two : (2 : ℝ) ≤ invDen := by    dsimp [invDen]    have hden_half : 1 - q ≤ (1 / 2 : ℝ) := by linarith    have hinv := one_div_le_one_div_of_le hden_pos hden_half    simpa using hinv  have hinner_eq_global :      ∀ᵐ x ∂volume, x ∈ inner → dyadicBallAverageLimit u x ρ = u x := by    have hinner_eq_ae :        ∀ᵐ x ∂volume.restrict inner, dyadicBallAverageLimit u x ρ = u x := by      simpa [inner, ρ] using ae_eq_dyadicBallAverageLimit_on_halfBall hα hR hcamp    rw [ae_restrict_iff' measurableSet_ball] at hinner_eq_ae    exact hinner_eq_ae  refine ⟨v, ?_, ?_⟩  · rw [ae_restrict_iff' measurableSet_ball]    filter_upwards [hinner_eq_global] with x hx hx_outer    by_cases hx_inner : x ∈ inner    · dsimp [v]      rw [if_pos hx_inner]      exact hx hx_inner    · dsimp [v]      rw [if_neg hx_inner]  · intro x hx y hy    have hx_inner : x ∈ inner := by simpa [inner] using hx    have hy_inner : y ∈ inner := by simpa [inner] using hy    have hvx : v x = dyadicBallAverageLimit u x ρ := by      dsimp [v]      rw [if_pos hx_inner]    have hvy : v y = dyadicBallAverageLimit u y ρ := by      dsimp [v]      rw [if_pos hy_inner]    by_cases hsmall : ‖x - y‖ ≤ ρ    · rw [hvx, hvy]      simpa [ρ] using        (dyadicBallAverageLimit_holder_small hα hα_le hR hcamp hx hy          (by simpa [ρ] using hsmall))    · have hlarge : ρ ≤ ‖x - y‖ := le_of_not_ge hsmall      rw [hvx, hvy]      simpa [ρ] using        (dyadicBallAverageLimit_holder_large hα hα_le hR hcamp hx hy          (by simpa [ρ] using hlarge))