diff --git a/Archive/Wiedijk100Theorems/BuffonsNeedle.lean b/Archive/Wiedijk100Theorems/BuffonsNeedle.lean index 656a3b476c2fcc..e78025ecdb1312 100644 --- a/Archive/Wiedijk100Theorems/BuffonsNeedle.lean +++ b/Archive/Wiedijk100Theorems/BuffonsNeedle.lean @@ -198,7 +198,7 @@ lemma buffon_integral : rw [ ← MeasureTheory.integral_map hBₘ.aemeasurable (stronglyMeasurable_needleCrossesIndicator l).aestronglyMeasurable, - hB, ProbabilityTheory.cond, MeasureTheory.integral_smul_measure, volume_needleSpace d hd, + hB.map_eq, ProbabilityTheory.cond, MeasureTheory.integral_smul_measure, volume_needleSpace d hd, ← ENNReal.ofReal_inv_of_pos (mul_pos hd Real.pi_pos), ENNReal.toReal_ofReal (inv_nonneg.mpr (mul_nonneg hd.le Real.pi_pos.le)), smul_eq_mul, ] diff --git a/Mathlib.lean b/Mathlib.lean index a3543e873adb2c..71ff668acf1e50 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5622,6 +5622,8 @@ public import Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv public import Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue public import Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym public import Mathlib.MeasureTheory.Measure.Dirac +public import Mathlib.MeasureTheory.Measure.Dirac.Basic +public import Mathlib.MeasureTheory.Measure.Dirac.Def public import Mathlib.MeasureTheory.Measure.DiracProba public import Mathlib.MeasureTheory.Measure.Doubling public import Mathlib.MeasureTheory.Measure.EverywherePos diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean index 23e632f49d08ac..9e1965f7859ac7 100644 --- a/Mathlib/Analysis/Convolution.lean +++ b/Mathlib/Analysis/Convolution.lean @@ -174,7 +174,7 @@ section Group variable [AddGroup G] -theorem AEStronglyMeasurable.convolution_integrand' [MeasurableAdd₂ G] +theorem AEStronglyMeasurable.convolution_integrand' [SFinite ν] [MeasurableAdd₂ G] [MeasurableNeg G] (hf : AEStronglyMeasurable f ν) (hg : AEStronglyMeasurable g <| map (fun p : G × G => p.1 - p.2) (μ.prod ν)) : AEStronglyMeasurable (fun p : G × G => L (f p.2) (g (p.1 - p.2))) (μ.prod ν) := diff --git a/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean b/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean index 68966e1fa0a353..860a075895b171 100644 --- a/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean +++ b/Mathlib/Dynamics/Ergodic/MeasurePreserving.lean @@ -185,7 +185,7 @@ theorem add_measure {f μa' μb'} (hf : MeasurePreserving f μa μb) theorem smul_measure {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] {f : α → β} (hf : MeasurePreserving f μa μb) (c : R) : MeasurePreserving f (c • μa) (c • μb) where measurable := hf.measurable - map_eq := by rw [Measure.map_smul, hf.map_eq] + map_eq := by rw [Measure.map_smul _ hf.aemeasurable, hf.map_eq] variable {μ : Measure α} {f : α → α} {s : Set α} diff --git a/Mathlib/Geometry/Euclidean/Volume/Measure.lean b/Mathlib/Geometry/Euclidean/Volume/Measure.lean index 1d1243790d60c1..3c01e468cbfdfa 100644 --- a/Mathlib/Geometry/Euclidean/Volume/Measure.lean +++ b/Mathlib/Geometry/Euclidean/Volume/Measure.lean @@ -138,7 +138,8 @@ theorem Isometry.euclideanHausdorffMeasure_preimage {f : X → Y} {d : ℕ} (hf theorem Isometry.map_euclideanHausdorffMeasure {f : X → Y} {d : ℕ} (hf : Isometry f) : μHE[d].map f = μHE[d].restrict (Set.range f) := by simp_rw [euclideanHausdorffMeasure_def] - rw [Measure.map_smul, map_hausdorffMeasure hf (by simp), Measure.restrict_smul] + rw [Measure.map_smul _ hf.continuous.aemeasurable, map_hausdorffMeasure hf (by simp), + Measure.restrict_smul] /-! ### Applying scalers to `μHE[d]` @@ -335,7 +336,7 @@ theorem EuclideanGeometry.euclideanHausdorffMeasure_eq_lintegral (p : P) {v : V} ‖v‖ₑ • (volume : Measure ℝ).map g := by unfold g rw [euclideanHausdorffMeasure_eq p', ← map_map hadd.measurable hf.measurable, - ← Measure.map_smul] + ← Measure.map_smul _ (by fun_prop)] congr let v' : (AffineSubspace.mk' p (ℝ ∙ v)).direction := ⟨v, by simp⟩ suffices volume = ‖v'‖ₑ • volume.map f by simpa [v'] diff --git a/Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean b/Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean index 32bba1780b5898..dbc0268d6a7cc1 100644 --- a/Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean +++ b/Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean @@ -67,8 +67,7 @@ structure TendstoInDistribution [OpensMeasurableSpace E] (X : (i : ι) → Ω i forall_aemeasurable : ∀ i, AEMeasurable (X i) (μ i) aemeasurable_limit : AEMeasurable Z μ' := by fun_prop tendsto : Tendsto (β := ProbabilityMeasure E) - (fun n ↦ ⟨(μ n).map (X n), Measure.isProbabilityMeasure_map (forall_aemeasurable n)⟩) l - (𝓝 ⟨μ'.map Z, Measure.isProbabilityMeasure_map aemeasurable_limit⟩) + (fun n ↦ ⟨(μ n).map (X n), inferInstance⟩) l (𝓝 ⟨μ'.map Z, inferInstance⟩) lemma tendstoInDistribution_const [OpensMeasurableSpace E] (hZ : AEMeasurable Z μ') : TendstoInDistribution (fun _ ↦ Z) l Z (fun _ ↦ μ') μ' where @@ -198,8 +197,6 @@ lemma tendstoInDistribution_of_tendstoInMeasure_sub {X : ι → Ω'' → E} · simp only [LipschitzWith.zero_iff] at hF_lip specialize hF_lip x₀ simp only [← hF_lip, integral_const, smul_eq_mul] - have h_prob n : IsProbabilityMeasure (μ''.map (Y n)) := Measure.isProbabilityMeasure_map (hY n) - have : IsProbabilityMeasure (μ'.map Z) := Measure.isProbabilityMeasure_map hZ simpa using! tendsto_const_nhds -- now `F` is `L`-Lipschitz with `L > 0` simp_rw [Metric.tendsto_nhds, Real.dist_eq] diff --git a/Mathlib/MeasureTheory/Group/Convolution.lean b/Mathlib/MeasureTheory/Group/Convolution.lean index 9821a43e51b6ef..351dbf2acb0938 100644 --- a/Mathlib/MeasureTheory/Group/Convolution.lean +++ b/Mathlib/MeasureTheory/Group/Convolution.lean @@ -103,10 +103,10 @@ theorem mconv_zero (μ : Measure M) : μ ∗ₘ (0 : Measure M) = (0 : Measure M -- `mconv_smul_right` needs an instance to get `SFinite (c • ν)` from `SFinite ν`, -- hence it is placed in the `WithDensity` file, where the instance is defined. @[to_additive conv_smul_left] -theorem mconv_smul_left (μ : Measure M) (ν : Measure M) [SFinite ν] (s : ℝ≥0∞) : +theorem mconv_smul_left [MeasurableMul₂ M] (μ : Measure M) (ν : Measure M) [SFinite ν] (s : ℝ≥0∞) : (s • μ) ∗ₘ ν = s • (μ ∗ₘ ν) := by unfold mconv - rw [← Measure.map_smul, Measure.prod_smul_left] + rw [← Measure.map_smul _ (by fun_prop), Measure.prod_smul_left] @[to_additive] theorem mconv_add [MeasurableMul₂ M] (μ : Measure M) (ν : Measure M) (ρ : Measure M) [SFinite μ] @@ -158,9 +158,10 @@ theorem mconv_assoc [MeasurableMul₂ M] (μ ν ρ : Measure M) @[to_additive] instance probabilitymeasure_of_probabilitymeasures_mconv (μ : Measure M) (ν : Measure M) - [MeasurableMul₂ M] [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] : - IsProbabilityMeasure (μ ∗ₘ ν) := - isProbabilityMeasure_map (by fun_prop) + [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] : + IsProbabilityMeasure (μ ∗ₘ ν) := by + rw [mconv] + infer_instance @[to_additive] theorem mconv_absolutelyContinuous [MeasurableMul₂ M] {μ ν ρ : Measure M} diff --git a/Mathlib/MeasureTheory/Group/Defs.lean b/Mathlib/MeasureTheory/Group/Defs.lean index 5f28013fe99b7a..9d689a484b2901 100644 --- a/Mathlib/MeasureTheory/Group/Defs.lean +++ b/Mathlib/MeasureTheory/Group/Defs.lean @@ -5,6 +5,7 @@ Authors: Floris van Doorn, Yury Kudryashov -/ module +public import Mathlib.MeasureTheory.Group.Arithmetic public import Mathlib.MeasureTheory.Measure.Map /-! @@ -91,19 +92,23 @@ class IsMulRightInvariant [Mul G] (μ : Measure G) : Prop where variable {μ : Measure G} @[to_additive] -instance IsMulLeftInvariant.smulInvariantMeasure [Mul G] [IsMulLeftInvariant μ] : +instance IsMulLeftInvariant.smulInvariantMeasure [Mul G] [IsMulLeftInvariant μ] + [MeasurableConstSMul G G] : SMulInvariantMeasure G G μ := - ⟨fun _x _s hs => measure_preimage_of_map_eq_self (map_mul_left_eq_self _) hs.nullMeasurableSet⟩ + ⟨fun _x _s hs => measure_preimage_of_map_eq_self (map_mul_left_eq_self _) + (measurable_const_smul (_x)).aemeasurable hs.nullMeasurableSet⟩ @[to_additive] -instance [Monoid G] (s : Submonoid G) [IsMulLeftInvariant μ] : +instance [Monoid G] [MeasurableConstSMul G G] (s : Submonoid G) [IsMulLeftInvariant μ] : SMulInvariantMeasure {x // x ∈ s} G μ := ⟨fun ⟨x, _⟩ _ h ↦ IsMulLeftInvariant.smulInvariantMeasure.1 x h⟩ @[to_additive] -instance IsMulRightInvariant.toSMulInvariantMeasure_op [Mul G] [μ.IsMulRightInvariant] : +instance IsMulRightInvariant.toSMulInvariantMeasure_op [Mul G] [MeasurableConstSMul Gᵐᵒᵖ G] + [μ.IsMulRightInvariant] : SMulInvariantMeasure Gᵐᵒᵖ G μ := - ⟨fun _x _s hs => measure_preimage_of_map_eq_self (map_mul_right_eq_self _) hs.nullMeasurableSet⟩ + ⟨fun _x _s hs => measure_preimage_of_map_eq_self (map_mul_right_eq_self _) + (measurable_const_smul _x).aemeasurable hs.nullMeasurableSet⟩ end Measure diff --git a/Mathlib/MeasureTheory/Group/MeasurableEquiv.lean b/Mathlib/MeasureTheory/Group/MeasurableEquiv.lean index 2ef36ccd37be2f..978a440d1661d6 100644 --- a/Mathlib/MeasureTheory/Group/MeasurableEquiv.lean +++ b/Mathlib/MeasureTheory/Group/MeasurableEquiv.lean @@ -237,7 +237,7 @@ lemma domSMul_apply (μ : Measure A) (g : Gᵈᵐᵃ) (s : Set A) : exact Set.preimage_smul_inv (DomMulAct.mk.symm g) s instance : SMulCommClass ℝ≥0 Gᵈᵐᵃ (Measure A) where - smul_comm r g μ := show r • μ.map _ = (r • μ).map _ by simp + smul_comm r g μ := show r • μ.map _ = (r • μ).map _ by rw [Measure.map_smul _ (by fun_prop)] instance : SMulCommClass Gᵈᵐᵃ ℝ≥0 (Measure A) := .symm .. diff --git a/Mathlib/MeasureTheory/Group/Measure.lean b/Mathlib/MeasureTheory/Group/Measure.lean index 0a8c5c7a091499..6b47bb8ce07250 100644 --- a/Mathlib/MeasureTheory/Group/Measure.lean +++ b/Mathlib/MeasureTheory/Group/Measure.lean @@ -54,21 +54,27 @@ theorem map_mul_right_eq_self (μ : Measure G) [IsMulRightInvariant μ] (g : G) IsMulRightInvariant.map_mul_right_eq_self g @[to_additive MeasureTheory.isAddLeftInvariant_smul] -instance isMulLeftInvariant_smul [IsMulLeftInvariant μ] (c : ℝ≥0∞) : IsMulLeftInvariant (c • μ) := - ⟨fun g => by rw [Measure.map_smul, map_mul_left_eq_self]⟩ +instance isMulLeftInvariant_smul [MeasurableConstSMul G G] [IsMulLeftInvariant μ] (c : ℝ≥0∞) : + IsMulLeftInvariant (c • μ) := + ⟨fun g => by + rw [Measure.map_smul, map_mul_left_eq_self] + exact (measurable_const_smul g).aemeasurable⟩ @[to_additive MeasureTheory.isAddRightInvariant_smul] -instance isMulRightInvariant_smul [IsMulRightInvariant μ] (c : ℝ≥0∞) : +instance isMulRightInvariant_smul [MeasurableConstSMul Gᵐᵒᵖ G] [IsMulRightInvariant μ] (c : ℝ≥0∞) : IsMulRightInvariant (c • μ) := - ⟨fun g => by rw [Measure.map_smul, map_mul_right_eq_self]⟩ + ⟨fun g => by + rw [Measure.map_smul, map_mul_right_eq_self] + exact (measurable_const_smul (MulOpposite.op g)).aemeasurable⟩ @[to_additive MeasureTheory.isAddLeftInvariant_smul_nnreal] -instance isMulLeftInvariant_smul_nnreal [IsMulLeftInvariant μ] (c : ℝ≥0) : +instance isMulLeftInvariant_smul_nnreal [MeasurableConstSMul G G] [IsMulLeftInvariant μ] (c : ℝ≥0) : IsMulLeftInvariant (c • μ) := MeasureTheory.isMulLeftInvariant_smul (c : ℝ≥0∞) @[to_additive MeasureTheory.isAddRightInvariant_smul_nnreal] -instance isMulRightInvariant_smul_nnreal [IsMulRightInvariant μ] (c : ℝ≥0) : +instance isMulRightInvariant_smul_nnreal [MeasurableConstSMul Gᵐᵒᵖ G] [IsMulRightInvariant μ] + (c : ℝ≥0) : IsMulRightInvariant (c • μ) := MeasureTheory.isMulRightInvariant_smul (c : ℝ≥0∞) @@ -788,12 +794,14 @@ theorem haar_singleton [ContinuousMul G] [BorelSpace G] (g : G) : μ {g} = μ {( simp only [mul_one, preimage_mul_left_singleton, inv_inv] @[to_additive IsAddHaarMeasure.smul] -theorem IsHaarMeasure.smul {c : ℝ≥0∞} (cpos : c ≠ 0) (ctop : c ≠ ∞) : IsHaarMeasure (c • μ) := +theorem IsHaarMeasure.smul [MeasurableConstSMul G G] {c : ℝ≥0∞} (cpos : c ≠ 0) (ctop : c ≠ ∞) : + IsHaarMeasure (c • μ) := { lt_top_of_isCompact := fun _K hK => ENNReal.mul_lt_top ctop.lt_top hK.measure_lt_top toIsOpenPosMeasure := isOpenPosMeasure_smul μ cpos } @[to_additive IsAddHaarMeasure.nnreal_smul] -lemma IsHaarMeasure.nnreal_smul {c : ℝ≥0} (hc : c ≠ 0) : IsHaarMeasure (c • μ) := +lemma IsHaarMeasure.nnreal_smul [MeasurableConstSMul G G] {c : ℝ≥0} (hc : c ≠ 0) : + IsHaarMeasure (c • μ) := .smul _ (by simp [hc]) (Option.some_ne_none _) /-- If a left-invariant measure gives positive mass to some compact set with nonempty interior, then diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean b/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean index 8611e81e90214a..6b84e4dfdccf18 100644 --- a/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean +++ b/Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean @@ -28,7 +28,7 @@ We introduce the following notation for the lower Lebesgue integral of a functio @[expose] public section -assert_not_exists Module.Basis Norm MeasureTheory.MeasurePreserving MeasureTheory.Measure.dirac +assert_not_exists Module.Basis Norm MeasureTheory.MeasurePreserving open Set hiding restrict restrict_apply diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue/Map.lean b/Mathlib/MeasureTheory/Integral/Lebesgue/Map.lean index 251ec24fe6e155..546cb20cdf3bb5 100644 --- a/Mathlib/MeasureTheory/Integral/Lebesgue/Map.lean +++ b/Mathlib/MeasureTheory/Integral/Lebesgue/Map.lean @@ -46,14 +46,12 @@ theorem lintegral_map' {f : β → ℝ≥0∞} {g : α → β} _ = ∫⁻ a, hf.mk f (g a) ∂μ := lintegral_congr_ae <| hg.ae_eq_mk.symm.fun_comp _ _ = ∫⁻ a, f (g a) ∂μ := lintegral_congr_ae (ae_eq_comp hg hf.ae_eq_mk.symm) -theorem lintegral_map_le (f : β → ℝ≥0∞) (g : α → β) : +theorem lintegral_map_le (f : β → ℝ≥0∞) {g : α → β} (hg : AEMeasurable g μ) : ∫⁻ a, f a ∂Measure.map g μ ≤ ∫⁻ a, f (g a) ∂μ := by - by_cases hg : AEMeasurable g μ - · rw [← iSup_lintegral_measurable_le_eq_lintegral] - refine iSup₂_le fun i hi => iSup_le fun h'i => ?_ - rw [lintegral_map' hi.aemeasurable hg] - exact lintegral_mono fun _ ↦ h'i _ - · simp [map_of_not_aemeasurable hg] + rw [← iSup_lintegral_measurable_le_eq_lintegral] + refine iSup₂_le fun i hi => iSup_le fun h'i => ?_ + rw [lintegral_map' hi.aemeasurable hg] + exact lintegral_mono fun _ ↦ h'i _ theorem lintegral_comp {f : β → ℝ≥0∞} {g : α → β} (hf : Measurable f) (hg : Measurable g) : lintegral μ (f ∘ g) = ∫⁻ a, f a ∂map g μ := diff --git a/Mathlib/MeasureTheory/Integral/Prod.lean b/Mathlib/MeasureTheory/Integral/Prod.lean index 72b8479bb48ccd..7484a64e40beac 100644 --- a/Mathlib/MeasureTheory/Integral/Prod.lean +++ b/Mathlib/MeasureTheory/Integral/Prod.lean @@ -128,11 +128,11 @@ protected theorem MeasureTheory.AEStronglyMeasurable.prod_swap [SFinite μ] [SFi rw [← prod_swap] at hf exact hf.comp_measurable measurable_swap -theorem MeasureTheory.AEStronglyMeasurable.comp_fst {γ} [TopologicalSpace γ] {f : α → γ} +theorem MeasureTheory.AEStronglyMeasurable.comp_fst [SFinite ν] {γ} [TopologicalSpace γ] {f : α → γ} (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun z : α × β => f z.1) (μ.prod ν) := hf.comp_quasiMeasurePreserving quasiMeasurePreserving_fst -theorem MeasureTheory.AEStronglyMeasurable.comp_snd {γ} [TopologicalSpace γ] {f : β → γ} +theorem MeasureTheory.AEStronglyMeasurable.comp_snd [SFinite ν] {γ} [TopologicalSpace γ] {f : β → γ} (hf : AEStronglyMeasurable f ν) : AEStronglyMeasurable (fun z : α × β => f z.2) (μ.prod ν) := hf.comp_quasiMeasurePreserving quasiMeasurePreserving_snd @@ -258,7 +258,6 @@ theorem Integrable.integral_norm_prod_right [SFinite μ] ⦃f : α × β → E (hf : Integrable f (μ.prod ν)) : Integrable (fun y => ∫ x, ‖f (x, y)‖ ∂μ) ν := hf.swap.integral_norm_prod_left -omit [SFinite ν] in theorem Integrable.op_fst_snd {F G : Type*} [NormedAddCommGroup F] [NormedAddCommGroup G] {op : E → F → G} (hop : Continuous op.uncurry) (hop_norm : ∃ C, ∀ x y, ‖op x y‖ ≤ C * ‖x‖ * ‖y‖) {f : α → E} {g : β → F} (hf : Integrable f μ) (hg : Integrable g ν) : @@ -288,14 +287,12 @@ lemma Integrable.comp_snd {f : β → E} (hf : Integrable f ν) (μ : Measure α rw [← memLp_one_iff_integrable] at hf ⊢ exact hf.comp_snd μ -omit [SFinite ν] in @[fun_prop] theorem Integrable.smul_prod {R : Type*} [NormedRing R] [Module R E] [IsBoundedSMul R E] {f : α → R} {g : β → E} (hf : Integrable f μ) (hg : Integrable g ν) : Integrable (fun z : α × β => f z.1 • g z.2) (μ.prod ν) := hf.op_fst_snd continuous_smul ⟨1, by simpa using norm_smul_le⟩ hg -omit [SFinite ν] in @[fun_prop] theorem Integrable.mul_prod {L : Type*} [NormedRing L] {f : α → L} {g : β → L} (hf : Integrable f μ) (hg : Integrable g ν) : Integrable (fun z : α × β => f z.1 * g z.2) (μ.prod ν) := diff --git a/Mathlib/MeasureTheory/Measure/AEMeasurable.lean b/Mathlib/MeasureTheory/Measure/AEMeasurable.lean index 5febd976b0ac1d..d4d3d4e77a114b 100644 --- a/Mathlib/MeasureTheory/Measure/AEMeasurable.lean +++ b/Mathlib/MeasureTheory/Measure/AEMeasurable.lean @@ -42,12 +42,6 @@ theorem aemeasurable_id'' (μ : Measure α) {m : MeasurableSpace α} (hm : m ≤ @AEMeasurable α α m m0 id μ := @Measurable.aemeasurable α α m0 m id μ (measurable_id'' hm) -lemma aemeasurable_of_map_neZero {μ : Measure α} - {f : α → β} (h : NeZero (μ.map f)) : - AEMeasurable f μ := by - by_contra h' - simp [h'] at h - namespace AEMeasurable theorem mono_set {s t} (h : s ⊆ t) (ht : AEMeasurable f (μ.restrict t)) : @@ -449,7 +443,13 @@ instance (μ : Measure α) (f : α → β) [SFinite μ] : SFinite (μ.map f) := · rw [← sum_sfiniteSeq μ] at H ⊢ rw [map_sum H] infer_instance - · rw [map_of_not_aemeasurable H] + · obtain rfl | hμ := eq_or_ne μ 0 + · rw [Measure.map_zero]; infer_instance + rw [map_of_not_aemeasurable_of_ne_zero H hμ] + have : Nonempty β := by + contrapose! H + exact (measurable_of_empty_codomain f).aemeasurable + have : IsFiniteMeasure (dirac Classical.ofNonempty : Measure β) := isFiniteMeasure_dirac infer_instance end Measure diff --git a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean index 957e5a28bbe18c..9480fba278e7bd 100644 --- a/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean +++ b/Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean @@ -127,7 +127,6 @@ lemma taylorWithinEval_charFun_two_zero (hX : AEMeasurable X P) (hint : MemLp id 2 (P.map X)) (t : ℝ) : taylorWithinEval (charFun (P.map X)) 2 univ 0 t = 1 + (P[X] : ℝ) * t * I - (P[X ^ 2] : ℝ) * t ^ 2 / 2 := by - have : IsProbabilityMeasure (P.map X) := Measure.isProbabilityMeasure_map hX convert! taylorWithinEval_charFun_zero hint t with x simp only [Pi.pow_apply, Nat.reduceAdd, Finset.sum_range_succ, Finset.range_one, Finset.sum_singleton, Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero, mul_one, diff --git a/Mathlib/MeasureTheory/Measure/Count.lean b/Mathlib/MeasureTheory/Measure/Count.lean index ab77e21937e97d..dc54be9d2d5c97 100644 --- a/Mathlib/MeasureTheory/Measure/Count.lean +++ b/Mathlib/MeasureTheory/Measure/Count.lean @@ -5,7 +5,7 @@ Authors: Johannes Hölzl -/ module -public import Mathlib.MeasureTheory.Measure.Dirac +public import Mathlib.MeasureTheory.Measure.Dirac.Basic import Mathlib.SetTheory.Cardinal.ENNReal diff --git a/Mathlib/MeasureTheory/Measure/Dirac.lean b/Mathlib/MeasureTheory/Measure/Dirac.lean index 1bab4f93ab825d..2165d2679e5043 100644 --- a/Mathlib/MeasureTheory/Measure/Dirac.lean +++ b/Mathlib/MeasureTheory/Measure/Dirac.lean @@ -5,380 +5,7 @@ Authors: Johannes Hölzl -/ module -public import Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated -public import Mathlib.MeasureTheory.Measure.MutuallySingular -public import Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass -public import Mathlib.MeasureTheory.Measure.Typeclasses.Probability -public import Mathlib.MeasureTheory.Measure.Typeclasses.SFinite +public import Mathlib.MeasureTheory.Measure.Dirac.Def +public import Mathlib.MeasureTheory.Measure.Dirac.Basic -/-! -# Dirac measure - -In this file we define the Dirac measure `MeasureTheory.Measure.dirac a` -and prove some basic facts about it. --/ - -@[expose] public section - -open Function Set -open scoped ENNReal NNReal - -noncomputable section - -variable {α β δ : Type*} [MeasurableSpace α] [MeasurableSpace β] {s : Set α} {a : α} - -namespace MeasureTheory - -namespace Measure - -/-- The dirac measure. -/ -def dirac (a : α) : Measure α := (OuterMeasure.dirac a).toMeasure (by simp) - -instance : MeasureSpace PUnit := - ⟨dirac PUnit.unit⟩ - -theorem le_dirac_apply {a} : s.indicator 1 a ≤ dirac a s := - OuterMeasure.dirac_apply a s ▸ le_toMeasure_apply _ _ _ - -@[simp] -theorem dirac_apply' (a : α) (hs : MeasurableSet s) : dirac a s = s.indicator 1 a := - toMeasure_apply _ _ hs - -theorem dirac_apply_eq_zero_or_one : - dirac a s = 0 ∨ dirac a s = 1 := by - rw [← measure_toMeasurable s, dirac_apply' a (measurableSet_toMeasurable ..), indicator] - simp only [Pi.one_apply, ite_eq_right_iff, one_ne_zero, imp_false, ite_eq_left_iff, zero_ne_one, - not_not] - tauto - -@[simp] -theorem dirac_apply_ne_zero_iff_eq_one : - dirac a s ≠ 0 ↔ dirac a s = 1 where - mp := dirac_apply_eq_zero_or_one.resolve_left - mpr := ne_zero_of_eq_one - -@[simp] -theorem dirac_apply_ne_one_iff_eq_zero : - dirac a s ≠ 1 ↔ dirac a s = 0 where - mp := dirac_apply_eq_zero_or_one.resolve_right - mpr h := h ▸ zero_ne_one - -@[simp] -theorem dirac_apply_of_mem {a : α} (h : a ∈ s) : dirac a s = 1 := by - have : ∀ t : Set α, a ∈ t → t.indicator (1 : α → ℝ≥0∞) a = 1 := fun t ht => indicator_of_mem ht 1 - refine le_antisymm (this univ trivial ▸ ?_) (this s h ▸ le_dirac_apply) - rw [← dirac_apply' a MeasurableSet.univ] - exact measure_mono (subset_univ s) - -@[simp] -theorem dirac_apply [MeasurableSingletonClass α] (a : α) (s : Set α) : - dirac a s = s.indicator 1 a := by - by_cases h : a ∈ s; · rw [dirac_apply_of_mem h, indicator_of_mem h, Pi.one_apply] - rw [indicator_of_notMem h, ← nonpos_iff_eq_zero] - calc - dirac a s ≤ dirac a {a}ᶜ := measure_mono (subset_compl_comm.1 <| singleton_subset_iff.2 h) - _ = 0 := by simp [dirac_apply' _ (measurableSet_singleton _).compl] - -@[simp] lemma dirac_ne_zero : dirac a ≠ 0 := - fun h ↦ by simpa [h] using dirac_apply_of_mem (mem_univ a) - -@[simp] -theorem map_dirac' {f : α → β} (hf : Measurable f) (a : α) : (dirac a).map f = dirac (f a) := by - classical - exact ext fun s hs => by simp [hs, map_apply hf hs, hf hs, indicator_apply] - -@[simp] -lemma map_const (μ : Measure α) (c : β) : μ.map (fun _ ↦ c) = (μ Set.univ) • dirac c := by - ext s hs - simp only [Measure.coe_smul, Pi.smul_apply, - dirac_apply' _ hs, smul_eq_mul] - classical - rw [Measure.map_apply measurable_const hs, Set.preimage_const] - by_cases hsc : c ∈ s - · rw [(Set.indicator_eq_one_iff_mem _).mpr hsc, mul_one, ite_eq_left hsc] - · rw [ite_eq_right hsc, (Set.indicator_eq_zero_iff_notMem _).mpr hsc, measure_empty, mul_zero] - -@[simp] -theorem restrict_singleton (μ : Measure α) (a : α) : μ.restrict {a} = μ {a} • dirac a := by - ext1 s hs - by_cases ha : a ∈ s - · have : s ∩ {a} = {a} := by simpa - simp [*] - · have : s ∩ {a} = ∅ := inter_singleton_eq_empty.2 ha - simp [*] - -/-- Two measures on a countable space are equal if they agree on singletons. -/ -theorem ext_of_singleton [Countable α] {μ ν : Measure α} (h : ∀ a, μ {a} = ν {a}) : μ = ν := - ext_of_sUnion_eq_univ (countable_range singleton) (by aesop) (by simp_all) - -/-- Two measures on a countable space are equal if and only if they agree on singletons. -/ -theorem ext_iff_singleton [Countable α] {μ ν : Measure α} : μ = ν ↔ ∀ a, μ {a} = ν {a} := - ⟨fun h _ ↦ h ▸ rfl, ext_of_singleton⟩ - -theorem _root_.MeasureTheory.ext_iff_measureReal_singleton [Countable α] - {μ1 μ2 : Measure α} [SigmaFinite μ1] [SigmaFinite μ2] : - μ1 = μ2 ↔ ∀ x, μ1.real {x} = μ2.real {x} := by - rw [Measure.ext_iff_singleton] - congr! with x - rw [measureReal_def, measureReal_def, ENNReal.toReal_eq_toReal_iff] - simp [measure_singleton_lt_top, ne_of_lt] - -alias ⟨_, ext_of_measureReal_singleton⟩ := MeasureTheory.ext_iff_measureReal_singleton - -/-- If `f` is a map with countable codomain, then `μ.map f` is a sum of Dirac measures. -/ -theorem map_eq_sum [Countable β] [MeasurableSingletonClass β] (μ : Measure α) (f : α → β) - (hf : Measurable f) : μ.map f = sum fun b : β => μ (f ⁻¹' {b}) • dirac b := by - ext s - have : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y}) := fun y _ => hf (measurableSet_singleton _) - simp [← tsum_measure_preimage_singleton (to_countable s) this, *, - tsum_subtype s fun b => μ (f ⁻¹' {b}), ← indicator_mul_right s fun b => μ (f ⁻¹' {b})] - -/-- A measure on a countable type is a sum of Dirac measures. -/ -@[simp] -theorem sum_smul_dirac [Countable α] [MeasurableSingletonClass α] (μ : Measure α) : - (sum fun a => μ {a} • dirac a) = μ := by simpa using (map_eq_sum μ id measurable_id).symm - -/-- The sum of scaled Dirac measures applied to a singleton is the coefficient of that singleton. -/ -lemma sum_smul_dirac_singleton [MeasurableSingletonClass α] {f : α → ℝ≥0∞} {a : α} : - sum (fun b : α ↦ f b • dirac b) {a} = f a := by - simp +contextual [tsum_eq_single a] - -/-- A measure on a countable type is a sum of Dirac measures. -If `α` has measurable singletons, `sum_smul_dirac` gives a simpler sum. -/ -lemma exists_sum_smul_dirac [Countable α] (μ : Measure α) : - ∃ s : Set α, μ = Measure.sum (fun x : s ↦ μ (measurableAtom x) • dirac (x : α)) := by - let measurableAtoms := measurableAtom '' (Set.univ : Set α) - have h_nonempty (s : measurableAtoms) : Set.Nonempty s.1 := by - obtain ⟨y, _, hy⟩ := s.2 - rw [← hy] - exact ⟨y, mem_measurableAtom_self y⟩ - let points : measurableAtoms → α := fun s ↦ (h_nonempty s).some - have h_points_mem (s : measurableAtoms) : points s ∈ s.1 := (h_nonempty s).some_mem - refine ⟨Set.range points, ext_of_measurableAtoms fun x ↦ ?_⟩ - rw [sum_apply _ (MeasurableSet.measurableAtom_of_countable x)] - simp only [Measure.smul_apply, smul_eq_mul] - simp_rw [dirac_apply' _ (MeasurableSet.measurableAtom_of_countable x)] - rw [tsum_eq_single ⟨points ⟨measurableAtom x, by simp [measurableAtoms]⟩, by simp⟩] - · rw [indicator_of_mem] - · simp only [Pi.one_apply, mul_one] - congr 1 - refine (measurableAtom_eq_of_mem ?_).symm - convert! h_points_mem _ - simp - · convert! h_points_mem _ - simp - · simp only [ne_eq, mul_eq_zero, indicator_apply_eq_zero, Pi.one_apply, one_ne_zero, imp_false, - Subtype.forall, Set.mem_range, Subtype.exists, Subtype.mk.injEq, forall_exists_index] - refine fun y s hs hsy hyx ↦ .inr fun hyx' ↦ hyx ?_ - rw [← hsy] - congr - have h1 : measurableAtom y = measurableAtom x := measurableAtom_eq_of_mem hyx' - have h2 : measurableAtom y = s := by - specialize h_points_mem ⟨s, hs⟩ - obtain ⟨z, _, hz⟩ := hs - simp only at h_points_mem - rw [← hz, ← hsy] - refine measurableAtom_eq_of_mem ?_ - convert! h_points_mem - rw [← h2, h1] - -/-- Given that `α` is a countable, measurable space with all singleton sets measurable, -write the measure of a set `s` as the sum of the measure of `{x}` for all `x ∈ s`. -/ -theorem tsum_indicator_apply_singleton [Countable α] [MeasurableSingletonClass α] (μ : Measure α) - (s : Set α) (hs : MeasurableSet s) : (∑' x : α, s.indicator (fun x => μ {x}) x) = μ s := by - classical - calc - (∑' x : α, s.indicator (fun x => μ {x}) x) = - Measure.sum (fun a => μ {a} • Measure.dirac a) s := by - simp only [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply, - Set.indicator_apply, mul_ite, Pi.one_apply, mul_one, mul_zero] - _ = μ s := by rw [μ.sum_smul_dirac] - -end Measure - -open Measure - -theorem mem_ae_dirac_iff {a : α} (hs : MeasurableSet s) : s ∈ ae (dirac a) ↔ a ∈ s := by - by_cases a ∈ s <;> simp [mem_ae_iff, dirac_apply', hs.compl, *] - -@[simp] theorem ae_dirac_iff {a : α} {p : α → Prop} (hp : MeasurableSet { x | p x }) : - (∀ᵐ x ∂dirac a, p x) ↔ p a := - mem_ae_dirac_iff hp - -@[simp] -theorem ae_dirac_eq [MeasurableSingletonClass α] (a : α) : ae (dirac a) = pure a := by - ext s - simp [mem_ae_iff, imp_false] - -theorem ae_eq_dirac' [MeasurableSingletonClass β] {a : α} {f : α → β} (hf : Measurable f) : - f =ᵐ[dirac a] const α (f a) := - (ae_dirac_iff <| show MeasurableSet (f ⁻¹' {f a}) from hf <| measurableSet_singleton _).2 rfl - -theorem ae_eq_dirac [MeasurableSingletonClass α] {a : α} (f : α → δ) : - f =ᵐ[dirac a] const α (f a) := by simp [Filter.EventuallyEq] - -@[fun_prop] -lemma aemeasurable_dirac [MeasurableSingletonClass α] {a : α} {f : α → β} : - AEMeasurable f (Measure.dirac a) := - ⟨fun _ ↦ f a, measurable_const, ae_eq_dirac f⟩ - -@[simp] -theorem Measure.map_dirac [MeasurableSingletonClass α] [MeasurableSingletonClass β] - {f : α → β} (a : α) : (dirac a).map f = dirac (f a) := by - classical - ext s hs - rw [map_apply_of_aemeasurable (by fun_prop) hs] - simp [indicator_apply] - -instance Measure.dirac.isProbabilityMeasure {x : α} : IsProbabilityMeasure (dirac x) := - ⟨dirac_apply_of_mem <| mem_univ x⟩ - -lemma _root_.HasSum.isProbabilityMeasure_sum_dirac_ennreal {ι : Type*} {mδ : MeasurableSpace δ} - {c : ι → ℝ≥0∞} {d : ι → δ} (h : HasSum c 1) : - IsProbabilityMeasure (Measure.sum fun i ↦ c i • .dirac (d i)) where - measure_univ := by simp [h.tsum_eq] - -lemma _root_.HasSum.isProbabilityMeasure_sum_dirac_nnreal {ι : Type*} {mδ : MeasurableSpace δ} - {c : ι → ℝ≥0} {d : ι → δ} (h : HasSum c 1) : - IsProbabilityMeasure (Measure.sum fun i ↦ c i • .dirac (d i)) := - (ENNReal.hasSum_coe.2 h).isProbabilityMeasure_sum_dirac_ennreal - -lemma _root_.HasSum.isProbabilityMeasure_sum_dirac {ι : Type*} {mδ : MeasurableSpace δ} - {c : ι → ℝ} {d : ι → δ} (h1 : ∀ i, 0 ≤ c i) (h2 : HasSum c 1) : - IsProbabilityMeasure (Measure.sum fun i ↦ ENNReal.ofReal (c i) • .dirac (d i)) := - HasSum.isProbabilityMeasure_sum_dirac_nnreal (by simpa using h2.toNNReal h1) - -instance [hα : Nonempty α] : Nonempty {μ : Measure α // IsProbabilityMeasure μ} := - ⟨Measure.dirac hα.some, inferInstance⟩ - -/-! Extra instances to short-circuit type class resolution -/ - -instance Measure.dirac.instIsFiniteMeasure {a : α} : IsFiniteMeasure (dirac a) := inferInstance -instance Measure.dirac.instSigmaFinite {a : α} : SigmaFinite (dirac a) := inferInstance - -theorem dirac_eq_one_iff_mem (hs : MeasurableSet s) : dirac a s = 1 ↔ a ∈ s := by - rw [← prob_compl_eq_zero_iff hs, ← mem_ae_iff] - apply mem_ae_dirac_iff hs - -theorem dirac_eq_zero_iff_not_mem (hs : MeasurableSet s) : dirac a s = 0 ↔ a ∉ s := by - rw [← compl_compl s, ← mem_ae_iff, notMem_compl_iff] - apply mem_ae_dirac_iff (MeasurableSet.compl_iff.mpr hs) - -theorem restrict_dirac' (hs : MeasurableSet s) [Decidable (a ∈ s)] : - (Measure.dirac a).restrict s = if a ∈ s then Measure.dirac a else 0 := by - split_ifs with has - · apply restrict_eq_self_of_ae_mem - rw [ae_dirac_iff] <;> assumption - · rw [restrict_eq_zero, dirac_apply' _ hs, indicator_of_notMem has] - -theorem restrict_dirac [MeasurableSingletonClass α] [Decidable (a ∈ s)] : - (Measure.dirac a).restrict s = if a ∈ s then Measure.dirac a else 0 := by - split_ifs with has - · apply restrict_eq_self_of_ae_mem - rwa [ae_dirac_eq] - · rw [restrict_eq_zero, dirac_apply, indicator_of_notMem has] - -lemma mutuallySingular_dirac [MeasurableSingletonClass α] (x : α) (μ : Measure α) - [NullSingletonClass μ] : - Measure.dirac x ⟂ₘ μ := - ⟨{x}ᶜ, (MeasurableSet.singleton x).compl, by simp, by simp⟩ - -section dirac_injective - -/-- Dirac delta measures at two points are equal if every measurable set contains either both or -neither of the points. -/ -lemma dirac_eq_dirac_iff_forall_mem_iff_mem {x y : α} : - Measure.dirac x = Measure.dirac y ↔ ∀ A, MeasurableSet A → (x ∈ A ↔ y ∈ A) := by - constructor - · intro h A A_mble - have obs := congr_arg (fun μ ↦ μ A) h - simp only [Measure.dirac_apply' _ A_mble] at obs - by_cases x_in_A : x ∈ A - · simpa only [x_in_A, indicator_of_mem, Pi.one_apply, true_iff, Eq.comm (a := (1 : ℝ≥0∞)), - indicator_eq_one_iff_mem] using obs - · simpa only [x_in_A, indicator_of_notMem, Eq.comm (a := (0 : ℝ≥0∞)), indicator_apply_eq_zero, - false_iff, not_false_eq_true, Pi.one_apply, one_ne_zero, imp_false] using obs - · intro h - ext A A_mble - by_cases x_in_A : x ∈ A - · simp only [Measure.dirac_apply' _ A_mble, x_in_A, indicator_of_mem, Pi.one_apply, - (h A A_mble).mp x_in_A] - · have y_notin_A : y ∉ A := by simp_all only [not_false_eq_true] - simp only [Measure.dirac_apply' _ A_mble, x_in_A, y_notin_A, - not_false_eq_true, indicator_of_notMem] - -/-- Dirac delta measures at two points are different if and only if there is a measurable set -containing one of the points but not the other. -/ -lemma dirac_ne_dirac_iff_exists_measurableSet {x y : α} : - Measure.dirac x ≠ Measure.dirac y ↔ ∃ A, MeasurableSet A ∧ x ∈ A ∧ y ∉ A := by - apply not_iff_not.mp - simp only [ne_eq, not_not, not_exists, not_and, dirac_eq_dirac_iff_forall_mem_iff_mem] - refine ⟨fun h A A_mble ↦ by simp only [h A A_mble, imp_self], fun h A A_mble ↦ ?_⟩ - by_cases x_in_A : x ∈ A - · simp only [x_in_A, h A A_mble x_in_A] - · simpa only [x_in_A, false_iff] using! h Aᶜ (MeasurableSet.compl_iff.mpr A_mble) x_in_A - -open MeasurableSpace -/-- Dirac delta measures at two different points are different, assuming the measurable space -separates points. -/ -lemma dirac_ne_dirac [SeparatesPoints α] {x y : α} (x_ne_y : x ≠ y) : - Measure.dirac x ≠ Measure.dirac y := by - obtain ⟨A, A_mble, x_in_A, y_notin_A⟩ := exists_measurableSet_of_ne x_ne_y - exact dirac_ne_dirac_iff_exists_measurableSet.mpr ⟨A, A_mble, x_in_A, y_notin_A⟩ - -/-- Dirac delta measures at two points are different if and only if the two points are different, -assuming the measurable space separates points. -/ -lemma dirac_ne_dirac_iff [SeparatesPoints α] {x y : α} : - Measure.dirac x ≠ Measure.dirac y ↔ x ≠ y := - ⟨fun h x_eq_y ↦ h <| congrArg dirac x_eq_y, fun h ↦ dirac_ne_dirac h⟩ - -/-- Dirac delta measures at two points are equal if and only if the two points are equal, -assuming the measurable space separates points. -/ -lemma dirac_eq_dirac_iff [SeparatesPoints α] {x y : α} : - Measure.dirac x = Measure.dirac y ↔ x = y := not_iff_not.mp dirac_ne_dirac_iff - -/-- The assignment `x ↦ dirac x` is injective, assuming the measurable space separates points. -/ -lemma injective_dirac [SeparatesPoints α] : - Function.Injective (fun (x : α) ↦ dirac x) := fun x y x_ne_y ↦ by rwa [← dirac_eq_dirac_iff] - -end dirac_injective - -end MeasureTheory - -namespace MeasureTheory.Measure -variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} - [MeasurableSingletonClass α] {f : β → α} {μ : Measure α} {s : Finset α} {a₁ a₂ : α} - -lemma ae_mem_finset_iff : (∀ᵐ a ∂μ, a ∈ s) ↔ μ = ∑ a ∈ s, μ {a} • .dirac a where - mp hμ := by - ext t ht - rw [← measure_sdiff_null (s := t) hμ] - dsimp - rw [Set.sdiff_compl, ← (s : Set α).biUnion_of_singleton] - simp_rw [Finset.mem_coe, Set.inter_iUnion] - rw [measure_biUnion_finset (fun i hi j hj hij ↦ .inter_left' _ <| .inter_right' _ ?_) - (by measurability)] - · simp only [coe_finsetSum, Finset.sum_apply, smul_apply] - congr with a - by_cases ha : a ∈ t <;> simp [*] - simpa - mpr hμ := by rw [hμ, ae_finsetSum_measure_iff]; exact fun i hi ↦ ae_smul_measure (by simpa) _ - -lemma ae_eq_or_eq_iff_eq_dirac_add_dirac (ha : a₁ ≠ a₂) : - (∀ᵐ a ∂μ, a = a₁ ∨ a = a₂) ↔ μ = μ {a₁} • .dirac a₁ + μ {a₂} • .dirac a₂ := by - -- FIXME: Why does `simpa using ...` not work? - convert! ae_mem_finset_iff (s := .cons a₁ { a₂ } <| by simpa) <;> simp - -lemma ae_mem_finset_iff_map_eq_sum_dirac {μ : Measure β} (hf : AEMeasurable f μ) : - (∀ᵐ b ∂μ, f b ∈ s) ↔ μ.map f = ∑ a ∈ s, μ (f ⁻¹' {a}) • .dirac a := by - rw [← ae_map_iff hf (by measurability), ae_mem_finset_iff] - simp [map_apply₀ hf] - -lemma ae_eq_or_eq_iff_map_eq_dirac_add_dirac {μ : Measure β} (hf : AEMeasurable f μ) - (ha : a₁ ≠ a₂) : - (∀ᵐ b ∂μ, f b = a₁ ∨ f b = a₂) ↔ - μ.map f = μ (f ⁻¹' {a₁}) • .dirac a₁ + μ (f ⁻¹' {a₂}) • .dirac a₂ := by - -- FIXME: Why does `simpa using ...` not work? - convert! ae_mem_finset_iff_map_eq_sum_dirac (s := .cons a₁ { a₂ } <| by simpa) hf <;> simp - -end MeasureTheory.Measure +deprecated_module (since := "2026-08-20") diff --git a/Mathlib/MeasureTheory/Measure/Dirac/Basic.lean b/Mathlib/MeasureTheory/Measure/Dirac/Basic.lean new file mode 100644 index 00000000000000..3431d6976e3a76 --- /dev/null +++ b/Mathlib/MeasureTheory/Measure/Dirac/Basic.lean @@ -0,0 +1,334 @@ +/- +Copyright (c) 2018 Johannes Hölzl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johannes Hölzl +-/ +module + +public import Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated +public import Mathlib.MeasureTheory.Measure.Dirac.Def +public import Mathlib.MeasureTheory.Measure.MutuallySingular +public import Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass +public import Mathlib.MeasureTheory.Measure.Typeclasses.Probability +public import Mathlib.MeasureTheory.Measure.Typeclasses.SFinite + +/-! +# Basic properties of the Dirac measure + +In this file we prove some basic facts about the Dirac measure `MeasureTheory.Measure.dirac a` +defined in the `Dirac.Def` file. +-/ + +@[expose] public section + +open Function Set +open scoped ENNReal NNReal + +noncomputable section + +variable {α β δ : Type*} [MeasurableSpace α] [MeasurableSpace β] {s : Set α} {a : α} + +namespace MeasureTheory + +namespace Measure + +@[simp] +theorem map_dirac' {f : α → β} (hf : Measurable f) (a : α) : (dirac a).map f = dirac (f a) := by + classical + exact ext fun s hs => by simp [hs, map_apply hf hs, hf hs, indicator_apply] + +@[simp] +lemma map_const (μ : Measure α) (c : β) : μ.map (fun _ ↦ c) = (μ Set.univ) • dirac c := by + ext s hs + simp only [Measure.coe_smul, Pi.smul_apply, + dirac_apply' _ hs, smul_eq_mul] + classical + rw [Measure.map_apply measurable_const hs, Set.preimage_const] + by_cases hsc : c ∈ s + · rw [(Set.indicator_eq_one_iff_mem _).mpr hsc, mul_one, ite_eq_left hsc] + · rw [ite_eq_right hsc, (Set.indicator_eq_zero_iff_notMem _).mpr hsc, measure_empty, mul_zero] + +@[simp] +theorem restrict_singleton (μ : Measure α) (a : α) : μ.restrict {a} = μ {a} • dirac a := by + ext1 s hs + by_cases ha : a ∈ s + · have : s ∩ {a} = {a} := by simpa + simp [*] + · have : s ∩ {a} = ∅ := inter_singleton_eq_empty.2 ha + simp [*] + +/-- Two measures on a countable space are equal if they agree on singletons. -/ +theorem ext_of_singleton [Countable α] {μ ν : Measure α} (h : ∀ a, μ {a} = ν {a}) : μ = ν := + ext_of_sUnion_eq_univ (countable_range singleton) (by aesop) (by simp_all) + +/-- Two measures on a countable space are equal if and only if they agree on singletons. -/ +theorem ext_iff_singleton [Countable α] {μ ν : Measure α} : μ = ν ↔ ∀ a, μ {a} = ν {a} := + ⟨fun h _ ↦ h ▸ rfl, ext_of_singleton⟩ + +theorem _root_.MeasureTheory.ext_iff_measureReal_singleton [Countable α] + {μ1 μ2 : Measure α} [SigmaFinite μ1] [SigmaFinite μ2] : + μ1 = μ2 ↔ ∀ x, μ1.real {x} = μ2.real {x} := by + rw [Measure.ext_iff_singleton] + congr! with x + rw [measureReal_def, measureReal_def, ENNReal.toReal_eq_toReal_iff] + simp [measure_singleton_lt_top, ne_of_lt] + +alias ⟨_, ext_of_measureReal_singleton⟩ := MeasureTheory.ext_iff_measureReal_singleton + +/-- If `f` is a map with countable codomain, then `μ.map f` is a sum of Dirac measures. -/ +theorem map_eq_sum [Countable β] [MeasurableSingletonClass β] (μ : Measure α) (f : α → β) + (hf : Measurable f) : μ.map f = sum fun b : β => μ (f ⁻¹' {b}) • dirac b := by + ext s + have : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y}) := fun y _ => hf (measurableSet_singleton _) + simp [← tsum_measure_preimage_singleton (to_countable s) this, *, + tsum_subtype s fun b => μ (f ⁻¹' {b}), ← indicator_mul_right s fun b => μ (f ⁻¹' {b})] + +/-- A measure on a countable type is a sum of Dirac measures. -/ +@[simp] +theorem sum_smul_dirac [Countable α] [MeasurableSingletonClass α] (μ : Measure α) : + (sum fun a => μ {a} • dirac a) = μ := by simpa using (map_eq_sum μ id measurable_id).symm + +/-- The sum of scaled Dirac measures applied to a singleton is the coefficient of that singleton. -/ +lemma sum_smul_dirac_singleton [MeasurableSingletonClass α] {f : α → ℝ≥0∞} {a : α} : + sum (fun b : α ↦ f b • dirac b) {a} = f a := by + simp +contextual [tsum_eq_single a] + +/-- A measure on a countable type is a sum of Dirac measures. +If `α` has measurable singletons, `sum_smul_dirac` gives a simpler sum. -/ +lemma exists_sum_smul_dirac [Countable α] (μ : Measure α) : + ∃ s : Set α, μ = Measure.sum (fun x : s ↦ μ (measurableAtom x) • dirac (x : α)) := by + let measurableAtoms := measurableAtom '' (Set.univ : Set α) + have h_nonempty (s : measurableAtoms) : Set.Nonempty s.1 := by + obtain ⟨y, _, hy⟩ := s.2 + rw [← hy] + exact ⟨y, mem_measurableAtom_self y⟩ + let points : measurableAtoms → α := fun s ↦ (h_nonempty s).some + have h_points_mem (s : measurableAtoms) : points s ∈ s.1 := (h_nonempty s).some_mem + refine ⟨Set.range points, ext_of_measurableAtoms fun x ↦ ?_⟩ + rw [sum_apply _ (MeasurableSet.measurableAtom_of_countable x)] + simp only [Measure.smul_apply, smul_eq_mul] + simp_rw [dirac_apply' _ (MeasurableSet.measurableAtom_of_countable x)] + rw [tsum_eq_single ⟨points ⟨measurableAtom x, by simp [measurableAtoms]⟩, by simp⟩] + · rw [indicator_of_mem] + · simp only [Pi.one_apply, mul_one] + congr 1 + refine (measurableAtom_eq_of_mem ?_).symm + convert! h_points_mem _ + simp + · convert! h_points_mem _ + simp + · simp only [ne_eq, mul_eq_zero, indicator_apply_eq_zero, Pi.one_apply, one_ne_zero, imp_false, + Subtype.forall, Set.mem_range, Subtype.exists, Subtype.mk.injEq, forall_exists_index] + refine fun y s hs hsy hyx ↦ .inr fun hyx' ↦ hyx ?_ + rw [← hsy] + congr + have h1 : measurableAtom y = measurableAtom x := measurableAtom_eq_of_mem hyx' + have h2 : measurableAtom y = s := by + specialize h_points_mem ⟨s, hs⟩ + obtain ⟨z, _, hz⟩ := hs + simp only at h_points_mem + rw [← hz, ← hsy] + refine measurableAtom_eq_of_mem ?_ + convert! h_points_mem + rw [← h2, h1] + +/-- Given that `α` is a countable, measurable space with all singleton sets measurable, +write the measure of a set `s` as the sum of the measure of `{x}` for all `x ∈ s`. -/ +theorem tsum_indicator_apply_singleton [Countable α] [MeasurableSingletonClass α] (μ : Measure α) + (s : Set α) (hs : MeasurableSet s) : (∑' x : α, s.indicator (fun x => μ {x}) x) = μ s := by + classical + calc + (∑' x : α, s.indicator (fun x => μ {x}) x) = + Measure.sum (fun a => μ {a} • Measure.dirac a) s := by + simp only [Measure.sum_apply _ hs, Measure.smul_apply, smul_eq_mul, Measure.dirac_apply, + Set.indicator_apply, mul_ite, Pi.one_apply, mul_one, mul_zero] + _ = μ s := by rw [μ.sum_smul_dirac] + +end Measure + +open Measure + +theorem mem_ae_dirac_iff {a : α} (hs : MeasurableSet s) : s ∈ ae (dirac a) ↔ a ∈ s := by + by_cases a ∈ s <;> simp [mem_ae_iff, dirac_apply', hs.compl, *] + +@[simp] theorem ae_dirac_iff {a : α} {p : α → Prop} (hp : MeasurableSet { x | p x }) : + (∀ᵐ x ∂dirac a, p x) ↔ p a := + mem_ae_dirac_iff hp + +@[simp] +theorem ae_dirac_eq [MeasurableSingletonClass α] (a : α) : ae (dirac a) = pure a := by + ext s + simp [mem_ae_iff, imp_false] + +theorem ae_eq_dirac' [MeasurableSingletonClass β] {a : α} {f : α → β} (hf : Measurable f) : + f =ᵐ[dirac a] const α (f a) := + (ae_dirac_iff <| show MeasurableSet (f ⁻¹' {f a}) from hf <| measurableSet_singleton _).2 rfl + +theorem ae_eq_dirac [MeasurableSingletonClass α] {a : α} (f : α → δ) : + f =ᵐ[dirac a] const α (f a) := by simp [Filter.EventuallyEq] + +@[fun_prop] +lemma aemeasurable_dirac [MeasurableSingletonClass α] {a : α} {f : α → β} : + AEMeasurable f (Measure.dirac a) := + ⟨fun _ ↦ f a, measurable_const, ae_eq_dirac f⟩ + +@[simp] +theorem Measure.map_dirac [MeasurableSingletonClass α] [MeasurableSingletonClass β] + {f : α → β} (a : α) : (dirac a).map f = dirac (f a) := by + classical + ext s hs + rw [map_apply_of_aemeasurable (by fun_prop) hs] + simp [indicator_apply] + +instance Measure.dirac.isProbabilityMeasure {x : α} : IsProbabilityMeasure (dirac x) := + ⟨dirac_apply_of_mem <| mem_univ x⟩ + +lemma _root_.HasSum.isProbabilityMeasure_sum_dirac_ennreal {ι : Type*} {mδ : MeasurableSpace δ} + {c : ι → ℝ≥0∞} {d : ι → δ} (h : HasSum c 1) : + IsProbabilityMeasure (Measure.sum fun i ↦ c i • .dirac (d i)) where + measure_univ := by simp [h.tsum_eq] + +lemma _root_.HasSum.isProbabilityMeasure_sum_dirac_nnreal {ι : Type*} {mδ : MeasurableSpace δ} + {c : ι → ℝ≥0} {d : ι → δ} (h : HasSum c 1) : + IsProbabilityMeasure (Measure.sum fun i ↦ c i • .dirac (d i)) := + (ENNReal.hasSum_coe.2 h).isProbabilityMeasure_sum_dirac_ennreal + +lemma _root_.HasSum.isProbabilityMeasure_sum_dirac {ι : Type*} {mδ : MeasurableSpace δ} + {c : ι → ℝ} {d : ι → δ} (h1 : ∀ i, 0 ≤ c i) (h2 : HasSum c 1) : + IsProbabilityMeasure (Measure.sum fun i ↦ ENNReal.ofReal (c i) • .dirac (d i)) := + HasSum.isProbabilityMeasure_sum_dirac_nnreal (by simpa using h2.toNNReal h1) + +instance [hα : Nonempty α] : Nonempty {μ : Measure α // IsProbabilityMeasure μ} := + ⟨Measure.dirac hα.some, inferInstance⟩ + +/-! Extra instances to short-circuit type class resolution -/ + +instance Measure.dirac.instIsFiniteMeasure {a : α} : IsFiniteMeasure (dirac a) := inferInstance +instance Measure.dirac.instSigmaFinite {a : α} : SigmaFinite (dirac a) := inferInstance + +theorem dirac_eq_one_iff_mem (hs : MeasurableSet s) : dirac a s = 1 ↔ a ∈ s := by + rw [← prob_compl_eq_zero_iff hs, ← mem_ae_iff] + apply mem_ae_dirac_iff hs + +theorem dirac_eq_zero_iff_not_mem (hs : MeasurableSet s) : dirac a s = 0 ↔ a ∉ s := by + rw [← compl_compl s, ← mem_ae_iff, notMem_compl_iff] + apply mem_ae_dirac_iff (MeasurableSet.compl_iff.mpr hs) + +theorem restrict_dirac' (hs : MeasurableSet s) [Decidable (a ∈ s)] : + (Measure.dirac a).restrict s = if a ∈ s then Measure.dirac a else 0 := by + split_ifs with has + · apply restrict_eq_self_of_ae_mem + rw [ae_dirac_iff] <;> assumption + · rw [restrict_eq_zero, dirac_apply' _ hs, indicator_of_notMem has] + +theorem restrict_dirac [MeasurableSingletonClass α] [Decidable (a ∈ s)] : + (Measure.dirac a).restrict s = if a ∈ s then Measure.dirac a else 0 := by + split_ifs with has + · apply restrict_eq_self_of_ae_mem + rwa [ae_dirac_eq] + · rw [restrict_eq_zero, dirac_apply, indicator_of_notMem has] + +lemma mutuallySingular_dirac [MeasurableSingletonClass α] (x : α) (μ : Measure α) + [NullSingletonClass μ] : + Measure.dirac x ⟂ₘ μ := + ⟨{x}ᶜ, (MeasurableSet.singleton x).compl, by simp, by simp⟩ + +section dirac_injective + +/-- Dirac delta measures at two points are equal if every measurable set contains either both or +neither of the points. -/ +lemma dirac_eq_dirac_iff_forall_mem_iff_mem {x y : α} : + Measure.dirac x = Measure.dirac y ↔ ∀ A, MeasurableSet A → (x ∈ A ↔ y ∈ A) := by + constructor + · intro h A A_mble + have obs := congr_arg (fun μ ↦ μ A) h + simp only [Measure.dirac_apply' _ A_mble] at obs + by_cases x_in_A : x ∈ A + · simpa only [x_in_A, indicator_of_mem, Pi.one_apply, true_iff, Eq.comm (a := (1 : ℝ≥0∞)), + indicator_eq_one_iff_mem] using obs + · simpa only [x_in_A, indicator_of_notMem, Eq.comm (a := (0 : ℝ≥0∞)), indicator_apply_eq_zero, + false_iff, not_false_eq_true, Pi.one_apply, one_ne_zero, imp_false] using obs + · intro h + ext A A_mble + by_cases x_in_A : x ∈ A + · simp only [Measure.dirac_apply' _ A_mble, x_in_A, indicator_of_mem, Pi.one_apply, + (h A A_mble).mp x_in_A] + · have y_notin_A : y ∉ A := by simp_all only [not_false_eq_true] + simp only [Measure.dirac_apply' _ A_mble, x_in_A, y_notin_A, + not_false_eq_true, indicator_of_notMem] + +/-- Dirac delta measures at two points are different if and only if there is a measurable set +containing one of the points but not the other. -/ +lemma dirac_ne_dirac_iff_exists_measurableSet {x y : α} : + Measure.dirac x ≠ Measure.dirac y ↔ ∃ A, MeasurableSet A ∧ x ∈ A ∧ y ∉ A := by + apply not_iff_not.mp + simp only [ne_eq, not_not, not_exists, not_and, dirac_eq_dirac_iff_forall_mem_iff_mem] + refine ⟨fun h A A_mble ↦ by simp only [h A A_mble, imp_self], fun h A A_mble ↦ ?_⟩ + by_cases x_in_A : x ∈ A + · simp only [x_in_A, h A A_mble x_in_A] + · simpa only [x_in_A, false_iff] using! h Aᶜ (MeasurableSet.compl_iff.mpr A_mble) x_in_A + +open MeasurableSpace +/-- Dirac delta measures at two different points are different, assuming the measurable space +separates points. -/ +lemma dirac_ne_dirac [SeparatesPoints α] {x y : α} (x_ne_y : x ≠ y) : + Measure.dirac x ≠ Measure.dirac y := by + obtain ⟨A, A_mble, x_in_A, y_notin_A⟩ := exists_measurableSet_of_ne x_ne_y + exact dirac_ne_dirac_iff_exists_measurableSet.mpr ⟨A, A_mble, x_in_A, y_notin_A⟩ + +/-- Dirac delta measures at two points are different if and only if the two points are different, +assuming the measurable space separates points. -/ +lemma dirac_ne_dirac_iff [SeparatesPoints α] {x y : α} : + Measure.dirac x ≠ Measure.dirac y ↔ x ≠ y := + ⟨fun h x_eq_y ↦ h <| congrArg dirac x_eq_y, fun h ↦ dirac_ne_dirac h⟩ + +/-- Dirac delta measures at two points are equal if and only if the two points are equal, +assuming the measurable space separates points. -/ +lemma dirac_eq_dirac_iff [SeparatesPoints α] {x y : α} : + Measure.dirac x = Measure.dirac y ↔ x = y := not_iff_not.mp dirac_ne_dirac_iff + +/-- The assignment `x ↦ dirac x` is injective, assuming the measurable space separates points. -/ +lemma injective_dirac [SeparatesPoints α] : + Function.Injective (fun (x : α) ↦ dirac x) := fun x y x_ne_y ↦ by rwa [← dirac_eq_dirac_iff] + +end dirac_injective + +end MeasureTheory + +namespace MeasureTheory.Measure +variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} + [MeasurableSingletonClass α] {f : β → α} {μ : Measure α} {s : Finset α} {a₁ a₂ : α} + +lemma ae_mem_finset_iff : (∀ᵐ a ∂μ, a ∈ s) ↔ μ = ∑ a ∈ s, μ {a} • .dirac a where + mp hμ := by + ext t ht + rw [← measure_sdiff_null (s := t) hμ] + dsimp + rw [Set.sdiff_compl, ← (s : Set α).biUnion_of_singleton] + simp_rw [Finset.mem_coe, Set.inter_iUnion] + rw [measure_biUnion_finset (fun i hi j hj hij ↦ .inter_left' _ <| .inter_right' _ ?_) + (by measurability)] + · simp only [coe_finsetSum, Finset.sum_apply, smul_apply] + congr with a + by_cases ha : a ∈ t <;> simp [*] + simpa + mpr hμ := by rw [hμ, ae_finsetSum_measure_iff]; exact fun i hi ↦ ae_smul_measure (by simpa) _ + +lemma ae_eq_or_eq_iff_eq_dirac_add_dirac (ha : a₁ ≠ a₂) : + (∀ᵐ a ∂μ, a = a₁ ∨ a = a₂) ↔ μ = μ {a₁} • .dirac a₁ + μ {a₂} • .dirac a₂ := by + -- FIXME: Why does `simpa using ...` not work? + convert! ae_mem_finset_iff (s := .cons a₁ { a₂ } <| by simpa) <;> simp + +lemma ae_mem_finset_iff_map_eq_sum_dirac {μ : Measure β} (hf : AEMeasurable f μ) : + (∀ᵐ b ∂μ, f b ∈ s) ↔ μ.map f = ∑ a ∈ s, μ (f ⁻¹' {a}) • .dirac a := by + rw [← ae_map_iff hf (by measurability), ae_mem_finset_iff] + simp [map_apply₀ hf] + +lemma ae_eq_or_eq_iff_map_eq_dirac_add_dirac {μ : Measure β} (hf : AEMeasurable f μ) + (ha : a₁ ≠ a₂) : + (∀ᵐ b ∂μ, f b = a₁ ∨ f b = a₂) ↔ + μ.map f = μ (f ⁻¹' {a₁}) • .dirac a₁ + μ (f ⁻¹' {a₂}) • .dirac a₂ := by + -- FIXME: Why does `simpa using ...` not work? + convert! ae_mem_finset_iff_map_eq_sum_dirac (s := .cons a₁ { a₂ } <| by simpa) hf <;> simp + +end MeasureTheory.Measure diff --git a/Mathlib/MeasureTheory/Measure/Dirac/Def.lean b/Mathlib/MeasureTheory/Measure/Dirac/Def.lean new file mode 100644 index 00000000000000..8ef25fb37fb7fa --- /dev/null +++ b/Mathlib/MeasureTheory/Measure/Dirac/Def.lean @@ -0,0 +1,79 @@ +/- +Copyright (c) 2018 Johannes Hölzl. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johannes Hölzl +-/ +module + +public import Mathlib.MeasureTheory.Measure.Module + +/-! +# Dirac measure + +In this file we define the Dirac measure `MeasureTheory.Measure.dirac a` +and prove some basic facts about it. +-/ + +@[expose] public section + +open Function Set +open scoped ENNReal NNReal + +noncomputable section + +variable {α : Type*} [MeasurableSpace α] {s : Set α} {a : α} + +namespace MeasureTheory.Measure + +/-- The dirac measure. -/ +def dirac (a : α) : Measure α := (OuterMeasure.dirac a).toMeasure (by simp) + +instance : MeasureSpace PUnit := + ⟨dirac PUnit.unit⟩ + +theorem le_dirac_apply {a} : s.indicator 1 a ≤ dirac a s := + OuterMeasure.dirac_apply a s ▸ le_toMeasure_apply _ _ _ + +@[simp] +theorem dirac_apply' (a : α) (hs : MeasurableSet s) : dirac a s = s.indicator 1 a := + toMeasure_apply _ _ hs + +theorem dirac_apply_eq_zero_or_one : + dirac a s = 0 ∨ dirac a s = 1 := by + rw [← measure_toMeasurable s, dirac_apply' a (measurableSet_toMeasurable ..), indicator] + simp only [Pi.one_apply, ite_eq_right_iff, one_ne_zero, imp_false, ite_eq_left_iff, zero_ne_one, + not_not] + tauto + +@[simp] +theorem dirac_apply_ne_zero_iff_eq_one : + dirac a s ≠ 0 ↔ dirac a s = 1 where + mp := dirac_apply_eq_zero_or_one.resolve_left + mpr := ne_zero_of_eq_one + +@[simp] +theorem dirac_apply_ne_one_iff_eq_zero : + dirac a s ≠ 1 ↔ dirac a s = 0 where + mp := dirac_apply_eq_zero_or_one.resolve_right + mpr h := h ▸ zero_ne_one + +@[simp] +theorem dirac_apply_of_mem {a : α} (h : a ∈ s) : dirac a s = 1 := by + have : ∀ t : Set α, a ∈ t → t.indicator (1 : α → ℝ≥0∞) a = 1 := fun t ht => indicator_of_mem ht 1 + refine le_antisymm (this univ trivial ▸ ?_) (this s h ▸ le_dirac_apply) + rw [← dirac_apply' a MeasurableSet.univ] + exact measure_mono (subset_univ s) + +@[simp] +theorem dirac_apply [MeasurableSingletonClass α] (a : α) (s : Set α) : + dirac a s = s.indicator 1 a := by + by_cases h : a ∈ s; · rw [dirac_apply_of_mem h, indicator_of_mem h, Pi.one_apply] + rw [indicator_of_notMem h, ← nonpos_iff_eq_zero] + calc + dirac a s ≤ dirac a {a}ᶜ := measure_mono (subset_compl_comm.1 <| singleton_subset_iff.2 h) + _ = 0 := by simp [dirac_apply' _ (measurableSet_singleton _).compl] + +@[simp] lemma dirac_ne_zero : dirac a ≠ 0 := + fun h ↦ by simpa [h] using dirac_apply_of_mem (mem_univ a) + +end MeasureTheory.Measure diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean index 08ec24dc5ac659..7d04b5e4e12094 100644 --- a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean @@ -928,25 +928,24 @@ lemma map_apply (ν : FiniteMeasure Ω) {f : Ω → Ω'} (f_mble : Measurable f) @[simp] lemma map_add {f : Ω → Ω'} (f_mble : Measurable f) (ν₁ ν₂ : FiniteMeasure Ω) : (ν₁ + ν₂).map f = ν₁.map f + ν₂.map f := by ext; simp [*] -@[simp] lemma map_smul {f : Ω → Ω'} (c : ℝ≥0) (ν : FiniteMeasure Ω) : +@[simp] lemma map_smul {f : Ω → Ω'} (c : ℝ≥0) {ν : FiniteMeasure Ω} (hf : AEMeasurable f ν) : (c • ν).map f = c • (ν.map f) := by ext s _ - simp [toMeasure_smul] + simp [toMeasure_smul, hf] /-- The push-forward of a finite measure by a function between measurable spaces as a linear map. -/ noncomputable def mapHom {f : Ω → Ω'} (f_mble : Measurable f) : FiniteMeasure Ω →ₗ[ℝ≥0] FiniteMeasure Ω' where toFun := fun ν ↦ ν.map f map_add' := map_add f_mble - map_smul' := map_smul + map_smul' m _ := map_smul m f_mble.aemeasurable -lemma mass_map_le (f : Ω → Ω') (μ : FiniteMeasure Ω) : (μ.map f).mass ≤ μ.mass := by +lemma mass_map_le {f : Ω → Ω'} {μ : FiniteMeasure Ω} (hf : AEMeasurable f μ) : + (μ.map f).mass ≤ μ.mass := by simp only [mass, coeFn_def, toMeasure_map, ne_eq, measure_ne_top, not_false_eq_true, ENNReal.toNNReal_le_toNNReal] - by_cases hf : AEMeasurable f μ - · rw [Measure.map_apply_of_aemeasurable hf MeasurableSet.univ] - exact measure_mono (subset_univ _) - · simp [Measure.map_of_not_aemeasurable hf] + rw [Measure.map_apply_of_aemeasurable hf MeasurableSet.univ] + exact measure_mono (subset_univ _) variable [TopologicalSpace Ω] [OpensMeasurableSpace Ω] variable [TopologicalSpace Ω'] [BorelSpace Ω'] @@ -980,7 +979,7 @@ noncomputable def mapCLM {f : Ω → Ω'} (f_cont : Continuous f) : FiniteMeasure Ω →L[ℝ≥0] FiniteMeasure Ω' where toFun := fun ν ↦ ν.map f map_add' := map_add f_cont.measurable - map_smul' := map_smul + map_smul' m _ := map_smul m f_cont.aemeasurable lemma Topology.IsClosedEmbedding.isEmbedding_map_finiteMeasure {Ω : Type*} [MeasurableSpace Ω] [TopologicalSpace Ω] [BorelSpace Ω] [NormalSpace Ω'] diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean index cd7c32276d72d9..2b804c058044f6 100644 --- a/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean +++ b/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean @@ -117,26 +117,23 @@ lemma prod_apply_symm (s : Set (α × β)) (s_mble : MeasurableSet s) : simp [coeFn_def] /-- The first marginal of a product probability measure is the first probability measure. -/ -@[simp] lemma map_fst_prod : (μ.prod ν).map measurable_fst.aemeasurable = μ := by +@[simp] lemma map_fst_prod : (μ.prod ν).map Prod.fst = μ := by apply Subtype.ext - simp only [val_eq_to_measure, toMeasure_map, toMeasure_prod, Measure.map_fst_prod, - measure_univ, one_smul] + simp /-- The second marginal of a product probability measure is the second probability measure. -/ -@[simp] lemma map_snd_prod : (μ.prod ν).map measurable_snd.aemeasurable = ν := by +@[simp] lemma map_snd_prod : (μ.prod ν).map Prod.snd = ν := by apply Subtype.ext - simp only [val_eq_to_measure, toMeasure_map, toMeasure_prod, Measure.map_snd_prod, - measure_univ, one_smul] + simp lemma map_prod_map {α' : Type*} [MeasurableSpace α'] {β' : Type*} [MeasurableSpace β'] {f : α → α'} {g : β → β'} (f_mble : Measurable f) (g_mble : Measurable g) : - (μ.map f_mble.aemeasurable).prod (ν.map g_mble.aemeasurable) - = (μ.prod ν).map (f_mble.prodMap g_mble).aemeasurable := by + (μ.map f).prod (ν.map g) = (μ.prod ν).map (Prod.map f g) := by apply Subtype.ext simp only [val_eq_to_measure, toMeasure_prod, toMeasure_map] rw [Measure.map_prod_map _ _ f_mble g_mble] -lemma prod_swap : (μ.prod ν).map measurable_swap.aemeasurable = ν.prod μ := by +lemma prod_swap : (μ.prod ν).map Prod.swap = ν.prod μ := by apply Subtype.ext simp [Measure.prod_swap] diff --git a/Mathlib/MeasureTheory/Measure/GiryMonad.lean b/Mathlib/MeasureTheory/Measure/GiryMonad.lean index 783072dfde0b1d..6e7ae7b53a019f 100644 --- a/Mathlib/MeasureTheory/Measure/GiryMonad.lean +++ b/Mathlib/MeasureTheory/Measure/GiryMonad.lean @@ -236,10 +236,11 @@ theorem bind_apply {m : Measure α} {f : α → Measure β} {s : Set β} (hs : M (hf : AEMeasurable f m) : bind m f s = ∫⁻ a, f a s ∂m := by rw [bind, join_apply hs, lintegral_map' (measurable_coe hs).aemeasurable hf] -theorem bind_apply_le {m : Measure α} (f : α → Measure β) {s : Set β} (hs : MeasurableSet s) : +theorem bind_apply_le {m : Measure α} {f : α → Measure β} (hf : AEMeasurable f m) {s : Set β} + (hs : MeasurableSet s) : bind m f s ≤ ∫⁻ a, f a s ∂m := by rw [bind, join_apply hs] - apply lintegral_map_le + apply lintegral_map_le _ hf theorem ae_ae_of_ae_bind {m : Measure α} {f : α → Measure β} {p : β → Prop} (hf : AEMeasurable f m) (h : ∀ᵐ b ∂m.bind f, p b) : ∀ᵐ a ∂m, ∀ᵐ b ∂f a, p b := @@ -279,16 +280,17 @@ theorem bind_sum {ι : Type*} (m : ι → Measure α) (f : α → Measure β) simp_rw [bind, map_sum h, join_sum] lemma bind_smul {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (c : R) (m : Measure α) - (f : α → Measure β) : (c • m).bind f = c • (m.bind f) := by - simp_rw [bind, Measure.map_smul, join_smul] + {f : α → Measure β} (hf : AEMeasurable f m) : (c • m).bind f = c • (m.bind f) := by + simp_rw [bind, Measure.map_smul _ hf, join_smul] theorem lintegral_bind {m : Measure α} {μ : α → Measure β} {f : β → ℝ≥0∞} (hμ : AEMeasurable μ m) (hf : AEMeasurable f (bind m μ)) : ∫⁻ x, f x ∂bind m μ = ∫⁻ a, ∫⁻ x, f x ∂μ a ∂m := (lintegral_join hf).trans (lintegral_map' (aemeasurable_lintegral hf) hμ) -theorem lintegral_bind_le (f : β → ℝ≥0∞) (m : Measure α) (μ : α → Measure β) : +theorem lintegral_bind_le (f : β → ℝ≥0∞) (m : Measure α) {μ : α → Measure β} + (hμ : AEMeasurable μ m) : ∫⁻ x, f x ∂bind m μ ≤ ∫⁻ a, ∫⁻ x, f x ∂μ a ∂m := - (lintegral_join_le _ _).trans (lintegral_map_le _ _) + (lintegral_join_le _ _).trans (lintegral_map_le _ hμ) theorem bind_bind {γ} [MeasurableSpace γ] {m : Measure α} {f : α → Measure β} {g : β → Measure γ} (hf : AEMeasurable f m) (hg : AEMeasurable g (m.bind f)) : diff --git a/Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean b/Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean index 02e80e2e752add..5448254a016ec7 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean @@ -100,7 +100,7 @@ theorem LinearMap.exists_map_addHaar_eq_smul_addHaar' (h : Function.Surjective L (addHaarScalarFactor_pos_of_isAddHaarMeasure (μT.map L') ν).ne' refine ⟨c₀ * c₁, by simp [pos_iff_ne_zero, c₀_pos, c₁_pos], ENNReal.mul_lt_top c₀_fin.lt_top c₁_fin.lt_top, ?_⟩ - simp only [I, h₀, Measure.map_smul, J, smul_smul, h₁] + simp only [I, h₀, Measure.map_smul, J, smul_smul, h₁, P_cont.aemeasurable, L'_cont.aemeasurable] rw [mul_assoc, mul_comm _ c₁, ← mul_assoc] /-- The image of an additive Haar measure under a surjective linear map is proportional to a given diff --git a/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean b/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean index e56cf9be86749a..0b9a5a22423865 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean @@ -228,5 +228,5 @@ theorem MeasureTheory.volume_eq_of_finrank_eq_one (h : Module.finrank ℝ E = 1) ext x simp [f, mul_comm, smul_smul] _ = ‖v‖ₑ • (volume : Measure ℝ).map (· • v) := by - rw [map_addHaar_smul _ (by simpa using hv)] + rw [map_addHaar_smul _ (by simpa using hv), Measure.map_smul _ (by fun_prop)] simp diff --git a/Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.lean b/Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.lean index 64aa4053868516..183507d645e9f8 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.lean @@ -56,7 +56,7 @@ lemma mulEquivHaarChar_eq (μ : Measure G) [IsHaarMeasure μ] conv => enter [1, 2, 2] rw [smul] - simp_rw [MeasureTheory.Measure.map_smul] + rw! [MeasureTheory.Measure.map_smul _ (by fun_prop)] exact haarScalarFactor_smul_smul _ _ (haarScalarFactor_pos_of_isHaarMeasure haar μ).ne' @[to_additive addEquivAddHaarChar_smul_map] diff --git a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean index 3b097929dd2aba..d8f27cee36e757 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean @@ -985,7 +985,7 @@ instance (priority := 100) IsHaarMeasure.isInvInvariant_of_regular let c : ℝ≥0∞ := haarScalarFactor μ.inv μ have hc : μ.inv = c • μ := isMulLeftInvariant_eq_smul_of_regular μ.inv μ have : map Inv.inv (map Inv.inv μ) = c ^ 2 • μ := by - rw [← inv_def μ, hc, Measure.map_smul, ← inv_def μ, hc, smul_smul, pow_two] + rw [← inv_def μ, hc, Measure.map_smul _ (by fun_prop), ← inv_def μ, hc, smul_smul, pow_two] have μeq : μ = c ^ 2 • μ := by rw [map_map continuous_inv.measurable continuous_inv.measurable] at this simpa only [inv_involutive, Involutive.comp_self, Measure.map_id] @@ -1011,7 +1011,7 @@ instance (priority := 100) IsHaarMeasure.isInvInvariant_of_innerRegular let c : ℝ≥0∞ := haarScalarFactor μ.inv μ have hc : μ.inv = c • μ := isMulLeftInvariant_eq_smul_of_innerRegular μ.inv μ have : map Inv.inv (map Inv.inv μ) = c ^ 2 • μ := by - rw [← inv_def μ, hc, Measure.map_smul, ← inv_def μ, hc, smul_smul, pow_two] + rw [← inv_def μ, hc, Measure.map_smul _ (by fun_prop), ← inv_def μ, hc, smul_smul, pow_two] have μeq : μ = c ^ 2 • μ := by rw [map_map continuous_inv.measurable continuous_inv.measurable] at this simpa only [inv_involutive, Involutive.comp_self, Measure.map_id] diff --git a/Mathlib/MeasureTheory/Measure/IntegralCharFun.lean b/Mathlib/MeasureTheory/Measure/IntegralCharFun.lean index dabe96f4ec7c91..c4d662dfde6804 100644 --- a/Mathlib/MeasureTheory/Measure/IntegralCharFun.lean +++ b/Mathlib/MeasureTheory/Measure/IntegralCharFun.lean @@ -151,7 +151,6 @@ lemma measureReal_abs_dual_gt_le_integral_charFunDual {E : Type*} [NormedAddComm [NormedSpace ℝ E] {mE : MeasurableSpace E} [OpensMeasurableSpace E] {μ : Measure E} [IsProbabilityMeasure μ] (L : StrongDual ℝ E) {r : ℝ} (hr : 0 < r) : μ.real {x | r < |L x|} ≤ 2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - charFunDual μ (t • L)‖ := by - have : IsProbabilityMeasure (μ.map L) := Measure.isProbabilityMeasure_map (by fun_prop) convert! measureReal_abs_gt_le_integral_charFun (μ := μ.map L) hr with x · rw [map_measureReal_apply (by fun_prop)] · simp @@ -164,8 +163,6 @@ lemma measureReal_abs_inner_gt_le_integral_charFun {E : Type*} [SeminormedAddCom [InnerProductSpace ℝ E] {mE : MeasurableSpace E} [OpensMeasurableSpace E] {μ : Measure E} [IsProbabilityMeasure μ] {a : E} {r : ℝ} (hr : 0 < r) : μ.real {x | r < |⟪a, x⟫|} ≤ 2⁻¹ * r * ‖∫ t in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ (t • a)‖ := by - have : IsProbabilityMeasure (μ.map (fun x ↦ ⟪a, x⟫)) := - Measure.isProbabilityMeasure_map (by fun_prop) convert! measureReal_abs_gt_le_integral_charFun (μ := μ.map (fun x ↦ ⟪a, x⟫)) hr with x · rw [map_measureReal_apply (by fun_prop)] · simp diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean index 61792c16573586..3ae55431909f6f 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean @@ -417,6 +417,8 @@ theorem map_matrix_volume_pi_eq_smul_volume_pi [DecidableEq ι] {M : Matrix ι · intro A B _ _ IHA IHB rw [toLin'_mul, det_mul, LinearMap.coe_comp, ← Measure.map_map, IHB, Measure.map_smul, IHA, smul_smul, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul, mul_comm, mul_inv] + · apply Continuous.aemeasurable + apply LinearMap.continuous_on_pi · apply Continuous.measurable apply LinearMap.continuous_on_pi · apply Continuous.measurable diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean index c22322acd7ddfc..58e8db04a65a8f 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean @@ -222,7 +222,7 @@ theorem map_linearMap_addHaar_pi_eq_smul_addHaar {ι : Type*} [Finite ι] {f : ( /- We have already proved the result for the Lebesgue product measure, using matrices. We deduce it for any Haar measure by uniqueness (up to scalar multiplication). -/ have := addHaarMeasure_unique μ (piIcc01 ι) - rw [this, addHaarMeasure_eq_volume_pi, Measure.map_smul, + rw [this, addHaarMeasure_eq_volume_pi, Measure.map_smul _ (by fun_prop), Real.map_linearMap_volume_pi_eq_smul_volume_pi hf, smul_comm] variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] @@ -252,7 +252,7 @@ theorem map_linearMap_addHaar_eq_smul_addHaar {f : E →ₗ[ℝ] E} (hf : Linear have : IsAddHaarMeasure (map e μ) := (e : E ≃+ (ι → ℝ)).isAddHaarMeasure_map μ Ce Cesymm have ecomp : e.symm ∘ e = id := by ext x; simp only [id, Function.comp_apply, LinearEquiv.symm_apply_apply] - rw [map_linearMap_addHaar_pi_eq_smul_addHaar hf (map e μ), Measure.map_smul, + rw [map_linearMap_addHaar_pi_eq_smul_addHaar hf (map e μ), Measure.map_smul _ (by fun_prop), map_map Cesymm.measurable Ce.measurable, ecomp, Measure.map_id] /-- The preimage of a set `s` under a linear map `f` with nonzero determinant has measure @@ -417,7 +417,7 @@ general Haar measures on general commutative groups. -/ theorem addHaar_ball_center {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [IsAddHaarMeasure μ] (x : E) (r : ℝ) : μ (ball x r) = μ (ball (0 : E) r) := by - have : ball (0 : E) r = (x + ·) ⁻¹' ball x r := by simp [preimage_add_ball] + have : ball (0 : E) r = (x + ·) ⁻¹' ball x r := by simp rw [this, measure_preimage_add] theorem addHaar_real_ball_center {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E] @@ -428,7 +428,7 @@ theorem addHaar_real_ball_center {E : Type*} [NormedAddCommGroup E] [MeasurableS theorem addHaar_closedBall_center {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [IsAddHaarMeasure μ] (x : E) (r : ℝ) : μ (closedBall x r) = μ (closedBall (0 : E) r) := by - have : closedBall (0 : E) r = (x + ·) ⁻¹' closedBall x r := by simp [preimage_add_closedBall] + have : closedBall (0 : E) r = (x + ·) ⁻¹' closedBall x r := by simp rw [this, measure_preimage_add] theorem addHaar_real_closedBall_center {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E] diff --git a/Mathlib/MeasureTheory/Measure/Map.lean b/Mathlib/MeasureTheory/Measure/Map.lean index 8bc220441e4cde..7abf0212ddd24b 100644 --- a/Mathlib/MeasureTheory/Measure/Map.lean +++ b/Mathlib/MeasureTheory/Measure/Map.lean @@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro module public import Mathlib.MeasureTheory.MeasurableSpace.Embedding +public import Mathlib.MeasureTheory.Measure.Dirac.Def public import Mathlib.MeasureTheory.Measure.Filter /-! @@ -84,13 +85,25 @@ theorem mapₗ_congr {f g : α → β} (hf : Measurable f) (hg : Measurable g) ( simpa only [mapₗ, hf, hg, hs, dite_eq_left, liftLinear_apply, OuterMeasure.map_apply] using! measure_congr (h.preimage s) +private lemma nonempty_of_not_aemeasurable {f : α → β} (hf : ¬AEMeasurable f μ) : + Nonempty β := by + contrapose! hf + exact (measurable_of_empty_codomain f).aemeasurable + open scoped Classical in -/-- The pushforward of a measure. It is defined to be `0` if `f` is not an almost everywhere -measurable function. -/ +/-- The pushforward of a measure. If `f` is not an almost everywhere measurable function, +we define it to be `0` if `μ = 0`, and to be an arbitrary Dirac mass otherwise. That way +we always have `map f 0 = 0`, and the push-forward of a probability measure is always a +probability measure. -/ noncomputable irreducible_def map [MeasurableSpace α] [MeasurableSpace β] (f : α → β) (μ : Measure α) : Measure β := - if hf : AEMeasurable f μ then mapₗ (hf.mk f) μ else 0 + if hf : AEMeasurable f μ + then mapₗ (hf.mk f) μ + else if μ = 0 then 0 + else + haveI : Nonempty β := by exact nonempty_of_not_aemeasurable hf + dirac Classical.ofNonempty theorem mapₗ_mk_apply_of_aemeasurable {f : α → β} (hf : AEMeasurable f μ) : mapₗ (hf.mk f) μ = map f μ := by simp [map, hf] @@ -109,11 +122,10 @@ protected theorem map_zero (f : α → β) : (0 : Measure α).map f = 0 := by by_cases hf : AEMeasurable f (0 : Measure α) <;> simp [map, hf] @[simp] -theorem map_of_not_aemeasurable {f : α → β} {μ : Measure α} (hf : ¬AEMeasurable f μ) : - μ.map f = 0 := by simp [map, hf] - -theorem _root_.AEMeasurable.of_map_ne_zero {f : α → β} {μ : Measure α} (hf : μ.map f ≠ 0) : - AEMeasurable f μ := not_imp_comm.1 map_of_not_aemeasurable hf +theorem map_of_not_aemeasurable_of_ne_zero {f : α → β} {μ : Measure α} (hf : ¬AEMeasurable f μ) + (hμ : μ ≠ 0) : + haveI : Nonempty β := by exact nonempty_of_not_aemeasurable hf + μ.map f = dirac Classical.ofNonempty := by simp [map, hf, hμ] theorem map_congr {f g : α → β} (h : f =ᵐ[μ] g) : Measure.map f μ = Measure.map g μ := by by_cases hf : AEMeasurable f μ @@ -122,26 +134,23 @@ theorem map_congr {f g : α → β} (h : f =ᵐ[μ] g) : Measure.map f μ = Meas exact mapₗ_congr hf.measurable_mk hg.measurable_mk (hf.ae_eq_mk.symm.trans (h.trans hg.ae_eq_mk)) · have hg : ¬AEMeasurable g μ := by simpa [← aemeasurable_congr h] using hf - simp [map_of_not_aemeasurable, hf, hg] + obtain rfl | hμ := eq_or_ne μ 0 + · simp + simp [map_of_not_aemeasurable_of_ne_zero, hf, hg, hμ] @[simp] protected theorem map_smul {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] - (c : R) (μ : Measure α) (f : α → β) : (c • μ).map f = c • μ.map f := by + (c : R) {μ : Measure α} {f : α → β} (hf : AEMeasurable f μ) : (c • μ).map f = c • μ.map f := by suffices ∀ c : ℝ≥0∞, (c • μ).map f = c • μ.map f by simpa using this (c • 1) clear c; intro c rcases eq_or_ne c 0 with (rfl | hc); · simp - by_cases hf : AEMeasurable f μ - · have hfc : AEMeasurable f (c • μ) := - ⟨hf.mk f, hf.measurable_mk, (ae_ennreal_smul_measure_iff hc).2 hf.ae_eq_mk⟩ - simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hfc, map_smulₛₗ, - RingHom.id_apply] - congr 1 - apply mapₗ_congr hfc.measurable_mk hf.measurable_mk - exact .trans ((ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk.symm) hf.ae_eq_mk - · have hfc : ¬AEMeasurable f (c • μ) := by - intro hfc - exact hf ⟨hfc.mk f, hfc.measurable_mk, (ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk⟩ - simp [map_of_not_aemeasurable hf, map_of_not_aemeasurable hfc] + have hfc : AEMeasurable f (c • μ) := + ⟨hf.mk f, hf.measurable_mk, (ae_ennreal_smul_measure_iff hc).2 hf.ae_eq_mk⟩ + simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hfc, map_smulₛₗ, + RingHom.id_apply] + congr 1 + apply mapₗ_congr hfc.measurable_mk hf.measurable_mk + exact .trans ((ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk.symm) hf.ae_eq_mk variable {f : α → β} @@ -177,14 +186,10 @@ theorem map_toOuterMeasure (hf : AEMeasurable f μ) : /-- If `map f μ = μ`, then the measure of the preimage of any null measurable set `s` is equal to the measure of `s`. Note that this lemma does not assume (a.e.) measurability of `f`. -/ -lemma measure_preimage_of_map_eq_self {f : α → α} (hf : map f μ = μ) +lemma measure_preimage_of_map_eq_self {f : α → α} (hf : map f μ = μ) (hfm : AEMeasurable f μ) {s : Set α} (hs : NullMeasurableSet s μ) : μ (f ⁻¹' s) = μ s := by - if hfm : AEMeasurable f μ then - rw [← map_apply₀ hfm, hf] - rwa [hf] - else - rw [map_of_not_aemeasurable hfm] at hf - simp [← hf] + rw [← map_apply₀ hfm, hf] + rwa [hf] lemma map_ne_zero_iff (hf : AEMeasurable f μ) : μ.map f ≠ 0 ↔ μ ≠ 0 := (map_eq_zero_iff hf).not lemma mapₗ_ne_zero_iff (hf : Measurable f) : Measure.mapₗ f μ ≠ 0 ↔ μ ≠ 0 := @@ -249,13 +254,11 @@ theorem ae_of_ae_map {f : α → β} (hf : AEMeasurable f μ) {p : β → Prop} ∀ᵐ x ∂μ, p (f x) := mem_ae_of_mem_ae_map hf h -theorem ae_map_mem_range {m0 : MeasurableSpace α} (f : α → β) (hf : MeasurableSet (range f)) - (μ : Measure α) : ∀ᵐ x ∂μ.map f, x ∈ range f := by - by_cases h : AEMeasurable f μ - · change range f ∈ ae (μ.map f) - rw [mem_ae_map_iff h hf] - filter_upwards using mem_range_self - · simp [map_of_not_aemeasurable h] +theorem ae_map_mem_range {m0 : MeasurableSpace α} {f : α → β} (hf : MeasurableSet (range f)) + {μ : Measure α} (h : AEMeasurable f μ) : ∀ᵐ x ∂μ.map f, x ∈ range f := by + change range f ∈ ae (μ.map f) + rw [mem_ae_map_iff h hf] + filter_upwards using mem_range_self end MeasureTheory diff --git a/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean b/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean index e9cb17f2c1a90a..9e07f59a285aec 100644 --- a/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean @@ -605,29 +605,29 @@ variable {Ω Ω' : Type*} [MeasurableSpace Ω] [MeasurableSpace Ω'] namespace ProbabilityMeasure /-- The push-forward of a probability measure by a measurable function. -/ -noncomputable def map (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν) : +noncomputable def map (ν : ProbabilityMeasure Ω) (f : Ω → Ω') : ProbabilityMeasure Ω' := - ⟨(ν : Measure Ω).map f, (ν : Measure Ω).isProbabilityMeasure_map f_aemble⟩ + ⟨(ν : Measure Ω).map f, inferInstance⟩ -@[simp] lemma toMeasure_map (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (hf : AEMeasurable f ν) : - (ν.map hf).toMeasure = ν.toMeasure.map f := rfl +@[simp] lemma toMeasure_map (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} : + (ν.map f).toMeasure = ν.toMeasure.map f := rfl /-- Note that this is an equality of elements of `ℝ≥0∞`. See also `MeasureTheory.ProbabilityMeasure.map_apply` for the corresponding equality as elements of `ℝ≥0`. -/ lemma map_apply' (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν) {A : Set Ω'} (A_mble : MeasurableSet A) : - (ν.map f_aemble : Measure Ω') A = (ν : Measure Ω) (f ⁻¹' A) := + (ν.map f : Measure Ω') A = (ν : Measure Ω) (f ⁻¹' A) := Measure.map_apply_of_aemeasurable f_aemble A_mble lemma map_apply_of_aemeasurable (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν) {A : Set Ω'} (A_mble : MeasurableSet A) : - (ν.map f_aemble) A = ν (f ⁻¹' A) := by + (ν.map f) A = ν (f ⁻¹' A) := by exact (ENNReal.toNNReal_eq_toNNReal_iff' (measure_ne_top _ _) (measure_ne_top _ _)).mpr <| ν.map_apply' f_aemble A_mble lemma map_apply (ν : ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ν) {A : Set Ω'} (A_mble : MeasurableSet A) : - (ν.map f_aemble) A = ν (f ⁻¹' A) := + (ν.map f) A = ν (f ⁻¹' A) := map_apply_of_aemeasurable ν f_aemble A_mble variable [TopologicalSpace Ω] [OpensMeasurableSpace Ω] @@ -639,8 +639,7 @@ distribution) of the push-forwards of these measures by `f`. -/ lemma tendsto_map_of_tendsto_of_continuous {ι : Type*} {L : Filter ι} (νs : ι → ProbabilityMeasure Ω) (ν : ProbabilityMeasure Ω) (lim : Tendsto νs L (𝓝 ν)) {f : Ω → Ω'} (f_cont : Continuous f) : - Tendsto (fun i ↦ (νs i).map f_cont.measurable.aemeasurable) L - (𝓝 (ν.map f_cont.measurable.aemeasurable)) := by + Tendsto (fun i ↦ (νs i).map f) L (𝓝 (ν.map f)) := by rw [ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto] at lim ⊢ intro g convert! lim (g.compContinuous ⟨f, f_cont⟩) <;> @@ -652,7 +651,7 @@ lemma tendsto_map_of_tendsto_of_continuous {ι : Type*} {L : Filter ι} the push-forward of probability measures `f* : ProbabilityMeasure X → ProbabilityMeasure Y` is continuous (in the topologies of convergence in distribution). -/ lemma continuous_map {f : Ω → Ω'} (f_cont : Continuous f) : - Continuous (fun ν ↦ ProbabilityMeasure.map ν f_cont.measurable.aemeasurable) := by + Continuous (fun ν ↦ ProbabilityMeasure.map ν f) := by rw [continuous_iff_continuousAt] exact fun _ ↦ tendsto_map_of_tendsto_of_continuous _ _ continuous_id.continuousAt f_cont diff --git a/Mathlib/MeasureTheory/Measure/Prod.lean b/Mathlib/MeasureTheory/Measure/Prod.lean index 794adb30a94b71..d142811d44dde2 100644 --- a/Mathlib/MeasureTheory/Measure/Prod.lean +++ b/Mathlib/MeasureTheory/Measure/Prod.lean @@ -178,11 +178,13 @@ theorem volume_eq_prod (α β) [MeasureSpace α] [MeasureSpace β] : (volume : Measure (α × β)) = (volume : Measure α).prod (volume : Measure β) := rfl +variable [SFinite ν] + /-- For an s-finite measure `ν`, see `prod_apply` below. -/ theorem prod_apply_le {s : Set (α × β)} (hs : MeasurableSet s) : μ.prod ν s ≤ ∫⁻ x, ν (Prod.mk x ⁻¹' s) ∂μ := by simp only [Measure.prod, ← map_apply measurable_prodMk_left hs] - exact bind_apply_le _ hs + exact bind_apply_le Measurable.map_prodMk_left.aemeasurable hs /-- For any measures `μ` and `ν` and any sets `s` and `t`, we have `μ.prod ν (s ×ˢ t) ≤ μ s * ν t`. @@ -218,8 +220,6 @@ instance prod.instNullSingletonClass_snd [NullSingletonClass ν] : _ ≤ μ {x} * ν {y} := prod_prod_le _ _ _ = 0 := by simp -variable [SFinite ν] - theorem prod_apply {s : Set (α × β)} (hs : MeasurableSet s) : μ.prod ν s = ∫⁻ x, ν (Prod.mk x ⁻¹' s) ∂μ := by simp_rw [Measure.prod, bind_apply hs (Measurable.map_prodMk_left (ν := ν)).aemeasurable, @@ -286,7 +286,7 @@ instance {X Y : Type*} prod.instIsOpenPosMeasure protected theorem FiniteAtFilter.prod {X Y : Type*} {m : MeasurableSpace X} {μ : Measure X} - {m' : MeasurableSpace Y} {ν : Measure Y} {l : Filter X} {l' : Filter Y} + {m' : MeasurableSpace Y} {ν : Measure Y} [SFinite ν] {l : Filter X} {l' : Filter Y} (hμ : μ.FiniteAtFilter l) (hν : ν.FiniteAtFilter l') : (μ.prod ν).FiniteAtFilter (l ×ˢ l') := by rcases hμ with ⟨s, hs, hμs⟩ @@ -297,14 +297,15 @@ protected theorem FiniteAtFilter.prod {X Y : Type*} {m : MeasurableSpace X} {μ instance prod.instIsLocallyFiniteMeasure {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {m : MeasurableSpace X} {μ : Measure X} [IsLocallyFiniteMeasure μ] {m' : MeasurableSpace Y} - {ν : Measure Y} [IsLocallyFiniteMeasure ν] : IsLocallyFiniteMeasure (μ.prod ν) where + {ν : Measure Y} [SFinite ν] [IsLocallyFiniteMeasure ν] : IsLocallyFiniteMeasure (μ.prod ν) where finiteAtNhds x := by rw [nhds_prod_eq] exact μ.finiteAt_nhds _ |>.prod <| ν.finiteAt_nhds _ instance {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {m : MeasureSpace X} [IsLocallyFiniteMeasure (volume : Measure X)] - {m' : MeasureSpace Y} [IsLocallyFiniteMeasure (volume : Measure Y)] : + {m' : MeasureSpace Y} [IsLocallyFiniteMeasure (volume : Measure Y)] + [SFinite (volume : Measure Y)] : IsLocallyFiniteMeasure (volume : Measure (X × Y)) := prod.instIsLocallyFiniteMeasure @@ -330,7 +331,7 @@ instance {α β : Type*} [MeasureSpace α] [MeasureSpace β] prod.instIsProbabilityMeasure _ _ instance prod.instIsFiniteMeasureOnCompacts {α β : Type*} [TopologicalSpace α] [TopologicalSpace β] - {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : Measure α) (ν : Measure β) + {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : Measure α) (ν : Measure β) [SFinite ν] [IsFiniteMeasureOnCompacts μ] [IsFiniteMeasureOnCompacts ν] : IsFiniteMeasureOnCompacts (μ.prod ν) where lt_top_of_isCompact K hK := calc @@ -341,7 +342,8 @@ instance prod.instIsFiniteMeasureOnCompacts {α β : Type*} [TopologicalSpace α instance {X Y : Type*} [TopologicalSpace X] [MeasureSpace X] [IsFiniteMeasureOnCompacts (volume : Measure X)] - [TopologicalSpace Y] [MeasureSpace Y] [IsFiniteMeasureOnCompacts (volume : Measure Y)] : + [TopologicalSpace Y] [MeasureSpace Y] [IsFiniteMeasureOnCompacts (volume : Measure Y)] + [SFinite (volume : Measure Y)] : IsFiniteMeasureOnCompacts (volume : Measure (X × Y)) := prod.instIsFiniteMeasureOnCompacts _ _ @@ -381,7 +383,7 @@ then `s` has `μ.prod ν` measure zero. This implication requires `s` to be measurable but does not require `ν` to be s-finite. See also `measure_prod_null` and `measure_ae_null_of_prod_null` below. -/ -theorem measure_prod_null_of_ae_null {s : Set (α × β)} (hsm : MeasurableSet s) +theorem measure_prod_null_of_ae_null [SFinite ν] {s : Set (α × β)} (hsm : MeasurableSet s) (hs : (fun x => ν (Prod.mk x ⁻¹' s)) =ᵐ[μ] 0) : μ.prod ν s = 0 := by rw [← nonpos_iff_eq_zero] calc @@ -411,7 +413,6 @@ theorem measure_ae_null_of_prod_null {s : Set (α × β)} (h : μ.prod ν s = 0) ⟨EventuallyLE.trans_eq (Eventually.of_forall fun x => measure_mono (preimage_mono hst)) ht, Eventually.of_forall fun x => zero_le⟩ -omit [SFinite ν] in theorem AbsolutelyContinuous.prod [SFinite ν'] (h1 : μ ≪ μ') (h2 : ν ≪ ν') : μ.prod ν ≪ μ'.prod ν' := by refine AbsolutelyContinuous.mk fun s hs h2s => ?_ @@ -419,7 +420,6 @@ theorem AbsolutelyContinuous.prod [SFinite ν'] (h1 : μ ≪ μ') (h2 : ν ≪ rw [measure_prod_null hs] at h2s exact (h2s.filter_mono h1.ae_le).mono fun _ h => h2 h -omit [SFinite ν] in @[gcongr] theorem prod_mono [SFinite ν'] (h1 : μ ≤ μ') (h2 : ν ≤ ν') : μ.prod ν ≤ μ'.prod ν' := by apply Measure.le_iff.2 (fun s hs ↦ ?_) calc μ.prod ν s @@ -450,7 +450,6 @@ theorem ae_prod_mem_iff_ae_ae_mem {s : Set (α × β)} (hs : MeasurableSet s) : (∀ᵐ z ∂μ.prod ν, z ∈ s) ↔ ∀ᵐ x ∂μ, ∀ᵐ y ∂ν, (x, y) ∈ s := measure_prod_null hs.compl -omit [SFinite ν] in @[fun_prop] theorem quasiMeasurePreserving_fst : QuasiMeasurePreserving Prod.fst (μ.prod ν) μ := by refine ⟨measurable_fst, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩ @@ -458,7 +457,6 @@ theorem quasiMeasurePreserving_fst : QuasiMeasurePreserving Prod.fst (μ.prod ν refine (prod_prod_le _ _).trans_eq ?_ rw [h2s, zero_mul] -omit [SFinite ν] in @[fun_prop] theorem quasiMeasurePreserving_snd : QuasiMeasurePreserving Prod.snd (μ.prod ν) ν := by refine ⟨measurable_snd, AbsolutelyContinuous.mk fun s hs h2s => ?_⟩ @@ -466,7 +464,6 @@ theorem quasiMeasurePreserving_snd : QuasiMeasurePreserving Prod.snd (μ.prod ν refine (prod_prod_le _ _).trans_eq ?_ rw [h2s, mul_zero] -omit [SFinite ν] in lemma set_prod_ae_eq {s s' : Set α} {t t' : Set β} (hs : s =ᵐ[μ] s') (ht : t =ᵐ[ν] t') : (s ×ˢ t : Set (α × β)) =ᵐ[μ.prod ν] (s' ×ˢ t' : Set (α × β)) := (quasiMeasurePreserving_fst.preimage_ae_eq hs).inter @@ -478,7 +475,6 @@ lemma measure_prod_compl_eq_zero {s : Set α} {t : Set β} rw [Set.compl_prod_eq_union, measure_union_null_iff] simp [s_ae_univ, t_ae_univ] -omit [SFinite ν] in lemma _root_.MeasureTheory.NullMeasurableSet.prod {s : Set α} {t : Set β} (s_mble : NullMeasurableSet s μ) (t_mble : NullMeasurableSet t ν) : NullMeasurableSet (s ×ˢ t) (μ.prod ν) := @@ -920,12 +916,12 @@ theorem prod_of_left {α β γ} [MeasurableSpace α] [MeasurableSpace β] [Measu MeasurableEquiv.prodComm).quasiMeasurePreserving @[fun_prop] -protected theorem fst {f : α → β × γ} (hf : QuasiMeasurePreserving f μ (ν.prod τ)) : +protected theorem fst [SFinite τ] {f : α → β × γ} (hf : QuasiMeasurePreserving f μ (ν.prod τ)) : QuasiMeasurePreserving (fun x ↦ (f x).1) μ ν := (quasiMeasurePreserving_fst (μ := ν) (ν := τ)).comp hf @[fun_prop] -protected theorem snd {f : α → β × γ} (hf : QuasiMeasurePreserving f μ (ν.prod τ)) : +protected theorem snd [SFinite τ] {f : α → β × γ} (hf : QuasiMeasurePreserving f μ (ν.prod τ)) : QuasiMeasurePreserving (fun x ↦ (f x).2) μ τ := (quasiMeasurePreserving_snd (μ := ν) (ν := τ)).comp hf @@ -951,19 +947,19 @@ theorem AEMeasurable.prod_swap [SFinite μ] [SFinite ν] {f : β × α → γ} rw [← Measure.prod_swap] at hf exact hf.comp_measurable measurable_swap -theorem MeasureTheory.NullMeasurable.comp_fst {f : α → γ} (hf : NullMeasurable f μ) : +theorem MeasureTheory.NullMeasurable.comp_fst [SFinite ν] {f : α → γ} (hf : NullMeasurable f μ) : NullMeasurable (fun z : α × β => f z.1) (μ.prod ν) := hf.comp_quasiMeasurePreserving quasiMeasurePreserving_fst -theorem AEMeasurable.comp_fst {f : α → γ} (hf : AEMeasurable f μ) : +theorem AEMeasurable.comp_fst [SFinite ν] {f : α → γ} (hf : AEMeasurable f μ) : AEMeasurable (fun z : α × β => f z.1) (μ.prod ν) := hf.comp_quasiMeasurePreserving quasiMeasurePreserving_fst -theorem MeasureTheory.NullMeasurable.comp_snd {f : β → γ} (hf : NullMeasurable f ν) : +theorem MeasureTheory.NullMeasurable.comp_snd [SFinite ν] {f : β → γ} (hf : NullMeasurable f ν) : NullMeasurable (fun z : α × β => f z.2) (μ.prod ν) := hf.comp_quasiMeasurePreserving quasiMeasurePreserving_snd -theorem AEMeasurable.comp_snd {f : β → γ} (hf : AEMeasurable f ν) : +theorem AEMeasurable.comp_snd [SFinite ν] {f : β → γ} (hf : AEMeasurable f ν) : AEMeasurable (fun z : α × β => f z.2) (μ.prod ν) := hf.comp_quasiMeasurePreserving quasiMeasurePreserving_snd @@ -1010,10 +1006,11 @@ theorem lintegral_prod (f : α × β → ℝ≥0∞) (hf : AEMeasurable f (μ.pr exact lintegral_map' ha (by fun_prop) omit [SFinite ν] in -theorem lintegral_prod_le (f : α × β → ℝ≥0∞) : +theorem lintegral_prod_le [SFinite ν] (f : α × β → ℝ≥0∞) : ∫⁻ z, f z ∂μ.prod ν ≤ ∫⁻ x, ∫⁻ y, f (x, y) ∂ν ∂μ := by rw [Measure.prod] - exact (lintegral_bind_le _ _ _).trans <| lintegral_mono fun a ↦ lintegral_map_le _ _ + exact (lintegral_bind_le _ _ Measurable.map_prodMk_left.aemeasurable).trans <| + lintegral_mono fun a ↦ lintegral_map_le _ (by fun_prop) /-- **Tonelli's Theorem for set integrals**: For `ℝ≥0∞`-valued almost everywhere measurable functions on `s ×ˢ t`, the integral of `f` on `s ×ˢ t` is equal to the iterated integral on `s` @@ -1117,20 +1114,16 @@ lemma fst_prod [IsProbabilityMeasure ν] : (μ.prod ν).fst = μ := by rw [fst_apply hs, ← prod_univ, prod_prod, measure_univ, mul_one] theorem fst_map_prodMk₀ {X : α → β} {Y : α → γ} {μ : Measure α} - (hY : AEMeasurable Y μ) : (μ.map fun a => (X a, Y a)).fst = μ.map X := by - by_cases hX : AEMeasurable X μ - · ext1 s hs - rw [Measure.fst_apply hs, Measure.map_apply_of_aemeasurable (hX.prodMk hY) (measurable_fst hs), - Measure.map_apply_of_aemeasurable hX hs, ← prod_univ, mk_preimage_prod, preimage_univ, - inter_univ] - · have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by - contrapose hX - exact measurable_fst.comp_aemeasurable hX - simp [map_of_not_aemeasurable, hX, this] - -theorem fst_map_prodMk {X : α → β} {Y : α → γ} {μ : Measure α} + (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) : + (μ.map fun a => (X a, Y a)).fst = μ.map X := by + ext1 s hs + rw [Measure.fst_apply hs, Measure.map_apply_of_aemeasurable (hX.prodMk hY) (measurable_fst hs), + Measure.map_apply_of_aemeasurable hX hs, ← prod_univ, mk_preimage_prod, preimage_univ, + inter_univ] + +theorem fst_map_prodMk {X : α → β} {Y : α → γ} {μ : Measure α} (hX : Measurable X) (hY : Measurable Y) : (μ.map fun a => (X a, Y a)).fst = μ.map X := - fst_map_prodMk₀ hY.aemeasurable + fst_map_prodMk₀ hX.aemeasurable hY.aemeasurable @[simp] lemma fst_add {μ ν : Measure (α × β)} : (μ + ν).fst = μ.fst + ν.fst := @@ -1178,21 +1171,18 @@ lemma snd_prod [IsProbabilityMeasure μ] : (μ.prod ν).snd = ν := by ext1 s hs rw [snd_apply hs, ← univ_prod, prod_prod, measure_univ, one_mul] -theorem snd_map_prodMk₀ {X : α → β} {Y : α → γ} {μ : Measure α} (hX : AEMeasurable X μ) : +theorem snd_map_prodMk₀ {X : α → β} {Y : α → γ} {μ : Measure α} (hX : AEMeasurable X μ) + (hY : AEMeasurable Y μ) : (μ.map fun a => (X a, Y a)).snd = μ.map Y := by - by_cases hY : AEMeasurable Y μ - · ext1 s hs - rw [Measure.snd_apply hs, Measure.map_apply_of_aemeasurable (hX.prodMk hY) (measurable_snd hs), - Measure.map_apply_of_aemeasurable hY hs, ← univ_prod, mk_preimage_prod, preimage_univ, - univ_inter] - · have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by - contrapose hY - exact measurable_snd.comp_aemeasurable hY - simp [map_of_not_aemeasurable, hY, this] - -theorem snd_map_prodMk {X : α → β} {Y : α → γ} {μ : Measure α} (hX : Measurable X) : + ext1 s hs + rw [Measure.snd_apply hs, Measure.map_apply_of_aemeasurable (hX.prodMk hY) (measurable_snd hs), + Measure.map_apply_of_aemeasurable hY hs, ← univ_prod, mk_preimage_prod, preimage_univ, + univ_inter] + +theorem snd_map_prodMk {X : α → β} {Y : α → γ} {μ : Measure α} (hX : Measurable X) + (hY : Measurable Y) : (μ.map fun a => (X a, Y a)).snd = μ.map Y := - snd_map_prodMk₀ hX.aemeasurable + snd_map_prodMk₀ hX.aemeasurable hY.aemeasurable @[simp] lemma snd_add {μ ν : Measure (α × β)} : (μ + ν).snd = μ.snd + ν.snd := diff --git a/Mathlib/MeasureTheory/Measure/Prokhorov.lean b/Mathlib/MeasureTheory/Measure/Prokhorov.lean index c6712ca53eaf3d..1a83535342af0c 100644 --- a/Mathlib/MeasureTheory/Measure/Prokhorov.lean +++ b/Mathlib/MeasureTheory/Measure/Prokhorov.lean @@ -208,7 +208,7 @@ lemma isCompact_setOfPred_finiteMeasure_le_of_isCompact ofPred_subset_ofPred, F, T] intro μ hμ rw [Measure.map_apply hf.continuous.measurable hK.measurableSet.compl] - refine ⟨(mass_map_le _ _).trans hμ, by simp [f]⟩ + refine ⟨(mass_map_le hf.measurable.aemeasurable).trans hμ, by simp [f]⟩ rw [this] apply IsCompact.image _ (by fun_prop) have : CompactSpace K := isCompact_iff_compactSpace.mp hK diff --git a/Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean b/Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean index 24b59937a2b98d..bbec63562761e5 100644 --- a/Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean +++ b/Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean @@ -97,7 +97,7 @@ protected theorem congr (hf : QuasiMeasurePreserving f μa μb) {f' : α → β} theorem smul_measure {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (hf : QuasiMeasurePreserving f μa μb) (c : R) : QuasiMeasurePreserving f (c • μa) (c • μb) := - ⟨hf.1, by rw [Measure.map_smul]; exact hf.2.smul c⟩ + ⟨hf.1, by rw [Measure.map_smul _ hf.aemeasurable]; exact hf.2.smul c⟩ theorem ae_map_le (h : QuasiMeasurePreserving f μa μb) : ae (μa.map f) ≤ ae μb := h.2.ae_le diff --git a/Mathlib/MeasureTheory/Measure/Tight.lean b/Mathlib/MeasureTheory/Measure/Tight.lean index b108919a7e0635..896e7fa8d07191 100644 --- a/Mathlib/MeasureTheory/Measure/Tight.lean +++ b/Mathlib/MeasureTheory/Measure/Tight.lean @@ -126,17 +126,15 @@ protected lemma inter (hS : IsTightMeasureSet S) (T : Set (Measure 𝓧)) : IsTightMeasureSet (S ∩ T) := hS.subset inter_subset_left -lemma map [TopologicalSpace 𝓨] [MeasurableSpace 𝓨] [OpensMeasurableSpace 𝓨] [T2Space 𝓨] - (hS : IsTightMeasureSet S) {f : 𝓧 → 𝓨} (hf : Continuous f) : +lemma map [OpensMeasurableSpace 𝓧] [TopologicalSpace 𝓨] [MeasurableSpace 𝓨] + [BorelSpace 𝓨] [T2Space 𝓨] (hS : IsTightMeasureSet S) {f : 𝓧 → 𝓨} (hf : Continuous f) : IsTightMeasureSet (Measure.map f '' S) := by rw [isTightMeasureSet_iff_exists_isCompact_measure_compl_le] at hS ⊢ simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro ε hε obtain ⟨K, hK_compact, hKS⟩ := hS ε hε refine ⟨f '' K, hK_compact.image hf, fun μ hμS ↦ ?_⟩ - by_cases hf_meas : AEMeasurable f μ - swap; · simp [Measure.map_of_not_aemeasurable hf_meas] - rw [Measure.map_apply_of_aemeasurable hf_meas (hK_compact.image hf).measurableSet.compl] + rw [Measure.map_apply_of_aemeasurable hf.aemeasurable (hK_compact.image hf).measurableSet.compl] refine (measure_mono ?_).trans (hKS μ hμS) simp only [preimage_compl, compl_subset_compl] exact subset_preimage_image f K diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean b/Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean index 86e8176e35b8ce..9955fb3bc39b94 100644 --- a/Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean +++ b/Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean @@ -115,6 +115,11 @@ instance isFiniteMeasureSMulOfNNRealTower {R} [SMul R ℝ≥0] [SMul R ℝ≥0 theorem isFiniteMeasure_of_le (μ : Measure α) [IsFiniteMeasure μ] (h : ν ≤ μ) : IsFiniteMeasure ν := { measure_univ_lt_top := (h Set.univ).trans_lt (measure_lt_top _ _) } +/-- This is not an instance as it is superseded by the fact that is is a probability measure. -/ +theorem isFiniteMeasure_dirac {a : α} : IsFiniteMeasure (dirac a) where + measure_univ_lt_top := by + simp [dirac_apply_of_mem <| mem_univ a] + @[instance] theorem Measure.isFiniteMeasure_map {m : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (f : α → β) : IsFiniteMeasure (μ.map f) := by @@ -122,8 +127,10 @@ theorem Measure.isFiniteMeasure_map {m : MeasurableSpace α} (μ : Measure α) [ · constructor rw [map_apply_of_aemeasurable hf MeasurableSet.univ] exact measure_lt_top μ _ - · rw [map_of_not_aemeasurable hf] - exact MeasureTheory.isFiniteMeasureZero + · obtain rfl | hμ := eq_or_ne μ 0 + · rw [Measure.map_zero]; infer_instance + rw [map_of_not_aemeasurable_of_ne_zero hf hμ] + exact isFiniteMeasure_dirac theorem Measure.isFiniteMeasure_of_map {μ : Measure α} {f : α → β} (hf : AEMeasurable f μ) [IsFiniteMeasure (μ.map f)] : IsFiniteMeasure μ where diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean b/Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean index 0f2bb605bb7d90..854e28ccdb1cca 100644 --- a/Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean +++ b/Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean @@ -121,23 +121,27 @@ lemma isProbabilityMeasure_iff_real {μ : Measure α} : IsProbabilityMeasure μ ↔ μ.real univ = 1 := by refine ⟨fun h ↦ probReal_univ, fun h ↦ ⟨(ENNReal.toReal_eq_one_iff (μ univ)).mp h⟩⟩ -theorem Measure.isProbabilityMeasure_map {f : α → β} (hf : AEMeasurable f μ) : - IsProbabilityMeasure (map f μ) := - ⟨by simp [map_apply_of_aemeasurable, hf]⟩ - -theorem Measure.isProbabilityMeasure_of_map {μ : Measure α} (f : α → β) - [IsProbabilityMeasure (μ.map f)] : IsProbabilityMeasure μ where +instance {f : α → β} : IsProbabilityMeasure (map f μ) where + measure_univ := by + rw [Measure.map] + split_ifs with hf hμ + · simp [mapₗ_mk_apply_of_aemeasurable, hf] + · have := measure_univ (μ := μ) + simp [hμ] at this + · exact dirac_apply_of_mem <| mem_univ _ + +theorem Measure.isProbabilityMeasure_of_map {μ : Measure α} {f : α → β} + [IsProbabilityMeasure (μ.map f)] (hf : AEMeasurable f μ) : IsProbabilityMeasure μ where measure_univ := by - have hf : AEMeasurable f μ := AEMeasurable.of_map_ne_zero (IsProbabilityMeasure.ne_zero _) rw [← Set.preimage_univ (f := f), ← map_apply_of_aemeasurable hf .univ] exact IsProbabilityMeasure.measure_univ theorem Measure.isProbabilityMeasure_map_iff {μ : Measure α} {f : α → β} (hf : AEMeasurable f μ) : IsProbabilityMeasure (μ.map f) ↔ IsProbabilityMeasure μ := - ⟨fun _ ↦ isProbabilityMeasure_of_map f, fun _ ↦ isProbabilityMeasure_map hf⟩ + ⟨fun _ ↦ isProbabilityMeasure_of_map hf, fun _ ↦ inferInstance⟩ instance IsProbabilityMeasure_comap_equiv (f : β ≃ᵐ α) : IsProbabilityMeasure (μ.comap f) := by - rw [← MeasurableEquiv.map_symm]; exact isProbabilityMeasure_map f.symm.measurable.aemeasurable + rw [← MeasurableEquiv.map_symm]; infer_instance /-- Note that this is not quite as useful as it looks because the measure takes values in `ℝ≥0∞`. Thus the subtraction appearing is the truncated subtraction of `ℝ≥0∞`, rather than the @@ -184,9 +188,6 @@ protected lemma _root_.MeasurableEmbedding.isProbabilityMeasure_comap (hf : Meas (hf' : ∀ᵐ a ∂μ, a ∈ range f) : IsProbabilityMeasure (μ.comap f) := isProbabilityMeasure_comap hf.injective hf' hf.measurableSet_image' -instance isProbabilityMeasure_map_up : - IsProbabilityMeasure (μ.map ULift.up) := isProbabilityMeasure_map measurable_up.aemeasurable - instance isProbabilityMeasure_comap_down : IsProbabilityMeasure (μ.comap ULift.down) := MeasurableEquiv.ulift.measurableEmbedding.isProbabilityMeasure_comap <| ae_of_all _ <| by simp [Function.Surjective.range_eq <| EquivLike.surjective _] @@ -217,9 +218,10 @@ lemma eq_zero_or_isProbabilityMeasure : μ = 0 ∨ IsProbabilityMeasure μ := by · exact Or.inr ⟨h⟩ instance {f : α → β} : IsZeroOrProbabilityMeasure (map f μ) := by - by_cases hf : AEMeasurable f μ - · simpa [isZeroOrProbabilityMeasure_iff, hf] using IsZeroOrProbabilityMeasure.measure_univ - · simp [isZeroOrProbabilityMeasure_iff, hf] + obtain rfl | _ := eq_zero_or_isProbabilityMeasure (μ := μ) + · rw [Measure.map_zero] + infer_instance + · infer_instance lemma prob_compl_lt_one_sub_of_lt_prob {p : ℝ≥0∞} (hμs : p < μ s) (s_mble : MeasurableSet s) : μ sᶜ < 1 - p := by diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses/ZeroOne.lean b/Mathlib/MeasureTheory/Measure/Typeclasses/ZeroOne.lean index 29f89f695d3be7..0a58736d88e2be 100644 --- a/Mathlib/MeasureTheory/Measure/Typeclasses/ZeroOne.lean +++ b/Mathlib/MeasureTheory/Measure/Typeclasses/ZeroOne.lean @@ -7,7 +7,7 @@ Authors: Gaëtan Serré module public import Mathlib.MeasureTheory.Constructions.Polish.Basic -public import Mathlib.MeasureTheory.Measure.Dirac +public import Mathlib.MeasureTheory.Measure.Dirac.Basic /-! diff --git a/Mathlib/MeasureTheory/Measure/WithDensity.lean b/Mathlib/MeasureTheory/Measure/WithDensity.lean index 47474362ff31f7..32b3c567aa7704 100644 --- a/Mathlib/MeasureTheory/Measure/WithDensity.lean +++ b/Mathlib/MeasureTheory/Measure/WithDensity.lean @@ -761,10 +761,11 @@ variable {M : Type*} [Monoid M] [MeasurableSpace M] -- `mconv_smul_left` is in the `Convolution` file. This lemma is here because this is the file in -- which we prove the instance that gives `SFinite (c • ν)`. @[to_additive conv_smul_right] -theorem Measure.mconv_smul_right (μ : Measure M) (ν : Measure M) [SFinite ν] (s : ℝ≥0∞) : +theorem Measure.mconv_smul_right [MeasurableMul₂ M] (μ : Measure M) (ν : Measure M) [SFinite ν] + (s : ℝ≥0∞) : μ ∗ₘ (s • ν) = s • (μ ∗ₘ ν) := by unfold mconv - rw [Measure.prod_smul_right, Measure.map_smul] + rw [Measure.prod_smul_right, Measure.map_smul _ (by fun_prop)] variable {G : Type*} [Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : Measure G} [SFinite μ] [IsMulLeftInvariant μ] diff --git a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean index c8a2bf72636d62..84469ca904942a 100644 --- a/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean +++ b/Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean @@ -6,7 +6,7 @@ Authors: Oliver Butterley, Yoh Tanimoto module public import Mathlib.Analysis.Normed.Module.Basic -public import Mathlib.MeasureTheory.Measure.Dirac +public import Mathlib.MeasureTheory.Measure.Dirac.Basic public import Mathlib.MeasureTheory.VectorMeasure.Variation.Defs /-! diff --git a/Mathlib/Probability/CDF.lean b/Mathlib/Probability/CDF.lean index ec6345bbd532f6..8fc5a37bbc5331 100644 --- a/Mathlib/Probability/CDF.lean +++ b/Mathlib/Probability/CDF.lean @@ -105,7 +105,6 @@ lemma cdf_measure_stieltjesFunction (f : StieltjesFunction ℝ) (hf0 : Tendsto f open unitInterval in lemma unitInterval.cdf_eq_real (μ : Measure I) [IsProbabilityMeasure μ] (x : I) : cdf (μ.map Subtype.val) x.1 = μ.real (Icc 0 x) := by - have : IsProbabilityMeasure (μ.map Subtype.val) := isProbabilityMeasure_map (by fun_prop) rw [ProbabilityTheory.cdf_eq_real, map_measureReal_apply measurable_subtype_coe measurableSet_Iic, subtype_Iic_eq_Icc] diff --git a/Mathlib/Probability/Density.lean b/Mathlib/Probability/Density.lean index 3b8db490b50342..151d395115028d 100644 --- a/Mathlib/Probability/Density.lean +++ b/Mathlib/Probability/Density.lean @@ -121,28 +121,10 @@ def pdf {_ : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω) (μ : Measure theorem pdf_def {_ : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E} : pdf X ℙ μ = (map X ℙ).rnDeriv μ := rfl -theorem pdf_of_not_aemeasurable {_ : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} - {X : Ω → E} (hX : ¬AEMeasurable X ℙ) : pdf X ℙ μ =ᵐ[μ] 0 := by - rw [pdf_def, map_of_not_aemeasurable hX] - exact rnDeriv_zero μ - theorem pdf_of_not_haveLebesgueDecomposition {_ : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E} (h : ¬(map X ℙ).HaveLebesgueDecomposition μ) : pdf X ℙ μ = 0 := rnDeriv_of_not_haveLebesgueDecomposition h -theorem aemeasurable_of_pdf_ne_zero {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} - (X : Ω → E) (h : ¬pdf X ℙ μ =ᵐ[μ] 0) : AEMeasurable X ℙ := by - contrapose h - exact pdf_of_not_aemeasurable h - -theorem hasPDF_of_pdf_ne_zero {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E} - (hac : map X ℙ ≪ μ) (hpdf : ¬pdf X ℙ μ =ᵐ[μ] 0) : HasPDF X ℙ μ := by - refine ⟨?_, ?_, hac⟩ - · exact aemeasurable_of_pdf_ne_zero X hpdf - · contrapose hpdf - have := pdf_of_not_haveLebesgueDecomposition hpdf - filter_upwards using congrFun this - @[fun_prop] theorem measurable_pdf {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω) (μ : Measure E := by volume_tac) : Measurable (pdf X ℙ μ) := by diff --git a/Mathlib/Probability/Distributions/Bernoulli.lean b/Mathlib/Probability/Distributions/Bernoulli.lean index c95b618d8e5286..da930cfe8dbaae 100644 --- a/Mathlib/Probability/Distributions/Bernoulli.lean +++ b/Mathlib/Probability/Distributions/Bernoulli.lean @@ -155,11 +155,11 @@ theorem map_bernoulliMeasure [MeasurableSingletonClass X] [MeasurableSingletonCl have hf (x : X) : AEMeasurable f (dirac x) := by fun_prop simp only [bernoulliMeasure_def] rw [AEMeasurable.map_add₀ (by fun_prop) (by fun_prop)] - simp + simp [hf] theorem map_bernoulliMeasure' (x y : X) {f : X → Y} (hf : Measurable f) (p : I) : Ber(x, y, p).map f = bernoulliMeasure (f x) (f y) p := by - simp [bernoulliMeasure_def, Measure.map_add _ _ hf, Measure.map_smul, map_dirac' hf] + simp [bernoulliMeasure_def, Measure.map_add _ _ hf, hf.aemeasurable, map_dirac' hf] section Integral diff --git a/Mathlib/Probability/Distributions/Binomial.lean b/Mathlib/Probability/Distributions/Binomial.lean index a9877fadd09921..3165db10675ce3 100644 --- a/Mathlib/Probability/Distributions/Binomial.lean +++ b/Mathlib/Probability/Distributions/Binomial.lean @@ -71,11 +71,9 @@ lemma binomial_zero : Bin(0, p) = dirac 0 := by simp [binomial] lemma map_cast_binomial_zero : Bin(R, 0, p) = dirac 0 := by simp [binomial, map_dirac' .of_discrete] -instance isProbabilityMeasure_binomial : IsProbabilityMeasure Bin(n, p) := - isProbabilityMeasure_map <| by fun_prop - -instance isProbabilityMeasure_map_cast_binomial : IsProbabilityMeasure Bin(R, n, p) := - isProbabilityMeasure_map .of_discrete +instance isProbabilityMeasure_binomial : IsProbabilityMeasure Bin(n, p) := by + rw [binomial] + infer_instance lemma ae_le_of_hasLaw_binomial {X : Ω → ℕ} (hX : HasLaw X Bin(n, p) P) : ∀ᵐ ω ∂P, X ω ≤ n := by rw [hX.ae_iff (p := (· ≤ n)) <| by fun_prop, binomial, @@ -147,7 +145,7 @@ lemma map_cast_binomial_eq_sum_dirac [MeasurableSingletonClass R] (n : ℕ) (p : ∑ k ∈ Finset.Iic n, ENNReal.ofReal ((n.choose k) * p ^ k * (1 - p) ^ (n - k)) • dirac (k : R) := by rw [binomial_eq_sum_dirac, Measure.map_finset_sum .of_discrete] - exact Finset.sum_congr rfl fun _ _ ↦ by rw [Measure.map_smul, map_dirac] + exact Finset.sum_congr rfl fun _ _ ↦ by rw [Measure.map_smul _ (by fun_prop), map_dirac] section Integral diff --git a/Mathlib/Probability/Distributions/Fernique.lean b/Mathlib/Probability/Distributions/Fernique.lean index 67dfc7e72e9c1b..31a85780a3f310 100644 --- a/Mathlib/Probability/Distributions/Fernique.lean +++ b/Mathlib/Probability/Distributions/Fernique.lean @@ -607,7 +607,8 @@ theorem exists_integrable_exp_sq_of_map_rotation_eq_self [IsFiniteMeasure μ] calc (μ'.prod μ').map (ContinuousLinearMap.rotation (-(π / 4))) _ = ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹) • (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) := by - simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul] + simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul, + (ContinuousLinearMap.rotation (-(π / 4))).continuous.aemeasurable] _ = ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹) • (μ.prod μ) := by rw [h_rot] _ = μ'.prod μ' := by simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul] diff --git a/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Basic.lean b/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Basic.lean index 75eb15838b1d9c..219f109b0f4320 100644 --- a/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Basic.lean +++ b/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Basic.lean @@ -43,24 +43,22 @@ variable [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] [mE : MeasurableS lemma HasGaussianLaw.congr {Y : Ω → E} (hX : HasGaussianLaw X P) (h : X =ᵐ[P] Y) : HasGaussianLaw Y P where + aemeasurable := hX.aemeasurable.congr h isGaussian_map := by rw [← Measure.map_congr h] exact hX.isGaussian_map -lemma IsGaussian.hasGaussianLaw [IsGaussian (P.map X)] : HasGaussianLaw X P where +lemma IsGaussian.hasGaussianLaw [IsGaussian (P.map X)] (hX : AEMeasurable X P) : + HasGaussianLaw X P where isGaussian_map := inferInstance variable {mE} in lemma IsGaussian.hasGaussianLaw_id {μ : Measure E} [IsGaussian μ] : HasGaussianLaw id μ where isGaussian_map := by rwa [Measure.map_id] -@[fun_prop] -lemma HasGaussianLaw.aemeasurable (hX : HasGaussianLaw X P) : AEMeasurable X P := - AEMeasurable.of_map_ne_zero hX.isGaussian_map.toIsProbabilityMeasure.ne_zero - lemma HasGaussianLaw.isProbabilityMeasure (hX : HasGaussianLaw X P) : IsProbabilityMeasure P := haveI := hX.isGaussian_map - P.isProbabilityMeasure_of_map X + P.isProbabilityMeasure_of_map hX.aemeasurable variable {mE} in lemma HasLaw.hasGaussianLaw {μ : Measure E} (hX : HasLaw X μ P) [IsGaussian μ] : @@ -91,9 +89,7 @@ variable [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] {X : Ω → E lemma of_subsingleton [NormedSpace ℝ E] [Subsingleton E] [IsProbabilityMeasure P] : HasGaussianLaw X P where - isGaussian_map := by - have : IsProbabilityMeasure (P.map X) := P.isProbabilityMeasure_map (by fun_prop) - exact .of_subsingleton + isGaussian_map := .of_subsingleton lemma charFun_map_eq [InnerProductSpace ℝ E] (t : E) (hX : HasGaussianLaw X P) : charFun (P.map X) t = exp ((P[fun ω ↦ ⟪t, X ω⟫] : ℝ) * I - Var[fun ω ↦ ⟪t, X ω⟫; P] / 2) := by @@ -106,7 +102,7 @@ lemma _root_.ProbabilityTheory.hasGaussianLaw_iff_charFun_map_eq [CompleteSpace charFun (P.map X) t = exp ((P[fun ω ↦ ⟪t, X ω⟫] : ℝ) * I - Var[fun ω ↦ ⟪t, X ω⟫; P] / 2) where mp h := h.charFun_map_eq mpr h := by - refine ⟨isGaussian_iff_charFun_eq.2 fun t ↦ ?_⟩ + refine ⟨hX, isGaussian_iff_charFun_eq.2 fun t ↦ ?_⟩ rw [h, integral_map, variance_map, integral_complex_ofReal, Function.comp_def] all_goals fun_prop @@ -123,7 +119,7 @@ lemma _root_.ProbabilityTheory.hasGaussianLaw_iff_charFunDual_map_eq charFunDual (P.map X) L = exp ((P[L ∘ X] : ℝ) * I - Var[L ∘ X; P] / 2) where mp h := h.charFunDual_map_eq mpr h := by - refine ⟨isGaussian_iff_charFunDual_eq.2 fun t ↦ ?_⟩ + refine ⟨hX, isGaussian_iff_charFunDual_eq.2 fun t ↦ ?_⟩ rw [h, integral_map, variance_map, integral_complex_ofReal, Function.comp_def] all_goals fun_prop diff --git a/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Def.lean b/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Def.lean index e5e8b01ab83684..ccc3be8253afb7 100644 --- a/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Def.lean +++ b/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Def.lean @@ -30,4 +30,7 @@ open MeasureTheory public structure ProbabilityTheory.HasGaussianLaw {Ω E : Type*} {mΩ : MeasurableSpace Ω} [TopologicalSpace E] [AddCommMonoid E] [Module ℝ E] [mE : MeasurableSpace E] (X : Ω → E) (P : Measure Ω) : Prop where + protected aemeasurable : AEMeasurable X P := by fun_prop protected isGaussian_map : IsGaussian (P.map X) + +attribute [fun_prop] ProbabilityTheory.HasGaussianLaw.aemeasurable diff --git a/Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Basic.lean b/Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Basic.lean index ee222f187c7006..c28af64482899b 100644 --- a/Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Basic.lean +++ b/Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Basic.lean @@ -48,8 +48,7 @@ lemma isProbabilityMeasure (hX : IsGaussianProcess X P) : hX.hasGaussianLaw Classical.ofNonempty |>.isProbabilityMeasure lemma aemeasurable (hX : IsGaussianProcess X P) (t : T) : AEMeasurable (X t) P := - AEMeasurable.of_map_ne_zero - (hX.hasGaussianLaw {t}).isGaussian_map.toIsProbabilityMeasure.ne_zero |>.eval ⟨t, by simp⟩ + (hX.hasGaussianLaw {t}).aemeasurable.eval ⟨t, by simp⟩ /-- A modification of a Gaussian process is a Gaussian process. -/ lemma congr (hX : IsGaussianProcess X P) (hXY : ∀ t, X t =ᵐ[P] Y t) : diff --git a/Mathlib/Probability/Distributions/Gaussian/Multivariate.lean b/Mathlib/Probability/Distributions/Gaussian/Multivariate.lean index 33af3d8ef94287..6953dbcb994d33 100644 --- a/Mathlib/Probability/Distributions/Gaussian/Multivariate.lean +++ b/Mathlib/Probability/Distributions/Gaussian/Multivariate.lean @@ -68,8 +68,9 @@ def stdGaussian : Measure E := variable [BorelSpace E] -instance isProbabilityMeasure_stdGaussian : IsProbabilityMeasure (stdGaussian E) := - Measure.isProbabilityMeasure_map (Measurable.aemeasurable (by fun_prop)) +instance isProbabilityMeasure_stdGaussian : IsProbabilityMeasure (stdGaussian E) := by + rw [stdGaussian] + infer_instance @[simp] lemma integral_id_stdGaussian : ∫ x, x ∂(stdGaussian E) = 0 := by diff --git a/Mathlib/Probability/Distributions/Gaussian/Real.lean b/Mathlib/Probability/Distributions/Gaussian/Real.lean index ce408ccaa93df3..2c0b1fd72f5d80 100644 --- a/Mathlib/Probability/Distributions/Gaussian/Real.lean +++ b/Mathlib/Probability/Distributions/Gaussian/Real.lean @@ -474,10 +474,9 @@ theorem complexMGF_id_gaussianReal (z : ℂ) : /-- The complex moment-generating function of a random variable with Gaussian distribution with mean `μ` and variance `v` is given by `z ↦ exp (z * μ + v * z ^ 2 / 2)`. -/ -theorem complexMGF_gaussianReal (hX : p.map X = gaussianReal μ v) (z : ℂ) : +theorem complexMGF_gaussianReal (hX : HasLaw X (gaussianReal μ v) p) (z : ℂ) : complexMGF X p z = cexp (z * μ + v * z ^ 2 / 2) := by - have hX_meas : AEMeasurable X p := aemeasurable_of_map_neZero (by rw [hX]; infer_instance) - rw [← complexMGF_id_map hX_meas, hX, complexMGF_id_gaussianReal] + rw [← complexMGF_id_map hX.aemeasurable, hX.map_eq, complexMGF_id_gaussianReal] /-- The characteristic function of a Gaussian distribution with mean `μ` and variance `v` is given by `t ↦ exp (t * μ - v * t ^ 2 / 2)`. -/ @@ -490,11 +489,11 @@ theorem charFun_gaussianReal (t : ℝ) : /-- The moment-generating function of a random variable with Gaussian distribution with mean `μ` and variance `v` is given by `t ↦ exp (μ * t + v * t ^ 2 / 2)`. -/ -theorem mgf_gaussianReal (hX : p.map X = gaussianReal μ v) (t : ℝ) : +theorem mgf_gaussianReal (hX : HasLaw X (gaussianReal μ v) p) (t : ℝ) : mgf X p t = rexp (μ * t + v * t ^ 2 / 2) := by suffices (mgf X p t : ℂ) = rexp (μ * t + ↑v * t ^ 2 / 2) from mod_cast this - have hX_meas : AEMeasurable X p := aemeasurable_of_map_neZero (by rw [hX]; infer_instance) - rw [← mgf_id_map hX_meas, ← complexMGF_ofReal, hX, complexMGF_id_gaussianReal, mul_comm μ] + rw [← mgf_id_map hX.aemeasurable, ← complexMGF_ofReal, hX.map_eq, complexMGF_id_gaussianReal, + mul_comm μ] norm_cast theorem mgf_fun_id_gaussianReal : @@ -508,7 +507,7 @@ theorem mgf_id_gaussianReal : mgf id (gaussianReal μ v) = fun t ↦ rexp (μ * /-- The cumulant-generating function of a random variable with Gaussian distribution with mean `μ` and variance `v` is given by `t ↦ μ * t + v * t ^ 2 / 2`. -/ -theorem cgf_gaussianReal (hX : p.map X = gaussianReal μ v) (t : ℝ) : +theorem cgf_gaussianReal (hX : HasLaw X (gaussianReal μ v) p) (t : ℝ) : cgf X p t = μ * t + v * t ^ 2 / 2 := by rw [cgf, mgf_gaussianReal hX t, Real.log_exp] @@ -653,13 +652,12 @@ lemma gaussianReal_conv_gaussianReal {m₁ m₂ : ℝ} {v₁ v₂ : ℝ≥0} : Gaussian distribution with mean `m₁ + m₂` and variance `v_1 + v_2`. -/ lemma gaussianReal_add_gaussianReal_of_indepFun {Ω} {mΩ : MeasurableSpace Ω} {P : Measure Ω} {m₁ m₂ : ℝ} {v₁ v₂ : ℝ≥0} {X Y : Ω → ℝ} (hXY : IndepFun X Y P) - (hX : P.map X = gaussianReal m₁ v₁) (hY : P.map Y = gaussianReal m₂ v₂) : + (hX : HasLaw X (gaussianReal m₁ v₁) P) (hY : HasLaw Y (gaussianReal m₂ v₂) P) : P.map (X + Y) = gaussianReal (m₁ + m₂) (v₁ + v₂) := by - rw [hXY.map_add_eq_map_conv_map₀', hX, hY, gaussianReal_conv_gaussianReal] - · apply AEMeasurable.of_map_ne_zero; simp [NeZero.ne, hX] - · apply AEMeasurable.of_map_ne_zero; simp [NeZero.ne, hY] - · rw [hX]; apply IsFiniteMeasure.toSigmaFinite - · rw [hY]; apply IsFiniteMeasure.toSigmaFinite + rw [hXY.map_add_eq_map_conv_map₀' hX.aemeasurable hY.aemeasurable, hX.map_eq, hY.map_eq, + gaussianReal_conv_gaussianReal] + · rw [hX.map_eq]; apply IsFiniteMeasure.toSigmaFinite + · rw [hY.map_eq]; apply IsFiniteMeasure.toSigmaFinite end GaussianReal diff --git a/Mathlib/Probability/Distributions/Poisson/Basic.lean b/Mathlib/Probability/Distributions/Poisson/Basic.lean index 9b92070095b9a6..c0c85e101a7ed8 100644 --- a/Mathlib/Probability/Distributions/Poisson/Basic.lean +++ b/Mathlib/Probability/Distributions/Poisson/Basic.lean @@ -68,10 +68,6 @@ lemma hasSum_one_poissonMeasure (r : ℝ≥0) : HasSum (fun n ↦ exp (-r) * r ^ instance (r : ℝ≥0) : IsProbabilityMeasure Po(r) := (hasSum_one_poissonMeasure r).isProbabilityMeasure_sum_dirac (fun _ ↦ by positivity) -instance (r : ℝ≥0) {R : Type*} [NatCast R] [MeasurableSpace R] : - IsProbabilityMeasure Po(R, r) := - Measure.isProbabilityMeasure_map .of_discrete - section Integral variable {E : Type*} [NormedAddCommGroup E] diff --git a/Mathlib/Probability/Distributions/Uniform.lean b/Mathlib/Probability/Distributions/Uniform.lean index 2f89b41d3a5078..2a0b2c81c73c35 100644 --- a/Mathlib/Probability/Distributions/Uniform.lean +++ b/Mathlib/Probability/Distributions/Uniform.lean @@ -5,8 +5,8 @@ Authors: Josha Dekker, Devon Tuma, Kexing Ying -/ module -public import Mathlib.Probability.Density public import Mathlib.Probability.ConditionalProbability +public import Mathlib.Probability.HasLaw public import Mathlib.Probability.ProbabilityMassFunction.Constructions /-! @@ -19,7 +19,7 @@ This file defines two related notions of uniform distributions, which will be un Defines the uniform distribution for any set with finite measure. ### Main definitions -* `IsUniform X s ℙ μ` : A random variable `X` has uniform distribution on `s` under `ℙ` if the +* `IsUniform X s P μ` : A random variable `X` has uniform distribution on `s` under `P` if the push-forward measure agrees with the rescaled restricted measure `μ`. ## Uniform probability mass functions @@ -46,7 +46,7 @@ This file defines a number of uniform `PMF` distributions from various inputs, open scoped Finset MeasureTheory NNReal ENNReal -- TODO: We can't `open ProbabilityTheory` without opening the `ProbabilityTheory` scope :( -open TopologicalSpace MeasureTheory.Measure PMF +open TopologicalSpace MeasureTheory.Measure PMF ProbabilityTheory noncomputable section @@ -57,103 +57,99 @@ variable {E : Type*} [MeasurableSpace E] {μ : Measure E} namespace pdf variable {Ω : Type*} -variable {_ : MeasurableSpace Ω} {ℙ : Measure Ω} +variable {_ : MeasurableSpace Ω} {P : Measure Ω} /-- A random variable `X` has uniform distribution on `s` if its push-forward measure is `(μ s)⁻¹ • μ.restrict s`. -/ -def IsUniform (X : Ω → E) (s : Set E) (ℙ : Measure Ω) (μ : Measure E := by volume_tac) := - map X ℙ = ProbabilityTheory.cond μ s +def IsUniform (X : Ω → E) (s : Set E) (P : Measure Ω) (μ : Measure E := by volume_tac) := + HasLaw X μ[|s] P namespace IsUniform -theorem aemeasurable {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞) - (hu : IsUniform X s ℙ μ) : AEMeasurable X ℙ := by - dsimp [IsUniform, ProbabilityTheory.cond] at hu - by_contra h - rw [map_of_not_aemeasurable h] at hu - apply zero_ne_one' ℝ≥0∞ - calc - 0 = (0 : Measure E) Set.univ := rfl - _ = _ := by rw [hu, Measure.smul_apply, restrict_apply MeasurableSet.univ, - Set.univ_inter, smul_eq_mul, ENNReal.inv_mul_cancel hns hnt] +theorem aemeasurable {X : Ω → E} {s : Set E} (hu : IsUniform X s P μ) : AEMeasurable X P := + ProbabilityTheory.HasLaw.aemeasurable hu + +theorem map_eq {X : Ω → E} {s : Set E} (hu : IsUniform X s P μ) : + P.map X = ProbabilityTheory.cond μ s := HasLaw.map_eq hu -theorem absolutelyContinuous {X : Ω → E} {s : Set E} (hu : IsUniform X s ℙ μ) : map X ℙ ≪ μ := by - rw [hu]; exact ProbabilityTheory.cond_absolutelyContinuous +theorem absolutelyContinuous {X : Ω → E} {s : Set E} (hu : IsUniform X s P μ) : map X P ≪ μ := by + rw [hu.map_eq]; exact ProbabilityTheory.cond_absolutelyContinuous -theorem measure_preimage {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞) - (hu : IsUniform X s ℙ μ) {A : Set E} (hA : MeasurableSet A) : - ℙ (X ⁻¹' A) = μ (s ∩ A) / μ s := by - rwa [← map_apply_of_aemeasurable (hu.aemeasurable hns hnt) hA, hu, ProbabilityTheory.cond_apply', +theorem measure_preimage {X : Ω → E} {s : Set E} (hu : IsUniform X s P μ) {A : Set E} + (hA : MeasurableSet A) : + P (X ⁻¹' A) = μ (s ∩ A) / μ s := by + rwa [← map_apply_of_aemeasurable hu.aemeasurable hA, hu.map_eq, ProbabilityTheory.cond_apply', ENNReal.div_eq_inv_mul] theorem isProbabilityMeasure {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞) - (hu : IsUniform X s ℙ μ) : IsProbabilityMeasure ℙ := + (hu : IsUniform X s P μ) : IsProbabilityMeasure P := ⟨by have : X ⁻¹' Set.univ = Set.univ := Set.preimage_univ - rw [← this, hu.measure_preimage hns hnt MeasurableSet.univ, Set.inter_univ, + rw [← this, hu.measure_preimage MeasurableSet.univ, Set.inter_univ, ENNReal.div_self hns hnt]⟩ theorem toMeasurable_iff {X : Ω → E} {s : Set E} : - IsUniform X (toMeasurable μ s) ℙ μ ↔ IsUniform X s ℙ μ := by + IsUniform X (toMeasurable μ s) P μ ↔ IsUniform X s P μ := by unfold IsUniform rw [ProbabilityTheory.cond_toMeasurable_eq] -protected theorem toMeasurable {X : Ω → E} {s : Set E} (hu : IsUniform X s ℙ μ) : - IsUniform X (toMeasurable μ s) ℙ μ := +protected theorem toMeasurable {X : Ω → E} {s : Set E} (hu : IsUniform X s P μ) : + IsUniform X (toMeasurable μ s) P μ := toMeasurable_iff.mpr hu -theorem hasPDF {X : Ω → E} {s : Set E} (hns : μ s ≠ 0) (hnt : μ s ≠ ∞) - (hu : IsUniform X s ℙ μ) : HasPDF X ℙ μ := by +theorem hasPDF {X : Ω → E} {s : Set E} (hnt : μ s ≠ ∞) (hu : IsUniform X s P μ) : + HasPDF X P μ := by let t := toMeasurable μ s - apply hasPDF_of_map_eq_withDensity (hu.aemeasurable hns hnt) (t.indicator ((μ t)⁻¹ • 1)) <| + apply hasPDF_of_map_eq_withDensity hu.aemeasurable (t.indicator ((μ t)⁻¹ • 1)) <| (measurable_one.aemeasurable.const_smul (μ t)⁻¹).indicator (measurableSet_toMeasurable μ s) - rw [hu, withDensity_indicator (measurableSet_toMeasurable μ s), withDensity_smul _ measurable_one, - withDensity_one, restrict_toMeasurable hnt, measure_toMeasurable, ProbabilityTheory.cond] + rw [hu.map_eq, withDensity_indicator (measurableSet_toMeasurable μ s), + withDensity_smul _ measurable_one, withDensity_one, restrict_toMeasurable hnt, + measure_toMeasurable, ProbabilityTheory.cond] theorem pdf_eq_zero_of_measure_eq_zero_or_top {X : Ω → E} {s : Set E} - (hu : IsUniform X s ℙ μ) (hμs : μ s = 0 ∨ μ s = ∞) : pdf X ℙ μ =ᵐ[μ] 0 := by + (hu : IsUniform X s P μ) (hμs : μ s = 0 ∨ μ s = ∞) : pdf X P μ =ᵐ[μ] 0 := by rcases hμs with H | H · simp only [IsUniform, ProbabilityTheory.cond, H, ENNReal.inv_zero, restrict_eq_zero.mpr H, smul_zero] at hu - simp [pdf, hu] + simp [pdf, hu.map_eq] · simp only [IsUniform, ProbabilityTheory.cond, H, ENNReal.inv_top, zero_smul] at hu - simp [pdf, hu] + simp [pdf, hu.map_eq] theorem pdf_eq {X : Ω → E} {s : Set E} (hms : MeasurableSet s) - (hu : IsUniform X s ℙ μ) : pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • (1 : E → ℝ≥0∞)) := by + (hu : IsUniform X s P μ) : pdf X P μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • (1 : E → ℝ≥0∞)) := by by_cases hnt : μ s = ∞ · simp [pdf_eq_zero_of_measure_eq_zero_or_top hu (Or.inr hnt), hnt] by_cases hns : μ s = 0 · filter_upwards [measure_eq_zero_iff_ae_notMem.mp hns, pdf_eq_zero_of_measure_eq_zero_or_top hu (Or.inl hns)] with x hx h'x simp [hx, h'x, hns] - have : HasPDF X ℙ μ := hasPDF hns hnt hu - have : IsProbabilityMeasure ℙ := isProbabilityMeasure hns hnt hu + have : HasPDF X P μ := hasPDF hnt hu + have : IsProbabilityMeasure P := isProbabilityMeasure hns hnt hu apply (eq_of_map_eq_withDensity _ _).mp - · rw [hu, withDensity_indicator hms, withDensity_smul _ measurable_one, withDensity_one, + · rw [hu.map_eq, withDensity_indicator hms, withDensity_smul _ measurable_one, withDensity_one, ProbabilityTheory.cond] · exact (measurable_one.aemeasurable.const_smul (μ s)⁻¹).indicator hms theorem pdf_toReal_ae_eq {X : Ω → E} {s : Set E} (hms : MeasurableSet s) - (hX : IsUniform X s ℙ μ) : - (fun x => (pdf X ℙ μ x).toReal) =ᵐ[μ] fun x => + (hX : IsUniform X s P μ) : + (fun x => (pdf X P μ x).toReal) =ᵐ[μ] fun x => (s.indicator ((μ s)⁻¹ • (1 : E → ℝ≥0∞)) x).toReal := Filter.EventuallyEq.fun_comp (pdf_eq hms hX) ENNReal.toReal variable {X : Ω → ℝ} {s : Set ℝ} -theorem mul_pdf_integrable (hcs : IsCompact s) (huX : IsUniform X s ℙ) : - Integrable fun x : ℝ => x * (pdf X ℙ volume x).toReal := by +theorem mul_pdf_integrable (hcs : IsCompact s) (huX : IsUniform X s P) : + Integrable fun x : ℝ => x * (pdf X P volume x).toReal := by by_cases hnt : volume s = 0 ∨ volume s = ∞ · have I : Integrable (fun x ↦ x * ENNReal.toReal (0)) := by simp apply I.congr filter_upwards [pdf_eq_zero_of_measure_eq_zero_or_top huX hnt] with x hx simp [hx] simp only [not_or] at hnt - have : IsProbabilityMeasure ℙ := isProbabilityMeasure hnt.1 hnt.2 huX + have : IsProbabilityMeasure P := isProbabilityMeasure hnt.1 hnt.2 huX constructor · exact aestronglyMeasurable_id.mul - (measurable_pdf X ℙ).aemeasurable.ennreal_toReal.aestronglyMeasurable + (measurable_pdf X P).aemeasurable.ennreal_toReal.aestronglyMeasurable refine hasFiniteIntegral_mul (pdf_eq hcs.measurableSet huX) ?_ set ind := (volume s)⁻¹ • (1 : ℝ → ℝ≥0∞) have : ∀ x, ‖x‖ₑ * s.indicator ind x = s.indicator (fun x => ‖x‖ₑ * ind x) x := fun x => @@ -166,15 +162,12 @@ theorem mul_pdf_integrable (hcs : IsCompact s) (huX : IsUniform X s ℙ) : /-- A real uniform random variable `X` with support `s` has expectation `(λ s)⁻¹ * ∫ x in s, x ∂λ` where `λ` is the Lebesgue measure. -/ -theorem integral_eq (huX : IsUniform X s ℙ) : - ∫ x, X x ∂ℙ = (volume s)⁻¹.toReal * ∫ x in s, x := by +theorem integral_eq (huX : IsUniform X s P) : + ∫ x, X x ∂P = (volume s)⁻¹.toReal * ∫ x in s, x := by rw [← smul_eq_mul, ← integral_smul_measure] dsimp only [IsUniform, ProbabilityTheory.cond] at huX - rw [← huX] - by_cases hX : AEMeasurable X ℙ - · exact (integral_map hX aestronglyMeasurable_id).symm - · rw [map_of_not_aemeasurable hX, integral_zero_measure, integral_non_aestronglyMeasurable] - rwa [aestronglyMeasurable_iff_aemeasurable] + rw [← huX.map_eq] + exact (integral_map huX.aemeasurable aestronglyMeasurable_id).symm end IsUniform @@ -182,7 +175,7 @@ variable {X : Ω → E} lemma IsUniform.cond {s : Set E} : IsUniform (id : E → E) s (ProbabilityTheory.cond μ s) μ := - map_id + .id /-- The density of the uniform measure on a set with respect to itself. This allows us to abstract away the choice of random variable and probability space. -/ @@ -190,8 +183,8 @@ def uniformPDF (s : Set E) (x : E) (μ : Measure E := by volume_tac) : ℝ≥0 s.indicator ((μ s)⁻¹ • (1 : E → ℝ≥0∞)) x /-- Check that indeed any uniform random variable has the uniformPDF. -/ -lemma uniformPDF_eq_pdf {s : Set E} (hs : MeasurableSet s) (hu : pdf.IsUniform X s ℙ μ) : - (fun x ↦ uniformPDF s x μ) =ᵐ[μ] pdf X ℙ μ := +lemma uniformPDF_eq_pdf {s : Set E} (hs : MeasurableSet s) (hu : pdf.IsUniform X s P μ) : + (fun x ↦ uniformPDF s x μ) =ᵐ[μ] pdf X P μ := (hu.pdf_eq hs).symm.trans (ae_eq_refl _) open scoped Classical in diff --git a/Mathlib/Probability/HasCondDistrib.lean b/Mathlib/Probability/HasCondDistrib.lean index 68b6d95b1793bb..ff80fb950ba1be 100644 --- a/Mathlib/Probability/HasCondDistrib.lean +++ b/Mathlib/Probability/HasCondDistrib.lean @@ -60,7 +60,7 @@ lemma HasCondDistrib.hasLaw_of_const [IsProbabilityMeasure P] {Q : Measure 𝓨} have h_snd : (P.map (fun ω ↦ (X ω, Y ω))).snd = Q := by rw [h.map_eq, Measure.snd_compProd] simp [Measure.map_apply_of_aemeasurable h.aemeasurable_fst] - rwa [Measure.snd_map_prodMk₀ h.aemeasurable_fst] at h_snd + rwa [Measure.snd_map_prodMk₀ h.aemeasurable_fst (by fun_prop)] at h_snd variable [SFinite P] [IsSFiniteKernel κ] diff --git a/Mathlib/Probability/HasLaw.lean b/Mathlib/Probability/HasLaw.lean index abc9e450f070bf..05caf188bf9926 100644 --- a/Mathlib/Probability/HasLaw.lean +++ b/Mathlib/Probability/HasLaw.lean @@ -83,6 +83,7 @@ lemma HasLaw.measurePreserving (h₁ : HasLaw X μ P) (h₂ : Measurable X) : measurable := h₂ map_eq := h₁.map_eq +@[to_fun (attr := simp)] protected lemma HasLaw.id : HasLaw id μ μ where map_eq := map_id diff --git a/Mathlib/Probability/Independence/Basic.lean b/Mathlib/Probability/Independence/Basic.lean index d28b9586f87796..a7860613371e64 100644 --- a/Mathlib/Probability/Independence/Basic.lean +++ b/Mathlib/Probability/Independence/Basic.lean @@ -878,8 +878,7 @@ theorem iIndepFun_iff_map_fun_eq_pi_map [Fintype ι] {β : ι → Type*} specialize h₀ (s := fun i ↦ if i ∈ S then s i else univ) fun i ↦ by split_ifs with hiS <;> simp [hiS, hs] simp only [apply_ite, preimage_univ, measure_univ, Finset.prod_ite_mem, Finset.univ_inter, - Finset.prod_ite, Finset.filter_univ_mem, iInter_ite, iInter_univ, inter_univ, h, - Measure.pi_pi] at h₀ + iInter_ite, iInter_univ, inter_univ, h, Measure.pi_pi] at h₀ rw [h₀.2, ← h₀.1] variable {ι : Type*} [Fintype ι] {Ω : ι → Type*} {mΩ : ∀ i, MeasurableSpace (Ω i)} diff --git a/Mathlib/Probability/Independence/Conditional.lean b/Mathlib/Probability/Independence/Conditional.lean index cad164fc93016f..a148c34fac1e3b 100644 --- a/Mathlib/Probability/Independence/Conditional.lean +++ b/Mathlib/Probability/Independence/Conditional.lean @@ -868,7 +868,7 @@ theorem condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight g ⟂ᵢ[k, hk; μ] f ↔ condDistrib f (fun ω ↦ (k ω, g ω)) μ =ᵐ[μ.map (fun ω ↦ (k ω, g ω))] (condDistrib f k μ).prodMkRight _ := by - rw [condDistrib_ae_eq_iff_measure_eq_compProd (μ := μ) _ hf.aemeasurable, + rw [condDistrib_ae_eq_iff_measure_eq_compProd (μ := μ) (by fun_prop) hf.aemeasurable, condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib hg hf hk, Measure.compProd_eq_comp_prod] let e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm @@ -883,7 +883,7 @@ theorem condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight rw [← Kernel.id] at h simpa using h.symm _ = (Kernel.id ×ₖ (condDistrib f k μ).prodMkRight _) ∘ₘ μ.map (fun a ↦ (k a, g a)) := by - rw [compProd_map_condDistrib hg.aemeasurable] + rw [compProd_map_condDistrib hk.aemeasurable hg.aemeasurable] rw [← h_eq] have h1 : μ.map (fun x ↦ ((k x, g x), f x)) = (μ.map (fun a ↦ (k a, g a, f a))).map e := by rw [Measure.map_map (by fun_prop) (by fun_prop)] diff --git a/Mathlib/Probability/Independence/InfinitePi.lean b/Mathlib/Probability/Independence/InfinitePi.lean index ee31542de0090e..e49b470ea7f4c2 100644 --- a/Mathlib/Probability/Independence/InfinitePi.lean +++ b/Mathlib/Probability/Independence/InfinitePi.lean @@ -44,7 +44,6 @@ lemma iIndepFun.map_fun_eq_infinitePi_map₀ (mX : AEMeasurable (fun ω i ↦ X (h : iIndepFun X P) : P.map (fun ω i ↦ X i ω) = infinitePi (fun i ↦ P.map (X i)) := by have := h.isProbabilityMeasure - have _ i := isProbabilityMeasure_map (mX.eval i) refine eq_infinitePi _ fun s t ht ↦ ?_ rw [iIndepFun_iff_finset] at h have : (s : Set ι).pi t = s.restrict ⁻¹' (Set.univ.pi fun i ↦ t i) := by ext; simp @@ -67,7 +66,6 @@ lemma iIndepFun_iff_map_fun_eq_infinitePi_map₀ [IsProbabilityMeasure P] iIndepFun X P ↔ P.map (fun ω i ↦ X i ω) = infinitePi (fun i ↦ P.map (X i)) where mp h := h.map_fun_eq_infinitePi_map₀ mX mpr h := by - have _ i := isProbabilityMeasure_map (mX.eval i) rw [iIndepFun_iff_finset] intro s rw [iIndepFun_iff_map_fun_eq_pi_map] @@ -165,10 +163,6 @@ lemma iIndepFun_uncurry {X : (i : ι) → (j : κ i) → Ω → 𝓧 i j} (mX : (h1 : iIndepFun (fun i ω ↦ (X i · ω)) P) (h2 : ∀ i, iIndepFun (X i) P) : iIndepFun (fun (p : (i : ι) × (κ i)) ω ↦ X p.1 p.2 ω) P := by have := h1.isProbabilityMeasure - have : ∀ i j, IsProbabilityMeasure (P.map (X i j)) := - fun i j ↦ isProbabilityMeasure_map (mX i j).aemeasurable - have : ∀ i, IsProbabilityMeasure (P.map (fun ω ↦ (X i · ω))) := - fun i ↦ isProbabilityMeasure_map (Measurable.aemeasurable (by fun_prop)) have : (MeasurableEquiv.piCurry 𝓧) ∘ (fun ω p ↦ X p.1 p.2 ω) = fun ω i j ↦ X i j ω := by ext; simp [Sigma.curry] rw [iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop), @@ -196,19 +190,16 @@ lemma iIndepFun_uncurry_infinitePi {Ω : (i : ι) → κ i → Type*} {mΩ : ∀ (infinitePi fun i ↦ infinitePi (μ i)) = _ rw [← map_map (by fun_prop) (by fun_prop), infinitePi_map_pi (X := fun i ↦ (j : κ i) → Ω i j) (μ := fun i ↦ infinitePi (μ i)) - (f := fun i f j ↦ X i j (f j)), @infinitePi_map_eval .., infinitePi_map_pi] + (f := fun i f j ↦ X i j (f j)), infinitePi_map_eval, infinitePi_map_pi] · congrm infinitePi fun j ↦ ?_ change _ = map (((fun f ↦ f j) ∘ (fun f ↦ f i)) ∘ (fun ω i j ↦ X i j (ω i j))) (infinitePi fun i ↦ infinitePi (μ i)) rw [← map_map (by fun_prop) (by fun_prop), infinitePi_map_pi (X := fun i ↦ (j : κ i) → Ω i j) (μ := fun i ↦ infinitePi (μ i)) (f := fun i f j ↦ X i j (f j)), ← map_map (by fun_prop) (by fun_prop), - @infinitePi_map_eval .., infinitePi_map_pi, @infinitePi_map_eval ..] - any_goals fun_prop - · exact fun _ ↦ isProbabilityMeasure_map (by fun_prop) - · exact fun _ ↦ isProbabilityMeasure_map (Measurable.aemeasurable (by fun_prop)) - any_goals fun_prop - exact fun _ ↦ isProbabilityMeasure_map (Measurable.aemeasurable (by fun_prop)) + infinitePi_map_eval, infinitePi_map_pi, infinitePi_map_eval] + all_goals fun_prop + all_goals fun_prop end dependent diff --git a/Mathlib/Probability/Kernel/CondDistrib.lean b/Mathlib/Probability/Kernel/CondDistrib.lean index db4d3fd70641c5..ad984f062007c1 100644 --- a/Mathlib/Probability/Kernel/CondDistrib.lean +++ b/Mathlib/Probability/Kernel/CondDistrib.lean @@ -72,20 +72,20 @@ variable {mβ : MeasurableSpace β} {s : Set Ω} {t : Set β} {f : β × Ω → /-- If the singleton `{x}` has non-zero mass for `μ.map X`, then for all `s : Set Ω`, `condDistrib Y X μ x s = (μ.map X {x})⁻¹ * μ.map (fun a => (X a, Y a)) ({x} ×ˢ s)` . -/ -lemma condDistrib_apply_of_ne_zero [MeasurableSingletonClass β] - (hY : Measurable Y) (x : β) (hX : μ.map X {x} ≠ 0) (s : Set Ω) : +lemma condDistrib_apply_of_ne_zero [MeasurableSingletonClass β] (hX : Measurable X) + (hY : Measurable Y) (x : β) (hX' : μ.map X {x} ≠ 0) (s : Set Ω) : condDistrib Y X μ x s = (μ.map X {x})⁻¹ * μ.map (fun a => (X a, Y a)) ({x} ×ˢ s) := by rw [condDistrib, Measure.condKernel_apply_of_ne_zero _ s] - · rw [Measure.fst_map_prodMk hY] - · rwa [Measure.fst_map_prodMk hY] + · rw [Measure.fst_map_prodMk hX hY] + · rwa [Measure.fst_map_prodMk hX hY] -lemma compProd_map_condDistrib (hY : AEMeasurable Y μ) : +lemma compProd_map_condDistrib (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) : (μ.map X) ⊗ₘ condDistrib Y X μ = μ.map fun a ↦ (X a, Y a) := by - rw [condDistrib, ← Measure.fst_map_prodMk₀ hY, Measure.disintegrate] + rw [condDistrib, ← Measure.fst_map_prodMk₀ hX hY, Measure.disintegrate] lemma condDistrib_comp_map (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) : condDistrib Y X μ ∘ₘ (μ.map X) = μ.map Y := by - rw [← Measure.snd_compProd, compProd_map_condDistrib hY, Measure.snd_map_prodMk₀ hX] + rw [← Measure.snd_compProd, compProd_map_condDistrib hX hY, Measure.snd_map_prodMk₀ hX hY] lemma condDistrib_congr {X' : α → β} {Y' : α → Ω} (hY : Y =ᵐ[μ] Y') (hX : X =ᵐ[μ] X') : condDistrib Y X μ = condDistrib Y' X' μ := by @@ -109,11 +109,12 @@ theorem measurable_condDistrib (hs : MeasurableSet s) : (Kernel.measurable_coe _ hs).comp (Measurable.of_comap_le le_rfl) theorem _root_.MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff - (hY : AEMeasurable Y μ) (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) : + (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) + (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) : (∀ᵐ a ∂μ.map X, Integrable (fun ω => f (a, ω)) (condDistrib Y X μ a)) ∧ Integrable (fun a => ∫ ω, ‖f (a, ω)‖ ∂condDistrib Y X μ a) (μ.map X) ↔ Integrable f (μ.map fun a => (X a, Y a)) := by - rw [condDistrib, ← hf.ae_integrable_condKernel_iff, Measure.fst_map_prodMk₀ hY] + rw [condDistrib, ← hf.ae_integrable_condKernel_iff, Measure.fst_map_prodMk₀ hX hY] variable [NormedSpace ℝ F] @@ -121,15 +122,15 @@ theorem _root_.MeasureTheory.StronglyMeasurable.integral_condDistrib (hf : Stron StronglyMeasurable (fun x ↦ ∫ y, f (x, y) ∂condDistrib Y X μ x) := by rw [condDistrib]; exact hf.integral_kernel_prod_right' -theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map +theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) : AEStronglyMeasurable (fun x => ∫ y, f (x, y) ∂condDistrib Y X μ x) (μ.map X) := by - rw [← Measure.fst_map_prodMk₀ hY, condDistrib]; exact hf.integral_condKernel + rw [← Measure.fst_map_prodMk₀ hX hY, condDistrib]; exact hf.integral_condKernel theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condDistrib (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) : AEStronglyMeasurable (fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a)) μ := - (hf.integral_condDistrib_map hY).comp_aemeasurable hX + (hf.integral_condDistrib_map hX hY).comp_aemeasurable hX theorem stronglyMeasurable_integral_condDistrib (hf : StronglyMeasurable f) : StronglyMeasurable[mβ.comap X] (fun a ↦ ∫ y, f (X a, y) ∂condDistrib Y X μ (X a)) := @@ -138,7 +139,7 @@ theorem stronglyMeasurable_integral_condDistrib (hf : StronglyMeasurable f) : theorem aestronglyMeasurable_integral_condDistrib (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf : AEStronglyMeasurable f (μ.map fun a => (X a, Y a))) : AEStronglyMeasurable[mβ.comap X] (fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a)) μ := - (hf.integral_condDistrib_map hY).comp_ae_measurable' hX + (hf.integral_condDistrib_map hX hY).comp_ae_measurable' hX end Measurability @@ -161,11 +162,9 @@ theorem condDistrib_ae_eq_of_measure_eq_compProd_of_measurable /-- `condDistrib` is a.e. uniquely defined as the kernel satisfying the defining property of `condKernel`. -/ lemma condDistrib_ae_eq_of_measure_eq_compProd - (X : α → β) (hY : AEMeasurable Y μ) {κ : Kernel β Ω} [IsFiniteKernel κ] + (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) {κ : Kernel β Ω} [IsFiniteKernel κ] (hκ : μ.map (fun x => (X x, Y x)) = μ.map X ⊗ₘ κ) : condDistrib Y X μ =ᵐ[μ.map X] κ := by - by_cases hX : AEMeasurable X μ - swap; · simp [Measure.map_of_not_aemeasurable hX, Filter.EventuallyEq] suffices condDistrib (hY.mk Y) (hX.mk X) μ =ᵐ[μ.map (hX.mk X)] κ by rwa [Measure.map_congr hX.ae_eq_mk, condDistrib_congr hY.ae_eq_mk hX.ae_eq_mk] refine condDistrib_ae_eq_of_measure_eq_compProd_of_measurable (μ := μ) @@ -175,41 +174,37 @@ lemma condDistrib_ae_eq_of_measure_eq_compProd · rw [Measure.map_congr hX.ae_eq_mk] lemma condDistrib_ae_eq_iff_measure_eq_compProd - (X : α → β) (hY : AEMeasurable Y μ) (κ : Kernel β Ω) [IsFiniteKernel κ] : + (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (κ : Kernel β Ω) [IsFiniteKernel κ] : (condDistrib Y X μ =ᵐ[μ.map X] κ) ↔ μ.map (fun x => (X x, Y x)) = μ.map X ⊗ₘ κ := by - refine ⟨fun h ↦ ?_, condDistrib_ae_eq_of_measure_eq_compProd X hY⟩ - rw [Measure.compProd_congr h.symm, compProd_map_condDistrib hY] + refine ⟨fun h ↦ ?_, condDistrib_ae_eq_of_measure_eq_compProd hX hY⟩ + rw [Measure.compProd_congr h.symm, compProd_map_condDistrib hX hY] lemma condDistrib_comp {Ω' : Type*} {mΩ' : MeasurableSpace Ω'} [StandardBorelSpace Ω'] - [Nonempty Ω'] (X : α → β) (hY : AEMeasurable Y μ) {f : Ω → Ω'} (hf : Measurable f) : + [Nonempty Ω'] (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) {f : Ω → Ω'} (hf : Measurable f) : condDistrib (f ∘ Y) X μ =ᵐ[μ.map X] (condDistrib Y X μ).map f := by - by_cases hX : AEMeasurable X μ - swap; · simp [Measure.map_of_not_aemeasurable hX, Filter.EventuallyEq] - refine condDistrib_ae_eq_of_measure_eq_compProd X (by fun_prop) ?_ + refine condDistrib_ae_eq_of_measure_eq_compProd hX (by fun_prop) ?_ calc μ.map (fun x ↦ (X x, (f ∘ Y) x)) _ = (μ.map (fun x ↦ (X x, Y x))).map (Prod.map id f) := by rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)] simp [Function.comp_def] - _ = (μ.map X ⊗ₘ condDistrib Y X μ).map (Prod.map id f) := by rw [compProd_map_condDistrib hY] + _ = (μ.map X ⊗ₘ condDistrib Y X μ).map (Prod.map id f) := by rw [compProd_map_condDistrib hX hY] _ = μ.map X ⊗ₘ (condDistrib Y X μ).map f := by rw [Measure.compProd_map hf] -lemma condDistrib_comp_self (X : α → β) {f : β → Ω} (hf : Measurable f) : +lemma condDistrib_comp_self (hX : AEMeasurable X μ) {f : β → Ω} (hf : Measurable f) : condDistrib (f ∘ X) X μ =ᵐ[μ.map X] Kernel.deterministic f hf := by - by_cases hX : AEMeasurable X μ - swap; · simp [Measure.map_of_not_aemeasurable hX, Filter.EventuallyEq] - refine condDistrib_ae_eq_of_measure_eq_compProd X (by fun_prop) ?_ + refine condDistrib_ae_eq_of_measure_eq_compProd hX (by fun_prop) ?_ rw [Measure.compProd_deterministic, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hX] simp [Function.comp_def] -lemma condDistrib_self (Y : α → Ω) : condDistrib Y Y μ =ᵐ[μ.map Y] Kernel.id := by - simpa using! condDistrib_comp_self Y measurable_id +lemma condDistrib_self (hY : AEMeasurable Y μ) : condDistrib Y Y μ =ᵐ[μ.map Y] Kernel.id := by + simpa using! condDistrib_comp_self hY measurable_id -lemma condDistrib_const (X : α → β) (c : Ω) : +lemma condDistrib_const (hX : AEMeasurable X μ) (c : Ω) : condDistrib (fun _ ↦ c) X μ =ᵐ[μ.map X] Kernel.deterministic (mα := mβ) (fun _ ↦ c) (by fun_prop) := by have : (fun _ : α ↦ c) = (fun _ : β ↦ c) ∘ X := rfl rw [this] - filter_upwards [condDistrib_comp_self X (measurable_const (a := c))] with b hb + filter_upwards [condDistrib_comp_self hX (measurable_const (a := c))] with b hb rw [hb] lemma condDistrib_map {γ : Type*} {mγ : MeasurableSpace γ} @@ -217,16 +212,15 @@ lemma condDistrib_map {γ : Type*} {mγ : MeasurableSpace γ} (hX : AEMeasurable X (ν.map f)) (hY : AEMeasurable Y (ν.map f)) (hf : AEMeasurable f ν) : condDistrib Y X (ν.map f) =ᵐ[ν.map (X ∘ f)] condDistrib (Y ∘ f) (X ∘ f) ν := by rw [← AEMeasurable.map_map_of_aemeasurable hX hf] - refine condDistrib_ae_eq_of_measure_eq_compProd (μ := ν.map f) X hY ?_ - rw [AEMeasurable.map_map_of_aemeasurable hX hf, compProd_map_condDistrib (by fun_prop), + refine condDistrib_ae_eq_of_measure_eq_compProd (μ := ν.map f) hX hY ?_ + rw [AEMeasurable.map_map_of_aemeasurable hX hf, + compProd_map_condDistrib (by fun_prop) (by fun_prop), AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf] simp [Function.comp_def] lemma condDistrib_fst_prod {γ : Type*} {mγ : MeasurableSpace γ} - (X : α → β) (hY : AEMeasurable Y μ) (ν : Measure γ) [IsProbabilityMeasure ν] : + (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (ν : Measure γ) [IsProbabilityMeasure ν] : condDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) (μ.prod ν) =ᵐ[μ.map X] condDistrib Y X μ := by - by_cases hX : AEMeasurable X μ - swap; · simp [Measure.map_of_not_aemeasurable hX, Filter.EventuallyEq] have h_map := condDistrib_map (X := X) (Y := Y) (f := Prod.fst (α := α) (β := γ)) (ν := μ.prod ν) (mα := inferInstance) (mβ := inferInstance) (by simpa) (by simpa) (by fun_prop) @@ -235,10 +229,8 @@ lemma condDistrib_fst_prod {γ : Type*} {mγ : MeasurableSpace γ} exact h_map.symm lemma condDistrib_snd_prod {γ : Type*} {mγ : MeasurableSpace γ} - (X : α → β) (hY : AEMeasurable Y μ) (ν : Measure γ) [IsProbabilityMeasure ν] : + (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (ν : Measure γ) [IsProbabilityMeasure ν] : condDistrib (fun ω ↦ Y ω.2) (fun ω ↦ X ω.2) (ν.prod μ) =ᵐ[μ.map X] condDistrib Y X μ := by - by_cases hX : AEMeasurable X μ - swap; · simp [Measure.map_of_not_aemeasurable hX, Filter.EventuallyEq] have h_map := condDistrib_map (X := X) (Y := Y) (f := Prod.snd (β := α) (α := γ)) (ν := ν.prod μ) (mα := inferInstance) (mβ := inferInstance) (by simpa) (by simpa) (by fun_prop) @@ -258,48 +250,48 @@ theorem integrable_toReal_condDistrib (hX : AEMeasurable X μ) (hs : MeasurableS _ = μ univ := lintegral_one _ < ∞ := measure_lt_top _ _ -theorem _root_.MeasureTheory.Integrable.condDistrib_ae_map +theorem _root_.MeasureTheory.Integrable.condDistrib_ae_map (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : ∀ᵐ b ∂μ.map X, Integrable (fun ω => f (b, ω)) (condDistrib Y X μ b) := by - rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hY]; exact hf_int.condKernel_ae + rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hX hY]; exact hf_int.condKernel_ae theorem _root_.MeasureTheory.Integrable.condDistrib_ae (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : ∀ᵐ a ∂μ, Integrable (fun ω => f (X a, ω)) (condDistrib Y X μ (X a)) := - ae_of_ae_map hX (hf_int.condDistrib_ae_map hY) + ae_of_ae_map hX (hf_int.condDistrib_ae_map hX hY) -theorem _root_.MeasureTheory.Integrable.integral_norm_condDistrib_map +theorem _root_.MeasureTheory.Integrable.integral_norm_condDistrib_map (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : Integrable (fun x => ∫ y, ‖f (x, y)‖ ∂condDistrib Y X μ x) (μ.map X) := by - rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hY]; exact hf_int.integral_norm_condKernel + rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hX hY]; exact hf_int.integral_norm_condKernel theorem _root_.MeasureTheory.Integrable.integral_norm_condDistrib (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : Integrable (fun a => ∫ y, ‖f (X a, y)‖ ∂condDistrib Y X μ (X a)) μ := - (hf_int.integral_norm_condDistrib_map hY).comp_aemeasurable hX + (hf_int.integral_norm_condDistrib_map hX hY).comp_aemeasurable hX variable [NormedSpace ℝ F] -theorem _root_.MeasureTheory.Integrable.norm_integral_condDistrib_map +theorem _root_.MeasureTheory.Integrable.norm_integral_condDistrib_map (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : Integrable (fun x => ‖∫ y, f (x, y) ∂condDistrib Y X μ x‖) (μ.map X) := by - rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hY]; exact hf_int.norm_integral_condKernel + rw [condDistrib, ← Measure.fst_map_prodMk₀ (X := X) hX hY]; exact hf_int.norm_integral_condKernel theorem _root_.MeasureTheory.Integrable.norm_integral_condDistrib (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : Integrable (fun a => ‖∫ y, f (X a, y) ∂condDistrib Y X μ (X a)‖) μ := - (hf_int.norm_integral_condDistrib_map hY).comp_aemeasurable hX + (hf_int.norm_integral_condDistrib_map hX hY).comp_aemeasurable hX -theorem _root_.MeasureTheory.Integrable.integral_condDistrib_map +theorem _root_.MeasureTheory.Integrable.integral_condDistrib_map (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : Integrable (fun x => ∫ y, f (x, y) ∂condDistrib Y X μ x) (μ.map X) := - (integrable_norm_iff (hf_int.1.integral_condDistrib_map hY)).mp - (hf_int.norm_integral_condDistrib_map hY) + (integrable_norm_iff (hf_int.1.integral_condDistrib_map hX hY)).mp + (hf_int.norm_integral_condDistrib_map hX hY) theorem _root_.MeasureTheory.Integrable.integral_condDistrib (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) : Integrable (fun a => ∫ y, f (X a, y) ∂condDistrib Y X μ (X a)) μ := - (hf_int.integral_condDistrib_map hY).comp_aemeasurable hX + (hf_int.integral_condDistrib_map hX hY).comp_aemeasurable hX end Integrability @@ -307,7 +299,8 @@ theorem setLIntegral_preimage_condDistrib (hX : Measurable X) (hY : AEMeasurable (hs : MeasurableSet s) (ht : MeasurableSet t) : ∫⁻ a in X ⁻¹' t, condDistrib Y X μ (X a) s ∂μ = μ (X ⁻¹' t ∩ Y ⁻¹' s) := by rw [← lintegral_map (Kernel.measurable_coe _ hs) hX, condDistrib, ← Measure.restrict_map hX ht, - ← Measure.fst_map_prodMk₀ hY, Measure.setLIntegral_condKernel_eq_measure_prod ht hs, + ← Measure.fst_map_prodMk₀ hX.aemeasurable hY, + Measure.setLIntegral_condKernel_eq_measure_prod ht hs, Measure.map_apply_of_aemeasurable (hX.aemeasurable.prodMk hY) (ht.prod hs), mk_preimage_prod] theorem setLIntegral_condDistrib_of_measurableSet (hX : Measurable X) (hY : AEMeasurable Y μ) @@ -350,8 +343,8 @@ theorem condExp_prod_ae_eq_integral_condDistrib' [NormedSpace ℝ F] [CompleteSp rw [← integral_map hX.aemeasurable (f := fun x' => ∫ y, f (x', y) ∂(condDistrib Y X μ) x')] swap · rw [← Measure.restrict_map hX ht] - exact (hf_int.1.integral_condDistrib_map hY).restrict - rw [← Measure.restrict_map hX ht, ← Measure.fst_map_prodMk₀ hY, condDistrib, + exact (hf_int.1.integral_condDistrib_map hX.aemeasurable hY).restrict + rw [← Measure.restrict_map hX ht, ← Measure.fst_map_prodMk₀ hX.aemeasurable hY, condDistrib, Measure.setIntegral_condKernel_univ_right ht hf_int.integrableOn, setIntegral_map (ht.prod MeasurableSet.univ) hf_int.1 (hX.aemeasurable.prodMk hY), mk_preimage_prod, preimage_univ, inter_univ] @@ -395,49 +388,45 @@ theorem condExp_ae_eq_integral_condDistrib' {Ω : Type*} [NormedAddCommGroup Ω] open MeasureTheory theorem _root_.MeasureTheory.AEStronglyMeasurable.comp_snd_map_prodMk {Ω F} {mΩ : MeasurableSpace Ω} - (X : Ω → β) {μ : Measure Ω} [TopologicalSpace F] {f : Ω → F} (hf : AEStronglyMeasurable f μ) : + {X : Ω → β} {μ : Measure Ω} (hX : AEMeasurable X μ) [TopologicalSpace F] {f : Ω → F} + (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun x : β × Ω => f x.2) (μ.map fun ω => (X ω, ω)) := by refine ⟨fun x => hf.mk f x.2, hf.stronglyMeasurable_mk.comp_measurable measurable_snd, ?_⟩ suffices h : Measure.QuasiMeasurePreserving Prod.snd (μ.map fun ω ↦ (X ω, ω)) μ from Measure.QuasiMeasurePreserving.ae_eq_comp h hf.ae_eq_mk refine ⟨measurable_snd, Measure.AbsolutelyContinuous.mk fun s hs hμs => ?_⟩ - rw [Measure.map_apply measurable_snd hs] - by_cases hX : AEMeasurable X μ - · rw [Measure.map_apply_of_aemeasurable] - · rw [← univ_prod, mk_preimage_prod, preimage_univ, univ_inter, preimage_id'] - exact hμs - · exact hX.prodMk aemeasurable_id - · exact measurable_snd hs - · rw [Measure.map_of_not_aemeasurable] - · simp - · contrapose hX; exact measurable_fst.comp_aemeasurable hX + rw [Measure.map_apply measurable_snd hs, Measure.map_apply_of_aemeasurable] + · rw [← univ_prod, mk_preimage_prod, preimage_univ, univ_inter, preimage_id'] + exact hμs + · exact hX.prodMk aemeasurable_id + · exact measurable_snd hs theorem _root_.MeasureTheory.Integrable.comp_snd_map_prodMk - {Ω} {mΩ : MeasurableSpace Ω} (X : Ω → β) {μ : Measure Ω} {f : Ω → F} (hf_int : Integrable f μ) : + {Ω} {mΩ : MeasurableSpace Ω} {X : Ω → β} {μ : Measure Ω} (hX : AEMeasurable X μ) + {f : Ω → F} (hf_int : Integrable f μ) : Integrable (fun x : β × Ω => f x.2) (μ.map fun ω => (X ω, ω)) := by - by_cases hX : AEMeasurable X μ - · have hf := hf_int.1.comp_snd_map_prodMk X (mΩ := mΩ) (mβ := mβ) - refine ⟨hf, ?_⟩ - rw [hasFiniteIntegral_iff_enorm, lintegral_map' hf.enorm (hX.prodMk aemeasurable_id)] - exact hf_int.2 - · rw [Measure.map_of_not_aemeasurable] - · simp - · contrapose hX; exact measurable_fst.comp_aemeasurable hX + have hf := hf_int.1.comp_snd_map_prodMk hX (mΩ := mΩ) (mβ := mβ) + refine ⟨hf, ?_⟩ + rw [hasFiniteIntegral_iff_enorm, lintegral_map' hf.enorm (hX.prodMk aemeasurable_id)] + exact hf_int.2 theorem aestronglyMeasurable_comp_snd_map_prodMk_iff {Ω F} {_ : MeasurableSpace Ω} [TopologicalSpace F] {X : Ω → β} {μ : Measure Ω} (hX : Measurable X) {f : Ω → F} : AEStronglyMeasurable (fun x : β × Ω => f x.2) (μ.map fun ω => (X ω, ω)) ↔ AEStronglyMeasurable f μ := - ⟨fun h => h.comp_measurable (hX.prodMk measurable_id), fun h => h.comp_snd_map_prodMk X⟩ + ⟨fun h => h.comp_measurable (hX.prodMk measurable_id), + fun h => h.comp_snd_map_prodMk hX.aemeasurable⟩ theorem integrable_comp_snd_map_prodMk_iff {Ω} {_ : MeasurableSpace Ω} {X : Ω → β} {μ : Measure Ω} (hX : Measurable X) {f : Ω → F} : Integrable (fun x : β × Ω => f x.2) (μ.map fun ω => (X ω, ω)) ↔ Integrable f μ := - ⟨fun h => h.comp_measurable (hX.prodMk measurable_id), fun h => h.comp_snd_map_prodMk X⟩ + ⟨fun h => h.comp_measurable (hX.prodMk measurable_id), + fun h => h.comp_snd_map_prodMk hX.aemeasurable⟩ theorem condExp_ae_eq_integral_condDistrib_id [NormedSpace ℝ F] [CompleteSpace F] {X : Ω → β} {μ : Measure Ω} [IsFiniteMeasure μ] (hX : Measurable X) {f : Ω → F} (hf_int : Integrable f μ) : μ[f | mβ.comap X] =ᵐ[μ] fun a => ∫ y, f y ∂condDistrib id X μ (X a) := - condExp_prod_ae_eq_integral_condDistrib' hX aemeasurable_id (hf_int.comp_snd_map_prodMk X) + condExp_prod_ae_eq_integral_condDistrib' hX aemeasurable_id + (hf_int.comp_snd_map_prodMk hX.aemeasurable) end ProbabilityTheory diff --git a/Mathlib/Probability/Kernel/Condexp.lean b/Mathlib/Probability/Kernel/Condexp.lean index 462b291681886f..66619490154c03 100644 --- a/Mathlib/Probability/Kernel/Condexp.lean +++ b/Mathlib/Probability/Kernel/Condexp.lean @@ -45,15 +45,16 @@ section AuxLemmas variable {Ω F : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f : Ω → F} -theorem _root_.MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id [TopologicalSpace F] - (hf : AEStronglyMeasurable f μ) : +theorem _root_.MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id (hm : m ≤ mΩ) + [TopologicalSpace F] (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable[m.prod mΩ] (fun x : Ω × Ω => f x.2) - (@Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) Function.diag μ) := hf.comp_snd_map_prodMk id + (@Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) Function.diag μ) := + hf.comp_snd_map_prodMk (@Measurable.aemeasurable Ω Ω mΩ m id μ (measurable_id'' hm)) -theorem _root_.MeasureTheory.Integrable.comp_snd_map_prod_id [NormedAddCommGroup F] +theorem _root_.MeasureTheory.Integrable.comp_snd_map_prod_id (hm : m ≤ mΩ) [NormedAddCommGroup F] (hf : Integrable f μ) : Integrable (fun x : Ω × Ω => f x.2) (@Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) Function.diag μ) := - hf.comp_snd_map_prodMk id + hf.comp_snd_map_prodMk (@Measurable.aemeasurable Ω Ω mΩ m id μ (measurable_id'' hm)) end AuxLemmas @@ -97,13 +98,15 @@ lemma compProd_trim_condExpKernel (hm : m ≤ mΩ) : rw [condExpKernel_eq, trim_eq_map hm] have : m ⊓ mΩ = m := inf_of_le_left hm refine (congrArg _ (Kernel.ext fun a => Measure.ext fun s hs => ?_)).trans - (compProd_map_condDistrib measurable_id.aemeasurable) + (compProd_map_condDistrib (@Measurable.aemeasurable Ω Ω mΩ m id μ (measurable_id'' hm)) + aemeasurable_id) simp only [Kernel.coe_comap, Function.comp_apply, id_eq] congr lemma condExpKernel_comp_trim (hm : m ≤ mΩ) : condExpKernel μ m ∘ₘ μ.trim hm = μ := by rw [← Measure.snd_compProd, compProd_trim_condExpKernel] - exact (@Measure.snd_map_prodMk Ω Ω Ω mΩ m mΩ id id μ (measurable_id'' hm)).trans Measure.map_id + exact (@Measure.snd_map_prodMk Ω Ω Ω mΩ m mΩ id id μ (measurable_id'' hm) measurable_id).trans + Measure.map_id section Measurability @@ -136,7 +139,7 @@ theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condExpKernel [Normed simp_rw [condExpKernel_apply_eq_condDistrib] exact AEStronglyMeasurable.integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id - hf.comp_snd_map_prod_id + (hf.comp_snd_map_prod_id inf_le_right) theorem aestronglyMeasurable_integral_condExpKernel [NormedSpace ℝ F] (hf : AEStronglyMeasurable f μ) : @@ -144,7 +147,8 @@ theorem aestronglyMeasurable_integral_condExpKernel [NormedSpace ℝ F] nontriviality Ω rw [condExpKernel_eq] have h := aestronglyMeasurable_integral_condDistrib - (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id hf.comp_snd_map_prod_id + (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id + (hf.comp_snd_map_prod_id inf_le_right) rw [MeasurableSpace.comap_id] at h exact h.mono inf_le_left @@ -166,7 +170,7 @@ theorem _root_.MeasureTheory.Integrable.condExpKernel_ae (hf_int : Integrable f rw [condExpKernel_eq] convert! Integrable.condDistrib_ae (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id - hf_int.comp_snd_map_prod_id using 1 + (hf_int.comp_snd_map_prod_id inf_le_right) using 1 theorem _root_.MeasureTheory.Integrable.integral_norm_condExpKernel (hf_int : Integrable f μ) : Integrable (fun ω => ∫ y, ‖f y‖ ∂condExpKernel μ m ω) μ := by @@ -174,7 +178,7 @@ theorem _root_.MeasureTheory.Integrable.integral_norm_condExpKernel (hf_int : In rw [condExpKernel_eq] convert! Integrable.integral_norm_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) - aemeasurable_id hf_int.comp_snd_map_prod_id using 1 + aemeasurable_id (hf_int.comp_snd_map_prod_id inf_le_right) using 1 theorem _root_.MeasureTheory.Integrable.norm_integral_condExpKernel [NormedSpace ℝ F] (hf_int : Integrable f μ) : @@ -183,7 +187,7 @@ theorem _root_.MeasureTheory.Integrable.norm_integral_condExpKernel [NormedSpace rw [condExpKernel_eq] convert! Integrable.norm_integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) - aemeasurable_id hf_int.comp_snd_map_prod_id using 1 + aemeasurable_id (hf_int.comp_snd_map_prod_id inf_le_right) using 1 theorem _root_.MeasureTheory.Integrable.integral_condExpKernel [NormedSpace ℝ F] (hf_int : Integrable f μ) : @@ -192,7 +196,7 @@ theorem _root_.MeasureTheory.Integrable.integral_condExpKernel [NormedSpace ℝ rw [condExpKernel_eq] convert! Integrable.integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) - aemeasurable_id hf_int.comp_snd_map_prod_id using 1 + aemeasurable_id (hf_int.comp_snd_map_prod_id inf_le_right) using 1 theorem integrable_toReal_condExpKernel {s : Set Ω} (hs : MeasurableSet s) : Integrable (fun ω => (condExpKernel μ m ω).real s) μ := by diff --git a/Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean b/Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean index 01a681dc71603f..adb882dda797d9 100644 --- a/Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean +++ b/Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean @@ -182,7 +182,7 @@ instance [∀ n, IsZeroOrProbabilityMeasure (μ n)] (I : Finset ℕ) : instance [∀ n, IsProbabilityMeasure (μ n)] (I : Finset ℕ) : IsProbabilityMeasure (inducedFamily μ I) := by rw [inducedFamily] - exact Measure.isProbabilityMeasure_map (measurable_restrict₂ _).aemeasurable + infer_instance /-- Given a family of measures `μ : (n : ℕ) → Measure (Π i : Iic n, X i)`, the induced family equals `μ` over the intervals `Iic n`. -/ @@ -769,8 +769,6 @@ variable {μ₀ : Measure (X 0)} [IsProbabilityMeasure μ₀] set_option backward.isDefEq.respectTransparency false in instance : IsProbabilityMeasure (trajMeasure μ₀ κ) := by rw [trajMeasure] - have : IsProbabilityMeasure (μ₀.map (MeasurableEquiv.piUnique ((fun i : Iic 0 ↦ X i))).symm) := - Measure.isProbabilityMeasure_map <| by fun_prop infer_instance lemma map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure {a : ℕ} : diff --git a/Mathlib/Probability/Moments/Basic.lean b/Mathlib/Probability/Moments/Basic.lean index 8bc06c60bcbd0e..17f19e29a10438 100644 --- a/Mathlib/Probability/Moments/Basic.lean +++ b/Mathlib/Probability/Moments/Basic.lean @@ -475,10 +475,9 @@ theorem measure_le_le_exp_cgf [IsFiniteMeasure μ] (ε : ℝ) (ht : t ≤ 0) end Chernoff -lemma mgf_dirac {x : ℝ} (hX : μ.map X = .dirac x) (t : ℝ) : mgf X μ t = exp (x * t) := by - have : IsProbabilityMeasure (μ.map X) := by rw [hX]; infer_instance - rw [← mgf_id_map (.of_map_ne_zero <| IsProbabilityMeasure.ne_zero _), mgf, hX, integral_dirac, - mul_comm, id_def] +lemma mgf_dirac {x : ℝ} (hX : HasLaw X (.dirac x) μ) (t : ℝ) : mgf X μ t = exp (x * t) := by + have : IsProbabilityMeasure (μ.map X) := by rw [hX.map_eq]; infer_instance + rw [← mgf_id_map hX.aemeasurable, mgf, hX.map_eq, integral_dirac, mul_comm, id_def] lemma mgf_dirac' [MeasurableSingletonClass Ω] {ω : Ω} : mgf X (Measure.dirac ω) t = exp (t * X ω) := by diff --git a/Mathlib/Probability/ProbabilityMassFunction/Basic.lean b/Mathlib/Probability/ProbabilityMassFunction/Basic.lean index d3f10e333090aa..99424f60bcad1d 100644 --- a/Mathlib/Probability/ProbabilityMassFunction/Basic.lean +++ b/Mathlib/Probability/ProbabilityMassFunction/Basic.lean @@ -6,7 +6,7 @@ Authors: Johannes Hölzl, Devon Tuma module public import Mathlib.Topology.Instances.ENNReal.Lemmas -public import Mathlib.MeasureTheory.Measure.Dirac +public import Mathlib.MeasureTheory.Measure.Dirac.Basic /-! # Probability mass functions diff --git a/Mathlib/Probability/ProductMeasure.lean b/Mathlib/Probability/ProductMeasure.lean index 2fa42c3ac915c7..8072c20d5c05ca 100644 --- a/Mathlib/Probability/ProductMeasure.lean +++ b/Mathlib/Probability/ProductMeasure.lean @@ -484,8 +484,6 @@ lemma infinitePi_map_eval (i : ι) : lemma infinitePi_map_pi {Y : ι → Type*} [∀ i, MeasurableSpace (Y i)] {f : (i : ι) → X i → Y i} (hf : ∀ i, Measurable (f i)) : (infinitePi μ).map (fun x i ↦ f i (x i)) = infinitePi (fun i ↦ (μ i).map (f i)) := by - have (i : ι) : IsProbabilityMeasure ((μ i).map (f i)) := - isProbabilityMeasure_map (hf i).aemeasurable refine eq_infinitePi _ fun s t ht ↦ ?_ rw [map_apply (by fun_prop) (.pi s.countable_toSet fun _ _ ↦ ht _)] have : (fun (x : Π i, X i) i ↦ f i (x i)) ⁻¹' ((s : Set ι).pi t) = diff --git a/Mathlib/Probability/StrongLaw.lean b/Mathlib/Probability/StrongLaw.lean index 626be158e016f4..81d5d670b9d64f 100644 --- a/Mathlib/Probability/StrongLaw.lean +++ b/Mathlib/Probability/StrongLaw.lean @@ -219,7 +219,6 @@ theorem sum_prob_mem_Ioc_le {X : Ω → ℝ} (hint : Integrable X) (hnonneg : 0 (hKN : K ≤ N) : ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc (j : ℝ) N} ≤ ENNReal.ofReal (𝔼[X] + 1) := by let ρ : Measure ℝ := Measure.map X ℙ - have : IsProbabilityMeasure ρ := Measure.isProbabilityMeasure_map hint.aemeasurable have A : ∑ j ∈ range K, ∫ _ in j..N, (1 : ℝ) ∂ρ ≤ 𝔼[X] + 1 := calc ∑ j ∈ range K, ∫ _ in j..N, (1 : ℝ) ∂ρ =