From 9a28a6c4eca9f619bbd15297e90eff63915de56e Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 4 Jun 2023 18:51:31 +0000 Subject: [PATCH] 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 Co-authored-by: Komyyy --- Mathlib/MeasureTheory/Constructions/Pi.lean | 67 +++++++++++++++++-- .../Constructions/Prod/Basic.lean | 25 +++++++ .../MeasureTheory/Measure/Haar/OfBasis.lean | 4 ++ .../MeasureTheory/Measure/Lebesgue/Basic.lean | 24 +------ 4 files changed, 92 insertions(+), 28 deletions(-) diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean index 1a4d773e900c8..0f44b65b4dc45 100644 --- 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,10 +549,16 @@ 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) @@ -549,6 +566,12 @@ instance [∀ i, TopologicalSpace (α i)] [∀ i, IsLocallyFiniteMeasure (μ 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 index e9b713329357c..b1c4f27022684 100644 --- 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 index 7f6d0c8856f81..b7323785c781f 100644 --- 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 index 16cd7c0e2f7ac..a850a900ad16f 100644 --- 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