This file contains results about continuity of integrals and averages over balls that were unused in HardyLittleWood, and whose destiny in Mathlib is unclear.

theorem MeasureTheory.LocallyIntegrable.integrableOn_of_isBounded {X : Type u_1} {E : Type u_2} [MeasurableSpace X] [PseudoMetricSpace X] [NormedAddCommGroup E] {μ : Measure X} [ProperSpace X] {f : X → E} (hf : LocallyIntegrable f μ) {s : Set X} (hs : Bornology.IsBounded s) : IntegrableOn f s μ

theorem MeasureTheory.LocallyIntegrable.integrableOn_ball {X : Type u_1} {E : Type u_2} [MeasurableSpace X] [PseudoMetricSpace X] [NormedAddCommGroup E] {μ : Measure X} [ProperSpace X] {f : X → E} (hf : LocallyIntegrable f μ) {x : X} {r : ℝ} : IntegrableOn f (Metric.ball x r) μ

theorem continuous_integral_ball {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] (g : X → ENNReal) (hg : ∀ (x : X), ∀ r > 0, ∫⁻ (y : X) in Metric.ball x r, g y ∂μ < ⊤) (hg2 : AEMeasurable g μ) (hμ : ∀ (z : X), ∀ r > 0, μ (Metric.sphere z r) = 0) : ContinuousOn (fun (x : X × ℝ) => ∫⁻ (y : X) in Metric.ball x.1 x.2, g y ∂μ) (Set.univ ×ˢ Set.Ioi 0)

theorem continuous_average_ball {X : Type u_1} {E : Type u_2} [MeasurableSpace X] [PseudoMetricSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {f : X → E} [μ.IsOpenPosMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [OpensMeasurableSpace X] [ProperSpace X] (hf : MeasureTheory.LocallyIntegrable f μ) (hμ : ∀ (z : X), ∀ r > 0, μ (Metric.sphere z r) = 0) : ContinuousOn (fun (x : X × ℝ) => ⨍⁻ (y : X) in Metric.ball x.1 x.2, ‖f y‖ₑ ∂μ) (Set.univ ×ˢ Set.Ioi 0)

theorem lowerSemiContinuousOn_integral_ball {X : Type u_1} {E : Type u_2} [MeasurableSpace X] [PseudoMetricSpace X] [NormedAddCommGroup E] {μ : MeasureTheory.Measure X} {f : X → E} [OpensMeasurableSpace X] (hf2 : MeasureTheory.AEStronglyMeasurable f μ) : LowerSemicontinuousOn (fun (x : X × ℝ) => ∫⁻ (y : X) in Metric.ball x.1 x.2, ‖f y‖ₑ ∂μ) (Set.univ ×ˢ Set.Ioi 0)