continuous_integral_ball

lemma continuous_integral_ball [OpensMeasurableSpace X]    (g : X → ℝ≥0∞) (hg : ∀ x : X, ∀ r > (0 : ℝ), ∫⁻ (y : X) in ball x r, g y ∂μ < ⊤)    (hg2 : AEMeasurable g μ) (hμ : ∀ z : X, ∀ r > (0 : ℝ), μ (sphere z r) = 0 ):    ContinuousOn (fun x : X × ℝ ↦ ∫⁻ y in ball x.1 x.2, g y ∂μ) (univ ×ˢ Ioi 0) := by  intro x hx  have hx_pos : x.2 > 0 := by simp only [mem_prod, mem_univ, mem_Ioi, true_and] at hx; exact hx  unfold ContinuousWithinAt  dsimp only  have : (fun x : X × ℝ ↦ ∫⁻ (y : X) in ball x.1 x.2, g y ∂μ) =      fun x : X × ℝ ↦ ∫⁻ (y : X), (ball x.1 x.2).indicator g y ∂μ := by    ext x    rw [← lintegral_indicator measurableSet_ball]  rw [this, ← lintegral_indicator measurableSet_ball]  apply tendsto_of_seq_tendsto  intro z hz  have hz' : Tendsto z atTop (𝓝 x) := tendsto_nhds_of_tendsto_nhdsWithin hz  have := isBounded_range_of_tendsto z hz'  obtain ⟨r, hr⟩ := Bornology.IsBounded.subset_ball this x  simp only [range, ball, setOf_subset_setOf, forall_exists_index, forall_apply_eq_imp_iff] at hr  simp_rw [Prod.dist_eq] at hr  have hsub (n : ℕ) : ball (z n).1 (z n).2 ⊆ ball x.1 (x.2 + 2 * r) := by    intro y hy    simp only [ball, mem_setOf_eq] at hy ⊢    calc dist y x.1    _  ≤ dist y (z n).1 + dist (z n).1 x.1 := dist_triangle y (z n).1 x.1    _ ≤ (z n).2 + dist (z n).1 x.1 := by gcongr    _ ≤ |(z n).2| + dist (z n).1 x.1 := by gcongr; exact le_abs_self (z n).2    _ = |(z n).2 - x.2 + x.2| + dist (z n).1 x.1 := by rw [sub_add_cancel]    _ ≤ |(z n).2 - x.2| + |x.2| + dist (z n).1 x.1 := by gcongr; exact abs_add_le _ _    _ < r + |x.2| + r := by      gcongr      · calc        _ = dist (z n).2 x.2 := by rw [← Real.dist_eq]        _ ≤ _ := le_max_right (dist (z n).1 x.1) (dist (z n).2 x.2)        _ < r := hr _      · calc        _ ≤ _ := le_max_left (dist (z n).1 x.1) (dist (z n).2 x.2)        _ < r := hr _    _ = r + x.2 + r := by      congr      simp only [mem_prod, mem_univ, mem_Ioi, true_and] at hx; rw [abs_of_nonneg hx.le]    _ = x.2 + 2 * r := by linarith  let bound := (ball x.1 (x.2 + 2 * r)).indicator g  apply tendsto_lintegral_of_dominated_convergence' bound  · exact fun _ ↦ hg2.indicator measurableSet_ball  · intro n    filter_upwards with a    unfold bound indicator    split_ifs with h₀ h₁    · simp    · contrapose! h₁; exact hsub n h₀    · simp    · simp  · unfold bound    rw [lintegral_indicator measurableSet_ball]    apply ne_of_lt    apply hg    have : 0 < r := by      calc      0 ≤ dist (z 0).1 x.1 := dist_nonneg      _ ≤ max (dist (z 0).1 x.1) (dist (z 0).2 x.2) := le_max_left _ _      _ < r := hr _    linarith  · have : ∀ᵐ z : X ∂μ, dist z x.1 ≠ x.2 := by      change (μ ({z | ¬ (dist z x.1 ≠ x.2)}) = 0)      simpa only [ne_eq, Decidable.not_not] using! hμ x.1 x.2 hx_pos    filter_upwards [this] with y hy    by_cases hy2 : dist y x.1 < x.2    · simp only [indicator, ball, mem_setOf_eq]      split_ifs      apply tendsto_nhds_of_eventually_eq      have hz2 : ∀ᶠ n : ℕ in atTop, dist y (z n).1 < (z n).2 := by        let dist_sub (a : X × ℝ) := dist y a.1 - a.2        have : ContinuousOn dist_sub (univ ×ˢ Ioi 0) := by fun_prop        have : Tendsto (dist_sub ∘ z) atTop (𝓝 (dist_sub x)) := Tendsto.comp (this x hx) hz        have : ∀ᶠ (n : ℕ) in atTop, dist y (z n).1 - (z n).2 < 0 := by          rw [← sub_lt_zero] at hy2; exact Tendsto.eventually_lt_const hy2 this        filter_upwards [this]; simp      filter_upwards [hz2]; intro a ha; split_ifs; rfl    · have hz2 : ∀ᶠ n : ℕ in atTop, dist y (z n).1 > (z n).2 := by        let dist_sub (a : X × ℝ) := dist y a.1 - a.2        have : ContinuousOn dist_sub (univ ×ˢ Ioi 0) := by fun_prop        have hcmp : Tendsto (dist_sub ∘ z) atTop (𝓝 (dist_sub x)) := Tendsto.comp (this x hx) hz        have hy2 : dist y x.1 > x.2 := by order        have hy2 : 0 < dist y x.1 - x.2 := sub_pos.mpr hy2        have : ∀ᶠ (n : ℕ) in atTop, 0 < dist y (z n).1 - (z n).2 := Tendsto.eventually_const_lt hy2 hcmp        filter_upwards [this]; simp      simp only [indicator, ball, mem_setOf_eq]      apply tendsto_nhds_of_eventually_eq      filter_upwards [hz2] with n hn      have : ¬ (dist y (z n).1 < (z n).2) := by linarith      split_ifs; rfl