feat(MeasureTheory/Measure/Tight): tightness of marginals implies tightness on product space (leanprover-community#39501)

This PR introduces `IsTightMeasureSet.prodMk`, which says that a set of measures on a product space is tight if both sets of marginals are tight. This is useful when proving weak compactness of probability measures on product spaces (via Prokhorov).

The proof makes use of `isTightMeasureSet_iff_exists_isCompact_measure_compl_le` and then proceeds in the conventional way. I also tried to write a purely filter-theoretic proof, but did not really succeed and it was nowhere near as simple as the direct proof.

Author: jvanwinden

Mathlib/MeasureTheory/Measure/Tight.lean

@@ -145,6 +145,24 @@ lemma map [TopologicalSpace 𝓨] [MeasurableSpace 𝓨] [OpensMeasurableSpace 
   simp only [preimage_compl, compl_subset_compl]
   exact subset_preimage_image f K
 
+/-- A set of measures on a product space is tight if both marginals are tight. -/
+lemma prodMk {m𝓨 : MeasurableSpace 𝓨} [TopologicalSpace 𝓨] {μ : Set (Measure (𝓧 × 𝓨))}
+    (hμ₁ : IsTightMeasureSet (Measure.fst '' μ)) (hμ₂ : IsTightMeasureSet (Measure.snd '' μ)) :
+    IsTightMeasureSet μ := by
+  rw [isTightMeasureSet_iff_exists_isCompact_measure_compl_le] at hμ₁ hμ₂ ⊢
+  intro ε hε
+  obtain ⟨K₁, hK₁_compact, hK₁_le⟩ := hμ₁ (ε / 2) (by aesop)
+  obtain ⟨K₂, hK₂_compact, hK₂_le⟩ := hμ₂ (ε / 2) (by aesop)
+  refine ⟨K₁ ×ˢ K₂, hK₁_compact.prod hK₂_compact, fun κ hκ_mem ↦ ?_⟩
+  grw [compl_prod_eq_union, measure_union_le, ← ENNReal.add_halves (a := ε)]
+  apply add_le_add
+  · specialize hK₁_le _ <| mem_image_of_mem _ hκ_mem
+    grw [Measure.fst, ← Measure.le_map_apply (by fun_prop)] at hK₁_le
+    simpa [prod_univ] using hK₁_le
+  · specialize hK₂_le _ <| Set.mem_image_of_mem _ hκ_mem
+    grw [Measure.snd, ← Measure.le_map_apply (by fun_prop)] at hK₂_le
+    simpa [univ_prod] using hK₂_le
+
 end IsTightMeasureSet
 end Basic