small_annulus_left

theorem small_annulus_left {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₂ / 2) hg (by linarith [hR₁.trans_lt hR1R2]) x  rw [ae_restrict_iff' (by measurability), ← Annulus.ci_eq] at hB  let bound (y : X) : ℝ := (Annulus.oo x (R₂ / 2) 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₂ / 2 < r) := by      apply eventually_nhdsWithin_of_eventually_nhds      apply eventually_nhds_iff_ball.mpr      use R₂ / 2      constructor      · simp [hR₁.trans_lt hR1R2]      · intro r hr        rw [mem_ball, dist_comm] 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 : dist x y < R₂      · have : nhdsWithin R₂ (Ioo R₁ R₂) |>.Eventually (fun r ↦ dist x y < r) := by          apply eventually_nhdsWithin_of_eventually_nhds          apply eventually_nhds_iff_ball.mpr          use (R₂ - dist x y)          constructor          · simp [hy]          · intro r hr            rw [mem_ball, dist_comm] at hr            linarith [Real.sub_le_dist R₂ r]        filter_upwards [this] with r hr        exact fun hy ↦ hr.not_gt hy.1      · filter_upwards with r; unfold Annulus.oo; rw [notMem_setOf_iff]; exact fun hy2 ↦ hy hy2.2    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