feat: more API for ae strongly measurable functions on compact sets (#33670)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

@@ -487,17 +487,12 @@ theorem ContinuousOn.locallyIntegrableOn [IsLocallyFiniteMeasure μ]
 theorem ContinuousOn.integrableOn_of_subset_isCompact (hf : ContinuousOn f K)
     (hK : IsCompact K) (hs : MeasurableSet s) (h's : s ⊆ K) (mus : μ s ≠ ∞) :
     IntegrableOn f s μ := by
-  constructor
-  · borelize E
-    rw [aestronglyMeasurable_iff_aemeasurable_separable]
-    refine ⟨(hf.mono h's).aemeasurable hs, f '' s, ?_, ?_⟩
-    · exact (hK.image_of_continuousOn hf).isSeparable.mono (image_mono h's)
-    · filter_upwards [ae_restrict_mem hs] with a ha using mem_image_of_mem f ha
-  · have : Fact (μ s < ∞) := ⟨mus.lt_top⟩
-    obtain ⟨C, hC⟩ : ∃ C, ∀ x ∈ f '' K, ‖x‖ ≤ C :=
-      IsBounded.exists_norm_le (hK.image_of_continuousOn hf).isBounded
-    apply HasFiniteIntegral.of_bounded (C := C)
-    filter_upwards [ae_restrict_mem hs] with a ha using hC _ (mem_image_of_mem f (h's ha))
+  refine ⟨hf.aestronglyMeasurable_of_subset_isCompact hK hs h's, ?_⟩
+  have : Fact (μ s < ∞) := ⟨mus.lt_top⟩
+  obtain ⟨C, hC⟩ : ∃ C, ∀ x ∈ f '' K, ‖x‖ ≤ C :=
+    IsBounded.exists_norm_le (hK.image_of_continuousOn hf).isBounded
+  apply HasFiniteIntegral.of_bounded (C := C)
+  filter_upwards [ae_restrict_mem hs] with a ha using hC _ (mem_image_of_mem f (h's ha))
 
 variable [IsFiniteMeasureOnCompacts μ]
 

Mathlib/MeasureTheory/Integral/IntegrableOn.lean

@@ -675,18 +675,31 @@ theorem ContinuousOn.aestronglyMeasurable [TopologicalSpace α] [TopologicalSpac
     exact isSeparable_range <| continuousOn_iff_continuous_restrict.1 hf
   · exact .of_separableSpace _
 
+/-- A function which is continuous on a compact set `s` is almost everywhere strongly measurable
+with respect to `μ.restrict t` for any measurable subset `t` of `s`. -/
+theorem ContinuousOn.aestronglyMeasurable_of_subset_isCompact
+    [TopologicalSpace α] [OpensMeasurableSpace α]
+    [TopologicalSpace β] [PseudoMetrizableSpace β] {f : α → β} {s t : Set α} {μ : Measure α}
+    (hf : ContinuousOn f s) (hs : IsCompact s) (ht : MeasurableSet t) (hts : t ⊆ s) :
+    AEStronglyMeasurable f (μ.restrict t) := by
+  borelize β
+  rw [aestronglyMeasurable_iff_aemeasurable_separable]
+  refine ⟨(hf.mono hts).aemeasurable ht, f '' s, ?_, ?_⟩
+  · exact (hs.image_of_continuousOn hf).isSeparable
+  · filter_upwards [ae_restrict_mem ht] with a ha using image_mono hts (mem_image_of_mem f ha)
+
 /-- A function which is continuous on a compact set `s` is almost everywhere strongly measurable
 with respect to `μ.restrict s`. -/
 theorem ContinuousOn.aestronglyMeasurable_of_isCompact [TopologicalSpace α] [OpensMeasurableSpace α]
     [TopologicalSpace β] [PseudoMetrizableSpace β] {f : α → β} {s : Set α} {μ : Measure α}
     (hf : ContinuousOn f s) (hs : IsCompact s) (h's : MeasurableSet s) :
-    AEStronglyMeasurable f (μ.restrict s) := by
-  letI := pseudoMetrizableSpacePseudoMetric β
-  borelize β
-  rw [aestronglyMeasurable_iff_aemeasurable_separable]
-  refine ⟨hf.aemeasurable h's, f '' s, ?_, ?_⟩
-  · exact (hs.image_of_continuousOn hf).isSeparable
-  · exact mem_of_superset (self_mem_ae_restrict h's) (subset_preimage_image _ _)
+    AEStronglyMeasurable f (μ.restrict s) :=
+  hf.aestronglyMeasurable_of_subset_isCompact hs h's Subset.rfl
+
+lemma Continuous.aestronglyMeasurable_of_compactSpace [TopologicalSpace α] [OpensMeasurableSpace α]
+    [CompactSpace α] [TopologicalSpace β] [PseudoMetrizableSpace β] {μ : Measure α} {f : α → β}
+    (hf : Continuous f) : AEStronglyMeasurable f μ := by
+  simpa using hf.continuousOn.aestronglyMeasurable_of_isCompact isCompact_univ .univ
 
 theorem ContinuousOn.integrableAt_nhdsWithin_of_isSeparable [TopologicalSpace α]
     [PseudoMetrizableSpace α] [OpensMeasurableSpace α] {μ : Measure α} [IsLocallyFiniteMeasure μ]

Mathlib/MeasureTheory/Measure/Restrict.lean

@@ -300,10 +300,16 @@ theorem restrict_map {f : α → β} (hf : Measurable f) {s : Set β} (hs : Meas
     (μ.map f).restrict s = (μ.restrict <| f ⁻¹' s).map f :=
   ext fun t ht => by simp [*, hf ht]
 
-theorem restrict_toMeasurable (h : μ s ≠ ∞) : μ.restrict (toMeasurable μ s) = μ.restrict s :=
-  ext fun t ht => by
-    rw [restrict_apply ht, restrict_apply ht, inter_comm, measure_toMeasurable_inter ht h,
-      inter_comm]
+theorem restrict_inter_toMeasurable (h : μ s ≠ ∞) (ht : MeasurableSet t) (hst : s ⊆ t) :
+    μ.restrict (t ∩ toMeasurable μ s) = μ.restrict s := by
+  ext u hu
+  rw [restrict_apply hu, restrict_apply hu, inter_comm t, inter_comm, inter_assoc,
+    measure_toMeasurable_inter (ht.inter hu) h]
+  congr 1
+  grind
+
+theorem restrict_toMeasurable (h : μ s ≠ ∞) : μ.restrict (toMeasurable μ s) = μ.restrict s := by
+  simpa using restrict_inter_toMeasurable h MeasurableSet.univ (subset_univ _)
 
 theorem restrict_eq_self_of_ae_mem {_m0 : MeasurableSpace α} ⦃s : Set α⦄ ⦃μ : Measure α⦄
     (hs : ∀ᵐ x ∂μ, x ∈ s) : μ.restrict s = μ :=

Mathlib/Topology/MetricSpace/Pseudo/Basic.lean

@@ -9,8 +9,7 @@ public import Mathlib.Data.ENNReal.Real
 public import Mathlib.Tactic.Bound.Attribute
 public import Mathlib.Topology.EMetricSpace.Basic
 public import Mathlib.Topology.MetricSpace.Pseudo.Defs
-
-import Mathlib.Topology.Metrizable.Basic
+public import Mathlib.Topology.Metrizable.Basic
 
 /-!
 ## Pseudo-metric spaces
@@ -205,23 +204,28 @@ end Real
 namespace Topology
 
 /-- The preimage of a separable set by an inducing map is separable. -/
-protected lemma IsInducing.isSeparable_preimage {f : β → α} [TopologicalSpace β]
+protected lemma IsInducing.isSeparable_preimage {α : Type*} [TopologicalSpace α]
+    [PseudoMetrizableSpace α] {f : β → α} [TopologicalSpace β]
     (hf : IsInducing f) {s : Set α} (hs : IsSeparable s) : IsSeparable (f ⁻¹' s) := by
+  letI : UniformSpace α := TopologicalSpace.pseudoMetrizableSpaceUniformity α
+  have := pseudoMetrizableSpaceUniformity_countably_generated
   have : SeparableSpace s := hs.separableSpace
   have : SecondCountableTopology s := UniformSpace.secondCountable_of_separable _
   have : IsInducing ((mapsTo_preimage f s).restrict _ _ _) :=
     (hf.comp IsInducing.subtypeVal).codRestrict _
   have := this.secondCountableTopology
   exact .of_subtype _
 
-protected theorem IsEmbedding.isSeparable_preimage {f : β → α} [TopologicalSpace β]
+protected theorem IsEmbedding.isSeparable_preimage {α : Type*} [TopologicalSpace α]
+    [PseudoMetrizableSpace α] {f : β → α} [TopologicalSpace β]
     (hf : IsEmbedding f) {s : Set α} (hs : IsSeparable s) : IsSeparable (f ⁻¹' s) :=
   hf.isInducing.isSeparable_preimage hs
 
 end Topology
 
 /-- A compact set is separable. -/
-theorem IsCompact.isSeparable {s : Set α} (hs : IsCompact s) : IsSeparable s :=
+theorem IsCompact.isSeparable {α : Type*} [TopologicalSpace α] [PseudoMetrizableSpace α]
+    {s : Set α} (hs : IsCompact s) : IsSeparable s :=
   haveI : CompactSpace s := isCompact_iff_compactSpace.mp hs
   .of_subtype s
 
@@ -270,7 +274,8 @@ lemma exists_finite_cover_balls_of_isCompact_closure (hs : IsCompact (closure s)
 end Compact
 
 /-- If a map is continuous on a separable set `s`, then the image of `s` is also separable. -/
-theorem ContinuousOn.isSeparable_image [TopologicalSpace β] {f : α → β} {s : Set α}
+theorem ContinuousOn.isSeparable_image {α : Type*} [TopologicalSpace α] [PseudoMetrizableSpace α]
+    [TopologicalSpace β] {f : α → β} {s : Set α}
     (hf : ContinuousOn f s) (hs : IsSeparable s) : IsSeparable (f '' s) := by
   rw [image_eq_range, ← image_univ]
   exact (isSeparable_univ_iff.2 hs.separableSpace).image hf.restrict