feat: the product of Borel spaces is Borel when either of them is sec…

…ond-countable (#6689)

We have currently that the product of two Borel spaces is Borel when both of them are second-countable. It is in fact sufficient to assume that only one of them is second-countable. We prove this in this PR.

Also move the definition of `SecondCountableEither` from `Function.StronglyMeasurable` to `BorelSpace.Basic` to be able to use it in the statement of the above theorem.

Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

@@ -86,9 +86,9 @@ namespace ContinuousLinearMap
 variable {𝕜 E F : Type*} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
   [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 
-theorem measurable_apply₂ [MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopology E]
-    [SecondCountableTopology (E →L[𝕜] F)] [MeasurableSpace F] [BorelSpace F] :
-    Measurable fun p : (E →L[𝕜] F) × E => p.1 p.2 :=
+theorem measurable_apply₂ [MeasurableSpace E] [OpensMeasurableSpace E]
+    [SecondCountableTopologyEither (E →L[𝕜] F) E]
+    [MeasurableSpace F] [BorelSpace F] : Measurable fun p : (E →L[𝕜] F) × E => p.1 p.2 :=
   isBoundedBilinearMapApply.continuous.measurable
 #align continuous_linear_map.measurable_apply₂ ContinuousLinearMap.measurable_apply₂
 

Mathlib/Analysis/Convolution.lean

@@ -737,7 +737,7 @@ theorem HasCompactSupport.continuous_convolution_right (hcg : HasCompactSupport
 
 /-- The convolution is continuous if one function is integrable and the other is bounded and
 continuous. -/
-theorem BddAbove.continuous_convolution_right_of_integrable [SecondCountableTopology G]
+theorem BddAbove.continuous_convolution_right_of_integrable [SecondCountableTopologyEither G E']
     (hbg : BddAbove (range fun x => ‖g x‖)) (hf : Integrable f μ) (hg : Continuous g) :
     Continuous (f ⋆[L, μ] g) := by
   refine' continuous_iff_continuousAt.mpr fun x₀ => _
@@ -823,7 +823,8 @@ theorem HasCompactSupport.continuous_convolution_left [FirstCountableTopology G]
   exact hcf.continuous_convolution_right L.flip hg hf
 #align has_compact_support.continuous_convolution_left HasCompactSupport.continuous_convolution_left
 
-theorem BddAbove.continuous_convolution_left_of_integrable [SecondCountableTopology G]
+theorem BddAbove.continuous_convolution_left_of_integrable
+    [FirstCountableTopology G] [SecondCountableTopologyEither G E]
     (hbf : BddAbove (range fun x => ‖f x‖)) (hf : Continuous f) (hg : Integrable g μ) :
     Continuous (f ⋆[L, μ] g) := by
   rw [← convolution_flip]

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -191,13 +191,15 @@ theorem Continuous.borel_measurable [TopologicalSpace α] [TopologicalSpace β]
 /-- A space with `MeasurableSpace` and `TopologicalSpace` structures such that
 all open sets are measurable. -/
 class OpensMeasurableSpace (α : Type*) [TopologicalSpace α] [h : MeasurableSpace α] : Prop where
+  /-- Borel-measurable sets are measurable. -/
   borel_le : borel α ≤ h
 #align opens_measurable_space OpensMeasurableSpace
 #align opens_measurable_space.borel_le OpensMeasurableSpace.borel_le
 
 /-- A space with `MeasurableSpace` and `TopologicalSpace` structures such that
 the `σ`-algebra of measurable sets is exactly the `σ`-algebra generated by open sets. -/
 class BorelSpace (α : Type*) [TopologicalSpace α] [MeasurableSpace α] : Prop where
+  /-- The measurable sets are exactly the Borel-measurable sets. -/
   measurable_eq : ‹MeasurableSpace α› = borel α
 #align borel_space BorelSpace
 #align borel_space.measurable_eq BorelSpace.measurable_eq
@@ -279,6 +281,12 @@ instance Subtype.opensMeasurableSpace {α : Type*} [TopologicalSpace α] [Measur
     exact comap_mono h.1⟩
 #align subtype.opens_measurable_space Subtype.opensMeasurableSpace
 
+lemma opensMeasurableSpace_iff_forall_measurableSet
+    [TopologicalSpace α] [MeasurableSpace α] :
+    OpensMeasurableSpace α ↔  (∀ (s : Set α), IsOpen s → MeasurableSet s) := by
+  refine ⟨fun h s hs ↦ ?_, fun h ↦ ⟨generateFrom_le h⟩⟩
+  exact OpensMeasurableSpace.borel_le _ <| GenerateMeasurable.basic _ hs
+
 instance (priority := 100) BorelSpace.countablyGenerated {α : Type*} [TopologicalSpace α]
     [MeasurableSpace α] [BorelSpace α] [SecondCountableTopology α] : CountablyGenerated α := by
   obtain ⟨b, bct, -, hb⟩ := exists_countable_basis α
@@ -398,15 +406,73 @@ instance Pi.opensMeasurableSpace {ι : Type*} {π : ι → Type*} [Countable ι]
   exact .basic _ (hi a ha)
 #align pi.opens_measurable_space Pi.opensMeasurableSpace
 
-instance Prod.opensMeasurableSpace [SecondCountableTopology α] [SecondCountableTopology β] :
+/-- The typeclass `SecondCountableTopologyEither α β` registers the fact that at least one of
+the two spaces has second countable topology. This is the right assumption to ensure that continuous
+maps from `α` to `β` are strongly measurable. -/
+class SecondCountableTopologyEither (α β : Type*) [TopologicalSpace α] [TopologicalSpace β] :
+  Prop where
+  /-- The projection out of `SecondCountableTopologyEither` -/
+  out : SecondCountableTopology α ∨ SecondCountableTopology β
+#align second_countable_topology_either SecondCountableTopologyEither
+
+instance (priority := 100) secondCountableTopologyEither_of_left (α β : Type*) [TopologicalSpace α]
+    [TopologicalSpace β] [SecondCountableTopology α] : SecondCountableTopologyEither α β
+    where out := Or.inl (by infer_instance)
+#align second_countable_topology_either_of_left secondCountableTopologyEither_of_left
+
+instance (priority := 100) secondCountableTopologyEither_of_right (α β : Type*)
+    [TopologicalSpace α] [TopologicalSpace β] [SecondCountableTopology β] :
+    SecondCountableTopologyEither α β where out := Or.inr (by infer_instance)
+#align second_countable_topology_either_of_right secondCountableTopologyEither_of_right
+
+/-- If either `α` or `β` has second-countable topology, then the open sets in `α × β` belong to the
+product sigma-algebra. -/
+instance Prod.opensMeasurableSpace [h : SecondCountableTopologyEither α β] :
     OpensMeasurableSpace (α × β) := by
-  constructor
-  rw [((isBasis_countableBasis α).prod (isBasis_countableBasis β)).borel_eq_generateFrom]
-  apply generateFrom_le
-  rintro _ ⟨u, v, hu, hv, rfl⟩
-  exact (isOpen_of_mem_countableBasis hu).measurableSet.prod
-    (isOpen_of_mem_countableBasis hv).measurableSet
-#align prod.opens_measurable_space Prod.opensMeasurableSpace
+  apply opensMeasurableSpace_iff_forall_measurableSet.2 (fun s hs ↦ ?_)
+  rcases h.out with hα|hβ
+  · let F : Set α → Set β := fun a ↦ {y | ∃ b, IsOpen b ∧ y ∈ b ∧ a ×ˢ b ⊆ s}
+    have A : ∀ a, IsOpen (F a) := by
+      intro a
+      apply isOpen_iff_forall_mem_open.2
+      rintro y ⟨b, b_open, yb, hb⟩
+      exact ⟨b, fun z zb ↦ ⟨b, b_open, zb, hb⟩, b_open, yb⟩
+    have : s = ⋃ a ∈ countableBasis α, a ×ˢ F a := by
+      apply Subset.antisymm
+      · rintro ⟨y1, y2⟩ hy
+        rcases isOpen_prod_iff.1 hs y1 y2 hy with ⟨u, v, u_open, v_open, yu, yv, huv⟩
+        obtain ⟨a, ha, ya, au⟩ : ∃ a ∈ countableBasis α, y1 ∈ a ∧ a ⊆ u :=
+          IsTopologicalBasis.exists_subset_of_mem_open (isBasis_countableBasis α) yu u_open
+        simp only [mem_iUnion, mem_prod, mem_setOf_eq, exists_and_left, exists_prop]
+        exact ⟨a, ya, ha, v, v_open, yv, (Set.prod_mono_left au).trans huv⟩
+      · rintro ⟨y1, y2⟩ hy
+        simp only [mem_iUnion, mem_prod, mem_setOf_eq, exists_and_left, exists_prop] at hy
+        rcases hy with ⟨a, ya, -, b, -, yb, hb⟩
+        exact hb (mem_prod.2 ⟨ya, yb⟩)
+    rw [this]
+    apply MeasurableSet.biUnion (countable_countableBasis α) (fun a ha ↦ ?_)
+    exact (isOpen_of_mem_countableBasis ha).measurableSet.prod (A a).measurableSet
+  · let F : Set β → Set α := fun a ↦ {y | ∃ b, IsOpen b ∧ y ∈ b ∧ b ×ˢ a ⊆ s}
+    have A : ∀ a, IsOpen (F a) := by
+      intro a
+      apply isOpen_iff_forall_mem_open.2
+      rintro y ⟨b, b_open, yb, hb⟩
+      exact ⟨b, fun z zb ↦ ⟨b, b_open, zb, hb⟩, b_open, yb⟩
+    have : s = ⋃ a ∈ countableBasis β, F a ×ˢ a := by
+      apply Subset.antisymm
+      · rintro ⟨y1, y2⟩ hy
+        rcases isOpen_prod_iff.1 hs y1 y2 hy with ⟨u, v, u_open, v_open, yu, yv, huv⟩
+        obtain ⟨a, ha, ya, au⟩ : ∃ a ∈ countableBasis β, y2 ∈ a ∧ a ⊆ v :=
+          IsTopologicalBasis.exists_subset_of_mem_open (isBasis_countableBasis β) yv v_open
+        simp only [mem_iUnion, mem_prod, mem_setOf_eq, exists_and_left, exists_prop]
+        exact ⟨a, ⟨u, u_open, yu, (Set.prod_mono_right au).trans huv⟩, ha, ya⟩
+      · rintro ⟨y1, y2⟩ hy
+        simp only [mem_iUnion, mem_prod, mem_setOf_eq, exists_and_left, exists_prop] at hy
+        rcases hy with ⟨a, ⟨b, -, yb, hb⟩, -, ya⟩
+        exact hb (mem_prod.2 ⟨yb, ya⟩)
+    rw [this]
+    apply MeasurableSet.biUnion (countable_countableBasis β) (fun a ha ↦ ?_)
+    exact (A a).measurableSet.prod (isOpen_of_mem_countableBasis ha).measurableSet
 
 variable {α' : Type*} [TopologicalSpace α'] [MeasurableSpace α']
 
@@ -943,13 +1009,13 @@ theorem measurable_of_continuousOn_compl_singleton [T1Space α] {f : α → γ}
     (continuousOn_iff_continuous_restrict.1 hf).measurable
 #align measurable_of_continuous_on_compl_singleton measurable_of_continuousOn_compl_singleton
 
-theorem Continuous.measurable2 [SecondCountableTopology α] [SecondCountableTopology β] {f : δ → α}
+theorem Continuous.measurable2 [SecondCountableTopologyEither α β] {f : δ → α}
     {g : δ → β} {c : α → β → γ} (h : Continuous fun p : α × β => c p.1 p.2) (hf : Measurable f)
     (hg : Measurable g) : Measurable fun a => c (f a) (g a) :=
   h.measurable.comp (hf.prod_mk hg)
 #align continuous.measurable2 Continuous.measurable2
 
-theorem Continuous.aemeasurable2 [SecondCountableTopology α] [SecondCountableTopology β]
+theorem Continuous.aemeasurable2 [SecondCountableTopologyEither α β]
     {f : δ → α} {g : δ → β} {c : α → β → γ} {μ : Measure δ}
     (h : Continuous fun p : α × β => c p.1 p.2) (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
     AEMeasurable (fun a => c (f a) (g a)) μ :=
@@ -974,9 +1040,9 @@ instance (priority := 100) ContinuousSub.measurableSub₂ [SecondCountableTopolo
 #align has_continuous_sub.has_measurable_sub₂ ContinuousSub.measurableSub₂
 
 instance (priority := 100) ContinuousSMul.measurableSMul₂ {M α} [TopologicalSpace M]
-    [SecondCountableTopology M] [MeasurableSpace M] [OpensMeasurableSpace M] [TopologicalSpace α]
-    [SecondCountableTopology α] [MeasurableSpace α] [BorelSpace α] [SMul M α] [ContinuousSMul M α] :
-    MeasurableSMul₂ M α :=
+    [MeasurableSpace M] [OpensMeasurableSpace M] [TopologicalSpace α]
+    [SecondCountableTopologyEither M α] [MeasurableSpace α] [BorelSpace α] [SMul M α]
+    [ContinuousSMul M α] : MeasurableSMul₂ M α :=
   ⟨continuous_smul.measurable⟩
 #align has_continuous_smul.has_measurable_smul₂ ContinuousSMul.measurableSMul₂
 
@@ -1010,7 +1076,7 @@ instance Pi.borelSpace {ι : Type*} {π : ι → Type*} [Countable ι] [∀ i, T
   ⟨le_antisymm pi_le_borel_pi OpensMeasurableSpace.borel_le⟩
 #align pi.borel_space Pi.borelSpace
 
-instance Prod.borelSpace [SecondCountableTopology α] [SecondCountableTopology β] :
+instance Prod.borelSpace [SecondCountableTopologyEither α β] :
     BorelSpace (α × β) :=
   ⟨le_antisymm prod_le_borel_prod OpensMeasurableSpace.borel_le⟩
 #align prod.borel_space Prod.borelSpace

Mathlib/MeasureTheory/Function/AEEqFun.lean

@@ -390,8 +390,8 @@ theorem coeFn_comp₂ (g : β → γ → δ) (hg : Continuous (uncurry g)) (f₁
 
 section
 
-variable [MeasurableSpace β] [PseudoMetrizableSpace β] [BorelSpace β] [SecondCountableTopology β]
-  [MeasurableSpace γ] [PseudoMetrizableSpace γ] [BorelSpace γ] [SecondCountableTopology γ]
+variable [MeasurableSpace β] [PseudoMetrizableSpace β] [BorelSpace β]
+  [MeasurableSpace γ] [PseudoMetrizableSpace γ] [BorelSpace γ] [SecondCountableTopologyEither β γ]
   [MeasurableSpace δ] [PseudoMetrizableSpace δ] [OpensMeasurableSpace δ] [SecondCountableTopology δ]
 
 /-- Given a measurable function `g : β → γ → δ`, and almost everywhere equal functions
@@ -468,8 +468,8 @@ theorem comp₂_toGerm (g : β → γ → δ) (hg : Continuous (uncurry g)) (f
   induction_on₂ f₁ f₂ fun f₁ _ f₂ _ => by simp
 #align measure_theory.ae_eq_fun.comp₂_to_germ MeasureTheory.AEEqFun.comp₂_toGerm
 
-theorem comp₂Measurable_toGerm [PseudoMetrizableSpace β] [SecondCountableTopology β]
-    [MeasurableSpace β] [BorelSpace β] [PseudoMetrizableSpace γ] [SecondCountableTopology γ]
+theorem comp₂Measurable_toGerm [PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β]
+    [PseudoMetrizableSpace γ] [SecondCountableTopologyEither β γ]
     [MeasurableSpace γ] [BorelSpace γ] [PseudoMetrizableSpace δ] [SecondCountableTopology δ]
     [MeasurableSpace δ] [OpensMeasurableSpace δ] (g : β → γ → δ) (hg : Measurable (uncurry g))
     (f₁ : α →ₘ[μ] β) (f₂ : α →ₘ[μ] γ) :

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -64,25 +64,6 @@ open MeasureTheory Filter TopologicalSpace Function Set MeasureTheory.Measure
 
 open ENNReal Topology MeasureTheory NNReal BigOperators
 
-/-- The typeclass `SecondCountableTopologyEither α β` registers the fact that at least one of
-the two spaces has second countable topology. This is the right assumption to ensure that continuous
-maps from `α` to `β` are strongly measurable. -/
-class SecondCountableTopologyEither (α β : Type*) [TopologicalSpace α] [TopologicalSpace β] :
-  Prop where
-  /-- The projection out of `SecondCountableTopologyEither` -/
-  out : SecondCountableTopology α ∨ SecondCountableTopology β
-#align second_countable_topology_either SecondCountableTopologyEither
-
-instance (priority := 100) secondCountableTopologyEither_of_left (α β : Type*) [TopologicalSpace α]
-    [TopologicalSpace β] [SecondCountableTopology α] : SecondCountableTopologyEither α β
-    where out := Or.inl (by infer_instance)
-#align second_countable_topology_either_of_left secondCountableTopologyEither_of_left
-
-instance (priority := 100) secondCountableTopologyEither_of_right (α β : Type*)
-    [TopologicalSpace α] [TopologicalSpace β] [SecondCountableTopology β] :
-    SecondCountableTopologyEither α β where out := Or.inr (by infer_instance)
-#align second_countable_topology_either_of_right secondCountableTopologyEither_of_right
-
 variable {α β γ ι : Type*} [Countable ι]
 
 namespace MeasureTheory