Ae eq dyadic Ball Average Limit on half Ball

lemma ae_eq_dyadicBallAverageLimit_on_halfBall    {u : E → ℝ} {x₀ : E} {R α C_camp : ℝ}    (hα : 0 < α) (hR : 0 < R)    (hcamp : HasCampanatoBound u x₀ R α C_camp) :    ∀ᵐ x ∂volume.restrict (Metric.ball x₀ (R / 2)),      dyadicBallAverageLimit u x (R / 2) = u x := by  classical  let outer : Set E := Metric.ball x₀ R  let inner : Set E := Metric.ball x₀ (R / 2)  let ρ : ℝ := R / 2  let f : E → ℝ := outer.indicator u  have hρ : 0 < ρ := by    dsimp [ρ]    positivity  have hρR : ρ ≤ R := by    dsimp [ρ]    linarith  have hinner_subset_outer : inner ⊆ outer := by    exact Metric.ball_subset_ball hρR  let bouter : CampanatoBall x₀ R := ⟨(x₀, R), ⟨hR, le_rfl, Set.Subset.rfl⟩⟩  have houter_int : IntegrableOn u outer volume := hcamp.integrableOn bouter  have hf_int : Integrable f volume := houter_int.integrable_indicator measurableSet_ball  have hdiff_ae :      ∀ᵐ x ∂volume,        Tendsto (fun n : ℕ => ⨍ y in Metric.closedBall x (ρ / (2 : ℝ) ^ n), f y ∂volume)          atTop (𝓝 (f x)) := by    filter_upwards        [((IsUnifLocDoublingMeasure.vitaliFamily (μ := volume) (K := 0)).ae_tendsto_average          hf_int.locallyIntegrable)] with x hdx    exact Tendsto.comp hdx <|      IsUnifLocDoublingMeasure.tendsto_closedBall_filterAt (μ := volume) (K := 0)        (fun _ : ℕ => x) (fun n : ℕ => ρ / (2 : ℝ) ^ n)        (tendsto_dyadic_radius_nhdsWithin_zero hρ)        (Eventually.of_forall fun n => by          exact Metric.mem_closedBall_self (x := x)            (by positivity : 0 ≤ 0 * (ρ / (2 : ℝ) ^ n)))  have hinner_eq_ae :      ∀ᵐ x ∂volume.restrict inner, dyadicBallAverageLimit u x ρ = u x := by    rw [ae_restrict_iff' measurableSet_ball]    filter_upwards [hdiff_ae] with x hdx hx_inner    have hx_outer : x ∈ outer := hinner_subset_outer hx_inner    have hsub_ball : Metric.ball x ρ ⊆ outer :=      ball_subset_ball_of_mem_ball_half hx_inner hρ.le le_rfl    have hlimit_u :        Tendsto (dyadicBallAverage u x ρ) atTop (𝓝 (dyadicBallAverageLimit u x ρ)) :=      tendsto_dyadicBallAverageLimit hα hcamp hρ hρR hsub_ball    have hclosed_to_u :        Tendsto (fun n : ℕ => ⨍ y in Metric.closedBall x (ρ / (2 : ℝ) ^ n), f y ∂volume)          atTop (𝓝 (u x)) := by      simpa [f, outer, hx_outer] using hdx    have hclosed_eq :        (fun n : ℕ => ⨍ y in Metric.closedBall x (ρ / (2 : ℝ) ^ n), f y ∂volume)          =ᶠ[atTop] dyadicBallAverage u x ρ := by      refine Eventually.of_forall fun n => ?_      have hrn_nonneg : 0 ≤ ρ / (2 : ℝ) ^ n := by positivity      have hrnR : ρ / (2 : ℝ) ^ n ≤ R / 2 := by        calc          ρ / (2 : ℝ) ^ n ≤ ρ := by            exact div_le_self hρ.le (one_le_pow₀ (by norm_num : (1 : ℝ) ≤ 2))          _ = R / 2 := by rfl      have hclosedsub :          Metric.closedBall x (ρ / (2 : ℝ) ^ n) ⊆ outer :=        closedBall_subset_ball_of_mem_ball_half hx_inner hrn_nonneg hrnR      calc        ⨍ y in Metric.closedBall x (ρ / (2 : ℝ) ^ n), f y ∂volume            = ⨍ y in Metric.closedBall x (ρ / (2 : ℝ) ^ n), u y ∂volume := by                apply MeasureTheory.setAverage_congr_fun Metric.isClosed_closedBall.measurableSet                exact Eventually.of_forall fun z hz => by                  simp [f, outer, hclosedsub hz]        _ = ⨍ y in Metric.ball x (ρ / (2 : ℝ) ^ n), u y ∂volume := by              exact setAverage_closedBall_eq_ball_of_pos x (by positivity)        _ = dyadicBallAverage u x ρ n := by              simp [dyadicBallAverage]    have hdyad_to_u :        Tendsto (dyadicBallAverage u x ρ) atTop (𝓝 (u x)) :=      Tendsto.congr' hclosed_eq hclosed_to_u    exact tendsto_nhds_unique hlimit_u hdyad_to_u  simpa [inner, ρ] using hinner_eq_ae