continuous_average_ball

lemma continuous_average_ball [μ.IsOpenPosMeasure] [IsFiniteMeasureOnCompacts μ] [OpensMeasurableSpace X]    [ProperSpace X] (hf : LocallyIntegrable f μ)    (hμ : ∀ z : X, ∀ r > (0 : ℝ), μ (sphere z r) = 0) :    ContinuousOn (fun x : X × ℝ ↦ ⨍⁻ y in ball x.1 x.2, ‖f y‖ₑ ∂μ) (univ ×ˢ Ioi 0) := by  rw [(isOpen_univ.prod isOpen_Ioi).continuousOn_iff]  intro x hx  have hx_pos : 0 < x.2 := by simp only [mem_prod, mem_univ, mem_Ioi, true_and] at hx; exact hx  have : (fun x : X × ℝ ↦ ⨍⁻ y in ball x.1 x.2, ‖f y‖ₑ ∂μ) =    fun x : X × ℝ ↦ (μ (ball x.1 x.2))⁻¹ * ∫⁻ y in ball x.1 x.2, ‖f y‖ₑ ∂μ     := by ext x; simp [laverage]  rw [this]  apply ENNReal.Tendsto.mul  · apply Tendsto.inv    have : (fun z : X × ℝ ↦ μ (ball z.1 z.2)) =        (fun z : X × ℝ ↦ ∫⁻ (y : X) in ball z.1 z.2, (1 : ℝ≥0∞) ∂μ) := by simp    rw [this, (setLIntegral_one (ball x.1 x.2)).symm]    have : ContinuousOn (fun x : X × ℝ ↦ ∫⁻ y in ball x.1 x.2, (1 : ℝ≥0∞) ∂μ) (univ ×ˢ Ioi 0) := by      apply continuous_integral_ball _ _ aemeasurable_const hμ      intro p r hr; rw [setLIntegral_one]; finiteness    rw [(isOpen_univ.prod isOpen_Ioi).continuousOn_iff] at this    apply this hx  · exact Or.inr (hf.integrableOn_ball.right.ne)  · have : ContinuousOn (fun x : X × ℝ ↦ ∫⁻ y in ball x.1 x.2, ‖f y‖ₑ ∂μ) (univ ×ˢ Ioi 0) := by      apply continuous_integral_ball _ _ _ hμ      · exact fun x r hr ↦ hf.integrableOn_ball.right      · exact hf.aestronglyMeasurable.enorm    rw [(isOpen_univ.prod isOpen_Ioi).continuousOn_iff] at this    exact this hx  · exact Or.inr (inv_ne_top.mpr (measure_ball_pos μ x.1 hx_pos).ne')