feat: add instances about volume (#4628)

Lean 3 was able to apply, e.g., instances about `measure_theory.measure.prod` to the volume on the Cartesian product. Lean 4 can't do this, so we need to duplicate many instances. Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com> Co-authored-by: Komyyy <pol_tta@outlook.jp>
leanprover-community · Jun 4, 2023 · 9a28a6c · 9a28a6c
1 parent 6ab2e35
commit 9a28a6c
Show file tree

Hide file tree

Showing 4 changed files with 92 additions and 28 deletions.
diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean
@@ -307,6 +307,13 @@ protected irreducible_def pi : Measure (∀ i, α i) :=
   toMeasure (OuterMeasure.pi fun i => (μ i).toOuterMeasure) (pi_caratheodory μ)
 #align measure_theory.measure.pi MeasureTheory.Measure.pi
 
+-- porting note: moved from below so that instances about `Measure.pi` and `MeasureSpace.pi`
+-- go together
+instance _root_.MeasureTheory.MeasureSpace.pi {α : ι → Type _} [∀ i, MeasureSpace (α i)] :
+    MeasureSpace (∀ i, α i) :=
+  ⟨Measure.pi fun _ => volume⟩
+#align measure_theory.measure_space.pi MeasureTheory.MeasureSpace.pi
+
 theorem pi_pi_aux [∀ i, SigmaFinite (μ i)] (s : ∀ i, Set (α i)) (hs : ∀ i, MeasurableSet (s i)) :
     Measure.pi μ (pi univ s) = ∏ i, μ i (s i) := by
   refine' le_antisymm _ _
@@ -409,6 +416,10 @@ instance pi.sigmaFinite : SigmaFinite (Measure.pi μ) :=
   (FiniteSpanningSetsIn.pi fun i => (μ i).toFiniteSpanningSetsIn).sigmaFinite
 #align measure_theory.measure.pi.sigma_finite MeasureTheory.Measure.pi.sigmaFinite
 
+instance {α : ι → Type _} [∀ i, MeasureSpace (α i)] [∀ i, SigmaFinite (volume : Measure (α i))] :
+    SigmaFinite (volume : Measure (∀ i, α i)) :=
+  pi.sigmaFinite _
+
 theorem pi_of_empty {α : Type _} [IsEmpty α] {β : α → Type _} {m : ∀ a, MeasurableSpace (β a)}
     (μ : ∀ a : α, Measure (β a)) (x : ∀ a, β a := isEmptyElim) : Measure.pi μ = dirac x := by
   haveI : ∀ a, SigmaFinite (μ a) := isEmptyElim
@@ -538,17 +549,29 @@ theorem pi_noAtoms (i : ι) [NoAtoms (μ i)] : NoAtoms (Measure.pi μ) :=
   ⟨fun x => flip measure_mono_null (pi_hyperplane μ i (x i)) (singleton_subset_iff.2 rfl)⟩
 #align measure_theory.measure.pi_has_no_atoms MeasureTheory.Measure.pi_noAtoms
 
-instance [h : Nonempty ι] [∀ i, NoAtoms (μ i)] : NoAtoms (Measure.pi μ) :=
+instance pi_noAtoms' [h : Nonempty ι] [∀ i, NoAtoms (μ i)] : NoAtoms (Measure.pi μ) :=
   h.elim fun i => pi_noAtoms i
 
-instance [∀ i, TopologicalSpace (α i)] [∀ i, IsLocallyFiniteMeasure (μ i)] :
+instance {α : ι → Type _} [Nonempty ι] [∀ i, MeasureSpace (α i)]
+    [∀ i, SigmaFinite (volume : Measure (α i))] [∀ i, NoAtoms (volume : Measure (α i))] :
+    NoAtoms (volume : Measure (∀ i, α i)) :=
+  pi_noAtoms'
+
+instance pi.isLocallyFiniteMeasure
+    [∀ i, TopologicalSpace (α i)] [∀ i, IsLocallyFiniteMeasure (μ i)] :
     IsLocallyFiniteMeasure (Measure.pi μ) := by
   refine' ⟨fun x => _⟩
   choose s hxs ho hμ using fun i => (μ i).exists_isOpen_measure_lt_top (x i)
   refine' ⟨pi univ s, set_pi_mem_nhds finite_univ fun i _ => IsOpen.mem_nhds (ho i) (hxs i), _⟩
   rw [pi_pi]
   exact ENNReal.prod_lt_top fun i _ => (hμ i).ne
 
+instance {X : ι → Type _} [∀ i, TopologicalSpace (X i)] [∀ i, MeasureSpace (X i)]
+    [∀ i, SigmaFinite (volume : Measure (X i))]
+    [∀ i, IsLocallyFiniteMeasure (volume : Measure (X i))] :
+    IsLocallyFiniteMeasure (volume : Measure (∀ i, X i)) :=
+  pi.isLocallyFiniteMeasure
+
 variable (μ)
 
 @[to_additive]
@@ -561,6 +584,12 @@ instance pi.isMulLeftInvariant [∀ i, Group (α i)] [∀ i, MeasurableMul (α i
 #align measure_theory.measure.pi.is_mul_left_invariant MeasureTheory.Measure.pi.isMulLeftInvariant
 #align measure_theory.measure.pi.is_add_left_invariant MeasureTheory.Measure.pi.isAddLeftInvariant
 
+@[to_additive]
+instance {G : ι → Type _} [∀ i, Group (G i)] [∀ i, MeasureSpace (G i)] [∀ i, MeasurableMul (G i)]
+    [∀ i, SigmaFinite (volume : Measure (G i))] [∀ i, IsMulLeftInvariant (volume : Measure (G i))] :
+    IsMulLeftInvariant (volume : Measure (∀ i, G i)) :=
+  pi.isMulLeftInvariant _
+
 @[to_additive]
 instance pi.isMulRightInvariant [∀ i, Group (α i)] [∀ i, MeasurableMul (α i)]
     [∀ i, IsMulRightInvariant (μ i)] : IsMulRightInvariant (Measure.pi μ) := by
@@ -571,6 +600,13 @@ instance pi.isMulRightInvariant [∀ i, Group (α i)] [∀ i, MeasurableMul (α
 #align measure_theory.measure.pi.is_mul_right_invariant MeasureTheory.Measure.pi.isMulRightInvariant
 #align measure_theory.measure.pi.is_add_right_invariant MeasureTheory.Measure.pi.isAddRightInvariant
 
+@[to_additive]
+instance {G : ι → Type _} [∀ i, Group (G i)] [∀ i, MeasureSpace (G i)] [∀ i, MeasurableMul (G i)]
+    [∀ i, SigmaFinite (volume : Measure (G i))]
+    [∀ i, IsMulRightInvariant (volume : Measure (G i))] :
+    IsMulRightInvariant (volume : Measure (∀ i, G i)) :=
+  pi.isMulRightInvariant _
+
 @[to_additive]
 instance pi.isInvInvariant [∀ i, Group (α i)] [∀ i, MeasurableInv (α i)]
     [∀ i, IsInvInvariant (μ i)] : IsInvInvariant (Measure.pi μ) := by
@@ -581,6 +617,12 @@ instance pi.isInvInvariant [∀ i, Group (α i)] [∀ i, MeasurableInv (α i)]
 #align measure_theory.measure.pi.is_inv_invariant MeasureTheory.Measure.pi.isInvInvariant
 #align measure_theory.measure.pi.is_neg_invariant MeasureTheory.Measure.pi.isNegInvariant
 
+@[to_additive]
+instance {G : ι → Type _} [∀ i, Group (G i)] [∀ i, MeasureSpace (G i)] [∀ i, MeasurableInv (G i)]
+    [∀ i, SigmaFinite (volume : Measure (G i))] [∀ i, IsInvInvariant (volume : Measure (G i))] :
+    IsInvInvariant (volume : Measure (∀ i, G i)) :=
+  pi.isInvInvariant _
+
 instance pi.isOpenPosMeasure [∀ i, TopologicalSpace (α i)] [∀ i, IsOpenPosMeasure (μ i)] :
     IsOpenPosMeasure (MeasureTheory.Measure.pi μ) := by
   constructor
@@ -593,6 +635,11 @@ instance pi.isOpenPosMeasure [∀ i, TopologicalSpace (α i)] [∀ i, IsOpenPosM
   apply (hs i).1.measure_pos (μ i) ⟨a i, (hs i).2⟩
 #align measure_theory.measure.pi.is_open_pos_measure MeasureTheory.Measure.pi.isOpenPosMeasure
 
+instance {X : ι → Type _} [∀ i, TopologicalSpace (X i)] [∀ i, MeasureSpace (X i)]
+    [∀ i, IsOpenPosMeasure (volume : Measure (X i))] [∀ i, SigmaFinite (volume : Measure (X i))] :
+    IsOpenPosMeasure (volume : Measure (∀ i, X i)) :=
+  pi.isOpenPosMeasure _
+
 instance pi.isFiniteMeasureOnCompacts [∀ i, TopologicalSpace (α i)]
     [∀ i, IsFiniteMeasureOnCompacts (μ i)] :
     IsFiniteMeasureOnCompacts (MeasureTheory.Measure.pi μ) := by
@@ -605,17 +652,25 @@ instance pi.isFiniteMeasureOnCompacts [∀ i, TopologicalSpace (α i)]
   exact fun i _ => ne_of_lt (IsCompact.measure_lt_top (IsCompact.image hK (continuous_apply i)))
 #align measure_theory.measure.pi.is_finite_measure_on_compacts MeasureTheory.Measure.pi.isFiniteMeasureOnCompacts
 
+instance {X : ι → Type _} [∀ i, MeasureSpace (X i)] [∀ i, TopologicalSpace (X i)]
+    [∀ i, SigmaFinite (volume : Measure (X i))]
+    [∀ i, IsFiniteMeasureOnCompacts (volume : Measure (X i))] :
+    IsFiniteMeasureOnCompacts (volume : Measure (∀ i, X i)) :=
+  pi.isFiniteMeasureOnCompacts _
+
 @[to_additive]
 instance pi.isHaarMeasure [∀ i, Group (α i)] [∀ i, TopologicalSpace (α i)]
     [∀ i, IsHaarMeasure (μ i)] [∀ i, MeasurableMul (α i)] : IsHaarMeasure (Measure.pi μ) where
 #align measure_theory.measure.pi.is_haar_measure MeasureTheory.Measure.pi.isHaarMeasure
 #align measure_theory.measure.pi.is_add_haar_measure MeasureTheory.Measure.pi.isAddHaarMeasure
 
-end Measure
+@[to_additive]
+instance {G : ι → Type _} [∀ i, Group (G i)] [∀ i, MeasureSpace (G i)] [∀ i, MeasurableMul (G i)]
+    [∀ i, TopologicalSpace (G i)] [∀ i, SigmaFinite (volume : Measure (G i))]
+    [∀ i, IsHaarMeasure (volume : Measure (G i))] : IsHaarMeasure (volume : Measure (∀ i, G i)) :=
+  pi.isHaarMeasure _
 
-instance MeasureSpace.pi [∀ i, MeasureSpace (α i)] : MeasureSpace (∀ i, α i) :=
-  ⟨Measure.pi fun _ => volume⟩
-#align measure_theory.measure_space.pi MeasureTheory.MeasureSpace.pi
+end Measure
 
 theorem volume_pi [∀ i, MeasureSpace (α i)] :
     (volume : Measure (∀ i, α i)) = Measure.pi fun _ => volume :=

diff --git a/Mathlib/MeasureTheory/Constructions/Prod/Basic.lean b/Mathlib/MeasureTheory/Constructions/Prod/Basic.lean
@@ -361,6 +361,12 @@ instance prod.instIsOpenPosMeasure {X Y : Type _} [TopologicalSpace X] [Topologi
   · exact v_open.measure_pos ν ⟨y, yv⟩
 #align measure_theory.measure.prod.is_open_pos_measure MeasureTheory.Measure.prod.instIsOpenPosMeasure
 
+instance {X Y : Type _}
+    [TopologicalSpace X] [MeasureSpace X] [IsOpenPosMeasure (volume : Measure X)]
+    [TopologicalSpace Y] [MeasureSpace Y] [IsOpenPosMeasure (volume : Measure Y)]
+    [SigmaFinite (volume : Measure Y)] : IsOpenPosMeasure (volume : Measure (X × Y)) :=
+  prod.instIsOpenPosMeasure
+
 instance prod.instIsFiniteMeasure {α β : Type _} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
     (μ : Measure α) (ν : Measure β) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
     IsFiniteMeasure (μ.prod ν) := by
@@ -369,12 +375,21 @@ instance prod.instIsFiniteMeasure {α β : Type _} {mα : MeasurableSpace α} {m
   exact mul_lt_top (measure_lt_top _ _).ne (measure_lt_top _ _).ne
 #align measure_theory.measure.prod.measure_theory.is_finite_measure MeasureTheory.Measure.prod.instIsFiniteMeasure
 
+instance {α β : Type _} [MeasureSpace α] [MeasureSpace β] [IsFiniteMeasure (volume : Measure α)]
+    [IsFiniteMeasure (volume : Measure β)] : IsFiniteMeasure (volume : Measure (α × β)) :=
+  prod.instIsFiniteMeasure _ _
+
 instance prod.instIsProbabilityMeasure {α β : Type _} {mα : MeasurableSpace α}
     {mβ : MeasurableSpace β} (μ : Measure α) (ν : Measure β) [IsProbabilityMeasure μ]
     [IsProbabilityMeasure ν] : IsProbabilityMeasure (μ.prod ν) :=
   ⟨by rw [← univ_prod_univ, prod_prod, measure_univ, measure_univ, mul_one]⟩
 #align measure_theory.measure.prod.measure_theory.is_probability_measure MeasureTheory.Measure.prod.instIsProbabilityMeasure
 
+instance {α β : Type _} [MeasureSpace α] [MeasureSpace β]
+    [IsProbabilityMeasure (volume : Measure α)] [IsProbabilityMeasure (volume : Measure β)] :
+    IsProbabilityMeasure (volume : Measure (α × β)) :=
+  prod.instIsProbabilityMeasure _ _
+
 instance prod.instIsFiniteMeasureOnCompacts {α β : Type _} [TopologicalSpace α] [TopologicalSpace β]
     {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : Measure α) (ν : Measure β)
     [IsFiniteMeasureOnCompacts μ] [IsFiniteMeasureOnCompacts ν] [SigmaFinite ν] :
@@ -392,6 +407,12 @@ instance prod.instIsFiniteMeasureOnCompacts {α β : Type _} [TopologicalSpace
       (IsCompact.measure_lt_top (hK.image continuous_snd)).ne
 #align measure_theory.measure.prod.measure_theory.is_finite_measure_on_compacts MeasureTheory.Measure.prod.instIsFiniteMeasureOnCompacts
 
+instance {X Y : Type _}
+    [TopologicalSpace X] [MeasureSpace X] [IsFiniteMeasureOnCompacts (volume : Measure X)]
+    [TopologicalSpace Y] [MeasureSpace Y] [IsFiniteMeasureOnCompacts (volume : Measure Y)]
+    [SigmaFinite (volume : Measure Y)] : IsFiniteMeasureOnCompacts (volume : Measure (X × Y)) :=
+  prod.instIsFiniteMeasureOnCompacts _ _
+
 theorem ae_measure_lt_top {s : Set (α × β)} (hs : MeasurableSet s) (h2s : (μ.prod ν) s ≠ ∞) :
     ∀ᵐ x ∂μ, ν (Prod.mk x ⁻¹' s) < ∞ := by
   rw [prod_apply hs] at h2s
@@ -460,6 +481,10 @@ instance prod.instSigmaFinite : SigmaFinite (μ.prod ν) :=
   (μ.toFiniteSpanningSetsIn.prod ν.toFiniteSpanningSetsIn).sigmaFinite
 #align measure_theory.measure.prod.sigma_finite MeasureTheory.Measure.prod.instSigmaFinite
 
+instance {α β} [MeasureSpace α] [SigmaFinite (volume : Measure α)]
+    [MeasureSpace β] [SigmaFinite (volume : Measure β)] : SigmaFinite (volume : Measure (α × β)) :=
+  prod.instSigmaFinite
+
 /-- A measure on a product space equals the product measure if they are equal on rectangles
   with as sides sets that generate the corresponding σ-algebras. -/
 theorem prod_eq_generateFrom {μ : Measure α} {ν : Measure β} {C : Set (Set α)} {D : Set (Set β)}

diff --git a/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean b/Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
@@ -257,6 +257,10 @@ instance (priority := 100) measureSpaceOfInnerProductSpace [NormedAddCommGroup E
     MeasureSpace E where volume := (stdOrthonormalBasis ℝ E).toBasis.addHaar
 #align measure_space_of_inner_product_space measureSpaceOfInnerProductSpace
 
+instance IsAddHaarMeasure [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
+    [MeasurableSpace E] [BorelSpace E] : IsAddHaarMeasure (volume : Measure E) :=
+  IsAddHaarMeasure_basis_addHaar _
+
 /- This instance should not be necessary, but Lean has difficulties to find it in product
 situations if we do not declare it explicitly. -/
 instance Real.measureSpace : MeasureSpace ℝ := by infer_instance

diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
@@ -98,7 +98,7 @@ theorem volume_Ioc {a b : ℝ} : volume (Ioc a b) = ofReal (b - a) := by simp [v
 theorem volume_singleton {a : ℝ} : volume ({a} : Set ℝ) = 0 := by simp [volume_val]
 #align real.volume_singleton Real.volume_singleton
 
-@[simp]
+-- @[simp] -- Porting note: simp can prove this, after mathlib4#4628
 theorem volume_univ : volume (univ : Set ℝ) = ∞ :=
   ENNReal.eq_top_of_forall_nnreal_le fun r =>
     calc
@@ -414,27 +414,7 @@ theorem volume_preserving_transvectionStruct [DecidableEq ι] (t : TransvectionS
       refine Measurable.add ?_ measurable_snd
       refine measurable_pi_lambda _ fun _ => Measurable.const_mul ?_ _
       exact this.comp measurable_fst
-    /-
-    Porting note: TODO
-    In Lean 4, the following tc search fails, even if we make `volume` reducible in
-    `MeasureSpaceDef`.
-    ```lean
-    variable [Fintype ι]
-    #synth SigmaFinite (volume : Measure (ι → ℝ))
-    -- fails
-    #synth SigmaFinite (Measure.pi fun _ => volume : Measure (ι → ℝ))
-    -- defeq and succeeds
-    #synth IsAddLeftInvariant (volume : Measure (ι → ℝ))
-    -- fails
-    #synth IsAddLeftInvariant (Measure.pi fun _ =>
-      (stdOrthonormalBasis ℝ ℝ).toBasis.addHaar : Measure (ι → ℝ))
-    -- defeq and succeeds
-    ```
-    These instances are required in this file.
-    This file can be built by specifying latter measures now, but this should be fixed clearly.
-    -/
-    (MeasurePreserving.id _).skew_product (μb := Measure.pi fun _ => volume)
-      (μd := Measure.pi fun _ => volume) g_meas
+    (MeasurePreserving.id _).skew_product g_meas
       (eventually_of_forall fun a => map_add_left_eq_self
         (Measure.pi fun _ => (stdOrthonormalBasis ℝ ℝ).toBasis.addHaar) _)
   exact ((A.symm e).comp B).comp A