small_annulus_right

theorem small_annulus_right {g : X → ℂ} (hg : BoundedFiniteSupport g) {R₁ R₂ : ℝ} (hR₁ : 0 < R₁) :    ContinuousWithinAt (fun R₂ ↦ ∫ y in Annulus.oo x R₁ R₂, K x y * g y) (Ioo R₁ R₂) R₁ := by  by_cases hR1R2 : R₁ < R₂  case neg => rw [Ioo_eq_empty hR1R2, ContinuousWithinAt, nhdsWithin_empty]; exact Filter.tendsto_bot  conv => arg 1; intro R; rw [← integral_indicator (by measurability)]  obtain ⟨B, hB⟩ := czOperator_bound (K := K) (r := R₁) hg hR₁ x  rw [ae_restrict_iff' (by measurability), ← Annulus.ci_eq] at hB  let bound (y : X) : ℝ := (Annulus.oo x R₁ R₂).indicator (fun y ↦ B) y  apply continuousWithinAt_of_dominated (bound := bound)  · filter_upwards with R    have : Measurable (K x) := measurable_K_right x    fun_prop (disch := measurability)  · unfold bound    simp_rw [norm_indicator_eq_indicator_norm]    have : nhdsWithin R₁ (Ioo R₁ R₂) |>.Eventually (fun r ↦ r < R₂) := by      apply eventually_nhdsWithin_of_eventually_nhds      apply eventually_nhds_iff_ball.mpr      use R₂ - R₁      constructor      · simp [hR1R2]      · intro r hr        rw [mem_ball] at hr        linarith [Real.sub_le_dist r R₁]    filter_upwards [this] with r hr    filter_upwards [hB] with y hy    refine indicator_le_indicator_of_subset (by gcongr)      (fun a ↦ by positivity) _ |>.trans <| indicator_le_indicator' ?_    exact fun h2y ↦ hy <| Annulus.oo_subset_ci (by rfl) h2y  · unfold bound    rw [integrable_indicator_iff (by measurability), Annulus.oo_eq]    apply integrableOn_const (measure_ne_top_of_subset inter_subset_left (by finiteness)) (by simp)  · -- This is painful because we have to show continuity of the indicator    -- which is needed to apply `dominated` because `R` is variable in the domain of the integral.    -- This in turn meant proving continuity at `R₁`, which actually aligns with the blueprint.    filter_upwards with y    unfold ContinuousWithinAt    have : nhdsWithin R₁ (Ioo R₁ R₂) |>.Eventually (fun r ↦ y ∉ Annulus.oo x R₁ r) := by      by_cases hy : R₁ < dist x y      · have : nhdsWithin R₁ (Ioo R₁ R₂) |>.Eventually (fun r ↦ r < dist x y) := by          apply eventually_nhdsWithin_of_eventually_nhds          apply eventually_nhds_iff_ball.mpr          use (dist x y - R₁)          constructor          · simp [hy]          · intro r hr            rw [mem_ball] at hr            linarith [Real.sub_le_dist r R₁]        filter_upwards [this] with r hr        exact fun hy ↦ hr.not_gt hy.2      · filter_upwards with r; unfold Annulus.oo; rw [notMem_setOf_iff]; exact fun hy2 ↦ hy hy2.1    rw [Filter.tendsto_iff_forall_eventually_mem]    intro s hs    filter_upwards [this] with r hr    apply mem_of_mem_nhds    simpa [indicator_of_notMem hr] using hs