Right Continuous integral annulus

lemma rightContinuous_integral_annulus (iof : IntegrableOn f (oo x R₁ R₂)) :    ContinuousWithinAt (fun R ↦ ∫ y in oo x R R₂, f y) (Ici R₁) R₁ := by  -- If `R₁ ≥ R₂` the proof is easy  rcases le_or_gt R₂ R₁ with hR₂ | hR₂  · simp_rw [continuousWithinAt_iff, mem_Ici]; intro ε εpos    use 1, zero_lt_one; intro R' hR' _    rw [oo_eq_empty (hR₂.trans hR'), oo_eq_empty hR₂, setIntegral_empty, dist_self]    exact εpos  -- Reduce to showing that the volumes of annuli `oc x R₁ R` can be arbitrarily small  suffices Tendsto (volume.restrict (oo x R₁ R₂) ∘ (oc x R₁ ·)) (𝓝[≥] R₁) (nhds 0) by    simp_rw [continuousWithinAt_iff, mem_Ici]; intro ε εpos    have key := iof.tendsto_setIntegral_nhds_zero this    simp_rw [← integral_indicator measurableSet_oc, ← integral_indicator measurableSet_oo,      indicator_indicator, tendsto_nhdsWithin_nhds, mem_Ici] at key    specialize key _ εpos; obtain ⟨δ, δpos, nb⟩ := key    use min δ (R₂ - R₁), lt_min_iff.mpr ⟨δpos, sub_pos.mpr hR₂⟩; intro y ly dy    rw [lt_min_iff] at dy; specialize nb ly dy.1    rw [dist_eq_norm, Real.norm_of_nonneg (sub_nonneg.mpr ly), sub_lt_sub_iff_right] at dy    rw [dist_eq_norm, sub_zero, inter_eq_self_of_subset_right (oc_subset_oo le_rfl dy.2),      integral_indicator measurableSet_oc] at nb    rw [dist_eq_norm']; convert nb    rw [sub_eq_iff_eq_add, ← setIntegral_union _ measurableSet_oo]; rotate_left    · exact iof.mono_set (oc_subset_oo le_rfl dy.2)    · exact iof.mono_set (by gcongr)    · simp_rw [disjoint_left, oc, oo, mem_setOf, mem_Ioc, mem_Ioo, not_and_or, not_lt]      exact fun z mz ↦ .inl mz.2    rw [oc_union_oo ly dy.2]  -- Obtain a strictly antitone sequence of numbers less than `R₂` and converging to `R₁`.  -- By monotone convergence we reduce to showing that the volumes of annuli `oc x R₁ R`  -- along this sequence can be arbitrarily small  obtain ⟨u, sau, mu, ttu⟩ := exists_seq_strictAnti_tendsto' hR₂  suffices Tendsto (fun n ↦ volume (oc x R₁ (u n))) atTop (nhds 0) by    rw [ENNReal.tendsto_nhds_zero]; intro ε εpos    rw [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff]    rw [ENNReal.tendsto_atTop_zero] at this    specialize this _ εpos; obtain ⟨n, hn⟩ := this; specialize hn _ le_rfl    use u n - R₁, sub_pos.mpr (mu n).1; intro y dy ly    rw [dist_eq_norm, Real.norm_of_nonneg (sub_nonneg.mpr ly), sub_lt_sub_iff_right] at dy    rw [Function.comp_apply, Measure.restrict_apply measurableSet_oc,      inter_eq_self_of_subset_left (oc_subset_oo le_rfl (dy.trans (mu n).2))]    exact (measure_mono (by gcongr)).trans hn  -- Split the annulus along the `u n`...  let s (n : ℕ) := oc x (u (n + 1)) (u n)  have us (k : ℕ) : ⋃ n, s (k + n) = oc x R₁ (u k) := by    ext y; simp_rw [mem_iUnion, s, oc, mem_setOf, mem_Ioc]; constructor <;> intro h    · obtain ⟨n, hn₁, hn₂⟩ := h      exact ⟨(mu (k + n + 1)).1.trans hn₁, hn₂.trans (sau.antitone (Nat.le_add_right ..))⟩    · let T : Set ℕ := {n | u (k + n) < dist x y}      have neT : T.Nonempty := by        rw [Metric.tendsto_atTop] at ttu        specialize ttu (dist x y - R₁) (by linarith only [h.1]); obtain ⟨N, hN⟩ := ttu        specialize hN (k + N) (Nat.le_add_left ..)        rw [dist_eq_norm, Real.norm_of_nonneg (by linarith only [(mu (k + N)).1]),          sub_lt_sub_iff_right] at hN; use N, hN      have wfT : T.IsWF := IsWF.of_wellFoundedLT T      use wfT.min neT - 1      have minT_mem := wfT.min_mem neT; simp_rw [T, mem_setOf] at minT_mem      have minT_pos : wfT.min neT ≠ 0 := by        by_contra! h'; rw [h'] at minT_mem; exact absurd h.2 (not_le.mpr minT_mem)      nth_rw 1 [← Nat.add_sub_assoc (by lia), Nat.sub_add_cancel (by lia), ← not_lt]      refine ⟨minT_mem, ?_⟩; change wfT.min neT - 1 ∉ T; contrapose! minT_pos      replace minT_pos := wfT.min_le neT minT_pos; lia  have ds (k : ℕ) : Pairwise (Function.onFun Disjoint fun n ↦ s (k + n)) := fun i j hn ↦ by    change Disjoint (s (k + i)) (s (k + j))    wlog hl : i < j generalizing i j; · exact (this j i hn.symm (by lia)).symm    simp_rw [s, disjoint_left, oc, mem_setOf, mem_Ioc]; intro y my    rw [not_and_or, not_le]; right    exact (sau.antitone (show k + i + 1 ≤ k + j by lia)).trans_lt my.1  -- ...and appeal to `ENNReal.tendsto_sum_nat_add`  conv =>    enter [1, n]; rw [← us, measure_iUnion (ds n) (fun _ ↦ measurableSet_oc)]    enter [1, k]; rw [add_comm]  specialize us 0; specialize ds 0; simp_rw [zero_add] at us ds  apply tendsto_sum_nat_add fun n ↦ volume (s n)  rw [← measure_iUnion ds (fun _ ↦ measurableSet_oc), us, ← lt_top_iff_ne_top]  calc    _ ≤ volume (closedBall x (u 0)) := by      refine measure_mono fun y my ↦ ?_; rw [oc_eq] at my; exact my.1    _ < _ := measure_closedBall_lt_top