feat: the product of vector measures (leanprover-community#41546)

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

Author: sgouezel

Mathlib.lean

@@ -5663,6 +5663,7 @@ public import Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
 public import Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
 public import Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
 public import Mathlib.MeasureTheory.VectorMeasure.Integral
+public import Mathlib.MeasureTheory.VectorMeasure.Prod
 public import Mathlib.MeasureTheory.VectorMeasure.SetIntegral
 public import Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
 public import Mathlib.MeasureTheory.VectorMeasure.Variation.Defs

Mathlib/MeasureTheory/VectorMeasure/Basic.lean

@@ -133,12 +133,30 @@ theorem hasSum_of_disjoint_iUnion (hm : ∀ i, MeasurableSet (f i)) (hd : Pairwi
   · simp [Function.apply_extend MeasurableSet, Function.comp_def, hm]
   · exact hd.disjoint_extend_bot (he.factorsThrough _)
 
+theorem of_if {ι : Type*} {x : ι} {B : Set ι} {A : Set α} [Decidable (x ∈ B)] :
+    v (if x ∈ B then A else ∅) = indicator B (fun _ => v A) x := by
+  split_ifs with h <;> simp [h]
+
 variable [T2Space M]
 
 theorem of_disjoint_iUnion (hm : ∀ i, MeasurableSet (f i)) (hd : Pairwise (Disjoint on f)) :
     v (⋃ i, f i) = ∑' i, v (f i) :=
   (hasSum_of_disjoint_iUnion hm hd).tsum_eq.symm
 
+theorem of_biUnion {ι : Type*} {s : Set ι} {f : ι → Set α} (hs : s.Countable)
+    (hd : s.Pairwise (Disjoint on f)) (h : ∀ b ∈ s, MeasurableSet (f b)) :
+    v (⋃ b ∈ s, f b) = ∑' p : s, v (f p) := by
+  haveI := hs.toEncodable
+  rw [biUnion_eq_iUnion]
+  apply of_disjoint_iUnion
+  · exact fun x ↦ h x x.2
+  · exact hd.on_injective Subtype.coe_injective fun x => x.2
+
+theorem of_biUnion_finset {ι : Type*} {s : Finset ι} {f : ι → Set α} (hd : PairwiseDisjoint (↑s) f)
+    (hm : ∀ b ∈ s, MeasurableSet (f b)) : v (⋃ b ∈ s, f b) = ∑ p ∈ s, v (f p) := by
+  rw [← Finset.sum_attach, Finset.attach_eq_univ, ← tsum_fintype (L := .unconditional s)]
+  exact of_biUnion s.countable_toSet hd hm
+
 theorem of_union {A B : Set α} (h : Disjoint A B) (hA : MeasurableSet A) (hB : MeasurableSet B) :
     v (A ∪ B) = v A + v B := by
   rw [Set.union_eq_iUnion, of_disjoint_iUnion, tsum_fintype, Fintype.sum_bool, cond, cond]
@@ -206,22 +224,6 @@ theorem of_nonpos_disjoint_union_eq_zero {s : SignedMeasure α} {A B : Set α} (
   rw [of_union h hA₁ hB₁] at hAB
   linarith
 
-lemma of_biUnion_finset {ι : Type*} {s : Finset ι} {f : ι → Set α} (hd : PairwiseDisjoint (↑s) f)
-    (hm : ∀ b ∈ s, MeasurableSet (f b)) : v (⋃ b ∈ s, f b) = ∑ p ∈ s, v (f p) := by
-  classical
-  induction s using Finset.induction with
-  | empty => simp
-  | insert a s has ih =>
-    simp only [Finset.mem_insert, iUnion_iUnion_eq_or_left, has, not_false_eq_true,
-      Finset.sum_insert]
-    rw [of_union, ih]
-    · exact hd.subset (by simp)
-    · grind
-    · simp only [disjoint_iUnion_right]
-      exact fun i hi ↦ hd (by simp) (by simp [hi]) (by grind)
-    · apply hm _ (by simp)
-    · apply Finset.measurableSet_biUnion _ (by grind)
-
 theorem tendsto_vectorMeasure_iUnion_atTop_nat
     {s : ℕ → Set α} (hm : Monotone s) (hs : ∀ i, MeasurableSet (s i)) :
     Tendsto (fun n ↦ v (s n)) atTop (𝓝 (v (⋃ n, s n))) := by
@@ -250,6 +252,22 @@ theorem tendsto_vectorMeasure_iInter_atTop_nat
   exact tendsto_vectorMeasure_iUnion_atTop_nat (fun i j hij ↦ by simpa using hm hij)
     (fun i ↦ (hs i).compl)
 
+/-- If two vector measures give the same mass to the whole space and coincide on a
+generating π-system, then they coincide. -/
+theorem ext_of_generateFrom {M : Type*} [AddCommGroup M] [TopologicalSpace M] [T2Space M]
+    {X : Type*} {mX : MeasurableSpace X} {μ ν : VectorMeasure X M}
+    (C : Set (Set X)) (hμν : ∀ s ∈ C, μ s = ν s)
+    (hA : mX = MeasurableSpace.generateFrom C) (hC : IsPiSystem C)
+    (h_univ : μ Set.univ = ν Set.univ) : μ = ν := by
+  ext s hs
+  induction s, hs using MeasurableSpace.induction_on_inter hA hC with
+  | empty => simp
+  | basic t ht => exact hμν t ht
+  | compl t htm iht =>
+    simp [of_compl, iht, htm, h_univ]
+  | iUnion f hfd hfm ihf =>
+    simp [of_disjoint_iUnion, hfm, hfd, ihf]
+
 end
 
 section SMul
@@ -714,6 +732,12 @@ theorem restrict_apply {i : Set α} (hi : MeasurableSet i) {j : Set α} (hj : Me
   rw [restrict, dif_pos hi]
   exact if_pos hj
 
+@[simp] theorem restrict_apply_univ {i : Set α} :
+    v.restrict i univ = v i := by
+  by_cases hi : MeasurableSet i
+  · simp [restrict_apply, hi]
+  · simp [restrict_not_measurable, hi]
+
 theorem restrict_eq_self {i : Set α} (hi : MeasurableSet i) {j : Set α} (hj : MeasurableSet j)
     (hij : j ⊆ i) : v.restrict i j = v j := by
   rw [restrict_apply v hi hj, Set.inter_eq_left.2 hij]

Mathlib/MeasureTheory/VectorMeasure/Prod.lean

@@ -0,0 +1,197 @@
+/-
+Copyright (c) 2026 Sébastien Gouëzel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sébastien Gouëzel
+-/
+module
+
+public import Mathlib.MeasureTheory.Integral.Prod
+public import Mathlib.MeasureTheory.VectorMeasure.SetIntegral
+public import Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
+
+/-!
+# Product of vector measures
+
+Given two vector measures, we define their product `μ.prod ν B` as the vector measure assigning
+to a measurable product `s × t` the mass `B (μ s) (ν t)`, if such a vector measure exists.
+We show that it exists when either `μ` or `ν` has finite variation.
+
+The API is modelled on the one for the product of positive measures.
+-/
+
+public section
+
+open Filter Function MeasureTheory RCLike Set TopologicalSpace Topology
+open scoped ENNReal NNReal Finset
+
+variable {ι X Y E F G H I J : Type*} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
+  [NormedAddCommGroup E] [NormedSpace ℝ E]
+  [NormedAddCommGroup F] [NormedSpace ℝ F]
+  [NormedAddCommGroup G] [NormedSpace ℝ G]
+  [NormedAddCommGroup H] [NormedSpace ℝ H]
+  [NormedAddCommGroup I] [NormedSpace ℝ I]
+  [NormedAddCommGroup J] [NormedSpace ℝ J]
+  {μ : VectorMeasure X E} {ν : VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G}
+
+namespace MeasureTheory.VectorMeasure
+
+/-- Two vector measures `μ` and `ν` have a product with respect to `B` if there exists a
+measure giving mass `B (μ s) (ν t)` to any measurable product set `s × t`.
+This is satisfied whenever `μ` or `ν` has finite variation. -/
+class HasProd (μ : VectorMeasure X E) (ν : VectorMeasure Y F) (B : E →L[ℝ] F →L[ℝ] G) : Prop where
+  exists_prod : ∃ ρ : VectorMeasure (X × Y) G, ∀ (s : Set X) (t : Set Y),
+    MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = B (μ s) (ν t)
+
+/-- The product of two vector measures `μ` and `ν` with respect to a continuous bilinear map `B`,
+giving mass `B (μ s) (ν t)` to any measurable product set `s × t`.
+If such a measure does not exist, we use the junk value `0`. -/
+noncomputable def prod (μ : VectorMeasure X E) (ν : VectorMeasure Y F) (B : E →L[ℝ] F →L[ℝ] G) :
+    VectorMeasure (X × Y) G :=
+  open scoped Classical in if h : HasProd μ ν B then h.exists_prod.choose else 0
+
+lemma prod_eq_zero_of_not_hasProd (h : ¬HasProd μ ν B) :
+    μ.prod ν B = 0 := by
+  grind [HasProd, prod]
+
+@[simp] lemma prod_apply [h : HasProd μ ν B] {s : Set X} {t : Set Y} :
+    μ.prod ν B (s ×ˢ t) = B (μ s) (ν t) := by
+  rcases eq_or_ne s ∅ with rfl | hs
+  · simp
+  rcases eq_or_ne t ∅ with rfl | ht
+  · simp
+  by_cases h's : MeasurableSet s; swap
+  · simp only [h's, not_false_eq_true, not_measurable, _root_.map_zero, _root_.zero_apply]
+    rw [not_measurable]
+    simp [measurableSet_prod, hs, ht, h's]
+  by_cases h't : MeasurableSet t; swap
+  · simp only [h't, not_false_eq_true, not_measurable, _root_.map_zero]
+    rw [not_measurable]
+    simp [measurableSet_prod, hs, ht, h't]
+  simpa [prod, h] using h.exists_prod.choose_spec s t h's h't
+
+lemma HasProd.flip [HasProd μ ν B] : HasProd ν μ B.flip where
+  exists_prod := by
+    refine ⟨(μ.prod ν B).map Prod.swap, fun s t hs ht ↦ ?_⟩
+    rw [map_apply _ (by fun_prop) (hs.prod ht)]
+    simp
+
+lemma hasProd_flip_iff : HasProd ν μ B.flip ↔ HasProd μ ν B :=
+  ⟨fun h ↦ by simpa using HasProd.flip (μ := ν) (ν := μ) (B := B.flip), fun h ↦ HasProd.flip⟩
+
+omit [NormedSpace ℝ F] in
+/-- If `ν` is a vector measure, and `s ⊆ X × Y` is measurable, then `x ↦ ν { y | (x, y) ∈ s }` is
+a strongly measurable function. -/
+theorem stronglyMeasurable_vectorMeasure_prodMk_left {s : Set (X × Y)}
+    (hs : MeasurableSet s) : StronglyMeasurable fun x ↦ ν (Prod.mk x ⁻¹' s) := by
+  induction s, hs
+    using MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod with
+  | empty => simp [stronglyMeasurable_const]
+  | basic s hs =>
+    obtain ⟨s, hs, t, -, rfl⟩ := hs
+    classical
+    simpa [mk_preimage_prod_right_eq_if, of_if] using stronglyMeasurable_const.indicator hs
+  | compl s hs ihs =>
+    simp_rw [preimage_compl, VectorMeasure.of_compl (measurable_prodMk_left hs)]
+    exact stronglyMeasurable_const.sub ihs
+  | iUnion f hfd hfm ihf =>
+    have (a : X) : HasSum (fun i ↦ ν (Prod.mk a ⁻¹' f i)) (ν (Prod.mk a ⁻¹' ⋃ i, f i)) := by
+      rw [preimage_iUnion]
+      apply hasSum_of_disjoint_iUnion
+      exacts [fun i ↦ measurable_prodMk_left (hfm i), hfd.mono fun _ _ ↦ .preimage _]
+    exact StronglyMeasurable.hasSum ihf this
+
+omit [NormedSpace ℝ E] in
+theorem integrable_vectorMeasure_prodMk_left [IsFiniteMeasure μ.variation]
+    {s : Set (X × Y)} (hs : MeasurableSet s) :
+    μ.Integrable fun x ↦ ν (Prod.mk x ⁻¹' s) := by
+  refine Integrable.of_bound (μ := μ.variation) ?_ ν.bound ?_
+  · exact (stronglyMeasurable_vectorMeasure_prodMk_left hs).aestronglyMeasurable
+  · exact Eventually.of_forall (fun x ↦ norm_apply_le_bound)
+
+/-- The product of two vector measures when the first one has finite variation, obtained by
+integrating the measure of the fibers, as in the definition of the product of positive measures.
+*Do not use*: This is only used to instantiate the typeclass `HasProd`. Instead, use `μ.prod ν B`,
+which uses the typeclass instance. -/
+private noncomputable def prodOfIsFiniteMeasureLeft
+    (μ : VectorMeasure X E) (ν : VectorMeasure Y F) (B : E →L[ℝ] F →L[ℝ] G)
+    [IsFiniteMeasure μ.variation] :
+    VectorMeasure (X × Y) G where
+  measureOf' s := open scoped Classical in
+    if MeasurableSet s then ∫ᵛ x, ν (Prod.mk x ⁻¹' s) ∂[B.flip; μ] else 0
+  empty' := by simp
+  not_measurable' := by simp +contextual
+  m_iUnion' f f_meas f_disj := by
+    simp only [f_meas, ↓reduceIte, implies_true, MeasurableSet.iUnion, preimage_iUnion,
+      HasSum, SummationFilter.unconditional_filter]
+    have A (a : Finset ℕ) : ∑ y ∈ a, ∫ᵛ x, ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ]
+        = ∫ᵛ x, ∑ y ∈ a, ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ] := by
+      rw [integral_finsetSum _ (fun i hi ↦ integrable_vectorMeasure_prodMk_left (f_meas i))]
+    simp_rw [A]
+    apply tendsto_integral_filter_of_dominated_convergence (bound := fun x ↦ ν.bound)
+    · apply Eventually.of_forall (fun a ↦ ?_)
+      apply StronglyMeasurable.aestronglyMeasurable
+      apply Finset.stronglyMeasurable_fun_sum _ (fun i hi ↦ ?_)
+      apply stronglyMeasurable_vectorMeasure_prodMk_left (f_meas i)
+    · filter_upwards with a
+      filter_upwards with x
+      rw [← VectorMeasure.of_biUnion_finset]
+      · apply norm_apply_le_bound
+      · exact fun i hi j hj hij ↦ (f_disj hij).preimage _
+      · exact fun i hi ↦ measurable_prodMk_left (f_meas i)
+    · apply integrable_const
+    · filter_upwards with x
+      apply hasSum_of_disjoint_iUnion
+      · exact fun i ↦ measurable_prodMk_left (f_meas i)
+      · exact fun i j hij ↦ (f_disj hij).preimage _
+
+instance [CompleteSpace G] [IsFiniteMeasure μ.variation] : HasProd μ ν B where
+  exists_prod := by
+    classical
+    refine ⟨prodOfIsFiniteMeasureLeft μ ν B, fun s t hs ht ↦ ?_⟩
+    simp [prodOfIsFiniteMeasureLeft, hs.prod ht, ↓reduceIte, mk_preimage_prod_right_eq_if,
+      of_if, integral_indicator hs, ContinuousLinearMap.flip_apply, hs, restrict_apply]
+
+instance [CompleteSpace G] [h : IsFiniteMeasure ν.variation] : HasProd μ ν B :=
+  hasProd_flip_iff.1 inferInstance
+
+lemma prod_eq_of_forall_apply_prod {ρ : VectorMeasure (X × Y) G} (hρ : ∀ (s : Set X) (t : Set Y),
+    MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = B (μ s) (ν t)) :
+    μ.prod ν B = ρ := by
+  have : HasProd μ ν B := ⟨ρ, hρ⟩
+  apply ext_of_generateFrom _ _ generateFrom_prod.symm isPiSystem_prod
+  · rw [← univ_prod_univ, hρ _ _ MeasurableSet.univ MeasurableSet.univ, prod_apply]
+  · rintro - ⟨s, hs, t, ht, rfl⟩
+    rw [prod_apply, hρ _ _ hs ht]
+
+lemma prod_apply_eq_integral [CompleteSpace G] [IsFiniteMeasure μ.variation]
+    {s : Set (X × Y)} (hs : MeasurableSet s) :
+    μ.prod ν B s = ∫ᵛ x, ν (Prod.mk x ⁻¹' s) ∂[B.flip; μ] := by
+  have : μ.prod ν B = prodOfIsFiniteMeasureLeft μ ν B := by
+    classical
+    apply prod_eq_of_forall_apply_prod (fun s t hs ht ↦ ?_)
+    simp [prodOfIsFiniteMeasureLeft, hs.prod ht, ↓reduceIte, mk_preimage_prod_right_eq_if,
+      of_if, integral_indicator hs, ContinuousLinearMap.flip_apply, restrict_apply, hs]
+  rw [this]
+  simp [prodOfIsFiniteMeasureLeft, hs]
+
+lemma prod_flip_apply_eq_integral [CompleteSpace G] [IsFiniteMeasure μ.variation]
+    {B : F →L[ℝ] E →L[ℝ] G} {s : Set (X × Y)} (hs : MeasurableSet s) :
+    μ.prod ν B.flip s = ∫ᵛ x, ν (Prod.mk x ⁻¹' s) ∂[B; μ] := by
+  simp [prod_apply_eq_integral hs]
+
+lemma variation_prod_le [CompleteSpace G] [IsFiniteMeasure μ.variation] [SFinite ν.variation] :
+    (μ.prod ν B).variation ≤ ‖B‖ₑ • μ.variation.prod ν.variation := by
+  apply variation_le_of_forall_enorm_le (fun s hs ↦ ?_)
+  rw [prod_apply_eq_integral hs]
+  simp only [Measure.smul_apply, smul_eq_mul, Measure.prod_apply hs]
+  grw [enorm_integral_le_lintegral_enorm, ContinuousLinearMap.opENorm_flip,
+    enorm_measure_le_variation]
+
+instance [CompleteSpace G] [IsFiniteMeasure μ.variation] [IsFiniteMeasure ν.variation] :
+    IsFiniteMeasure (μ.prod ν B).variation := by
+  have : IsFiniteMeasure (‖B‖ₑ • μ.variation.prod ν.variation) := by
+    simp only [enorm_eq_nnnorm, Measure.coe_nnreal_smul]
+    infer_instance
+  exact isFiniteMeasure_of_le _ variation_prod_le
+
+end MeasureTheory.VectorMeasure