diff --git a/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean b/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean index 8e3f7ec3ae3617..2793ab68ffe51f 100644 --- a/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean +++ b/Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean @@ -320,21 +320,26 @@ lemma set_lintegral_rnDeriv_le (s : Set α) : ∫⁻ x in s, μ.rnDeriv ν x ∂ν ≤ μ s := (withDensity_apply_le _ _).trans (Measure.le_iff'.1 (withDensity_rnDeriv_le μ ν) s) -lemma set_lintegral_rnDeriv [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) {s : Set α} +lemma set_lintegral_rnDeriv' [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) {s : Set α} (hs : MeasurableSet s) : ∫⁻ x in s, μ.rnDeriv ν x ∂ν = μ s := by rw [← withDensity_apply _ hs, Measure.withDensity_rnDeriv_eq _ _ hμν] +lemma set_lintegral_rnDeriv [HaveLebesgueDecomposition μ ν] [SFinite ν] + (hμν : μ ≪ ν) (s : Set α) : + ∫⁻ x in s, μ.rnDeriv ν x ∂ν = μ s := by + rw [← withDensity_apply' _ s, Measure.withDensity_rnDeriv_eq _ _ hμν] + lemma lintegral_rnDeriv [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) : ∫⁻ x, μ.rnDeriv ν x ∂ν = μ Set.univ := by - rw [← set_lintegral_univ, set_lintegral_rnDeriv hμν MeasurableSet.univ] + rw [← set_lintegral_univ, set_lintegral_rnDeriv' hμν MeasurableSet.univ] lemma integrableOn_toReal_rnDeriv {s : Set α} (hμs : μ s ≠ ∞) : IntegrableOn (fun x ↦ (μ.rnDeriv ν x).toReal) s ν := by refine integrable_toReal_of_lintegral_ne_top (Measure.measurable_rnDeriv _ _).aemeasurable ?_ exact ((set_lintegral_rnDeriv_le _).trans_lt hμs.lt_top).ne -lemma set_integral_toReal_rnDeriv_eq_withDensity [SigmaFinite μ] +lemma set_integral_toReal_rnDeriv_eq_withDensity' [SigmaFinite μ] {s : Set α} (hs : MeasurableSet s) : ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν) s).toReal := by rw [integral_toReal (Measure.measurable_rnDeriv _ _).aemeasurable] @@ -342,6 +347,13 @@ lemma set_integral_toReal_rnDeriv_eq_withDensity [SigmaFinite μ] simp · exact ae_restrict_of_ae (Measure.rnDeriv_lt_top _ _) +lemma set_integral_toReal_rnDeriv_eq_withDensity [SigmaFinite μ] [SFinite ν] (s : Set α) : + ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν) s).toReal := by + rw [integral_toReal (Measure.measurable_rnDeriv _ _).aemeasurable] + · rw [ENNReal.toReal_eq_toReal_iff, ← withDensity_apply' _ s] + simp + · exact ae_restrict_of_ae (Measure.rnDeriv_lt_top _ _) + lemma set_integral_toReal_rnDeriv_le [SigmaFinite μ] {s : Set α} (hμs : μ s ≠ ∞) : ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν ≤ (μ s).toReal := by set t := toMeasurable μ s with ht @@ -353,20 +365,24 @@ lemma set_integral_toReal_rnDeriv_le [SigmaFinite μ] {s : Set α} (hμs : μ s · exact integrableOn_toReal_rnDeriv hμt · exact ae_of_all _ (by simp) _ ≤ (μ t).toReal := by - rw [set_integral_toReal_rnDeriv_eq_withDensity ht_m, ENNReal.toReal_le_toReal _ hμt] + rw [set_integral_toReal_rnDeriv_eq_withDensity' ht_m, ENNReal.toReal_le_toReal _ hμt] · exact withDensity_rnDeriv_le _ _ _ ht_m · exact ((withDensity_rnDeriv_le _ _ _ ht_m).trans_lt hμt.lt_top).ne _ = (μ s).toReal := by rw [← measure_toMeasurable s] -lemma set_integral_toReal_rnDeriv [SigmaFinite μ] [HaveLebesgueDecomposition μ ν] +lemma set_integral_toReal_rnDeriv' [SigmaFinite μ] [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) {s : Set α} (hs : MeasurableSet s) : ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν = (μ s).toReal := by - rw [set_integral_toReal_rnDeriv_eq_withDensity hs, Measure.withDensity_rnDeriv_eq _ _ hμν] -#align measure_theory.measure.with_density_rn_deriv_to_real_eq MeasureTheory.Measure.set_integral_toReal_rnDeriv + rw [set_integral_toReal_rnDeriv_eq_withDensity' hs, Measure.withDensity_rnDeriv_eq _ _ hμν] +#align measure_theory.measure.with_density_rn_deriv_to_real_eq MeasureTheory.Measure.set_integral_toReal_rnDeriv' + +lemma set_integral_toReal_rnDeriv [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) (s : Set α) : + ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν = (μ s).toReal := by + rw [set_integral_toReal_rnDeriv_eq_withDensity s, Measure.withDensity_rnDeriv_eq _ _ hμν] lemma integral_toReal_rnDeriv [SigmaFinite μ] [SigmaFinite ν] (hμν : μ ≪ ν) : ∫ x, (μ.rnDeriv ν x).toReal ∂ν = (μ Set.univ).toReal := by - rw [← integral_univ, set_integral_toReal_rnDeriv hμν MeasurableSet.univ] + rw [← integral_univ, set_integral_toReal_rnDeriv hμν Set.univ] end Measure @@ -380,7 +396,7 @@ theorem withDensityᵥ_rnDeriv_eq (s : SignedMeasure α) (μ : Measure α) [Sigm totalVariation_absolutelyContinuous_iff] at h · ext1 i hi rw [withDensityᵥ_apply (integrable_rnDeriv _ _) hi, rnDeriv, integral_sub, - set_integral_toReal_rnDeriv h.1 hi, set_integral_toReal_rnDeriv h.2 hi] + set_integral_toReal_rnDeriv h.1 i, set_integral_toReal_rnDeriv h.2 i] · conv_rhs => rw [← s.toSignedMeasure_toJordanDecomposition] erw [VectorMeasure.sub_apply] rw [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi] diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean index 82fa9a5474459e..64d043b893cc9f 100644 --- a/Mathlib/Probability/Distributions/Gaussian.lean +++ b/Mathlib/Probability/Distributions/Gaussian.lean @@ -199,14 +199,13 @@ instance instIsProbabilityMeasureGaussianReal (μ : ℝ) (v : ℝ≥0) : IsProbabilityMeasure (gaussianReal μ v) where measure_univ := by by_cases h : v = 0 <;> simp [gaussianReal_of_var_ne_zero, h] -lemma gaussianReal_apply (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) {s : Set ℝ} (hs : MeasurableSet s) : +lemma gaussianReal_apply (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) (s : Set ℝ) : gaussianReal μ v s = ∫⁻ x in s, gaussianPdf μ v x := by - rw [gaussianReal_of_var_ne_zero _ hv, withDensity_apply _ hs] + rw [gaussianReal_of_var_ne_zero _ hv, withDensity_apply' _ s] -lemma gaussianReal_apply_eq_integral (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) - {s : Set ℝ} (hs : MeasurableSet s) : +lemma gaussianReal_apply_eq_integral (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) (s : Set ℝ) : gaussianReal μ v s = ENNReal.ofReal (∫ x in s, gaussianPdfReal μ v x) := by - rw [gaussianReal_apply _ hv hs, ofReal_integral_eq_lintegral_ofReal] + rw [gaussianReal_apply _ hv s, ofReal_integral_eq_lintegral_ofReal] · rfl · exact (integrable_gaussianPdfReal _ _).restrict · exact ae_of_all _ (gaussianPdfReal_nonneg _ _) @@ -266,7 +265,7 @@ lemma gaussianReal_map_add_const (y : ℝ) : ext s' hs' rw [MeasurableEquiv.gaussianReal_map_symm_apply hv e he' hs'] simp only [abs_neg, abs_one, MeasurableEquiv.coe_mk, Equiv.coe_fn_mk, one_mul, ne_eq] - rw [gaussianReal_apply_eq_integral _ hv hs'] + rw [gaussianReal_apply_eq_integral _ hv s'] simp [gaussianPdfReal_sub _ y, Homeomorph.addRight, ← sub_eq_add_neg] /-- The map of a Gaussian distribution by addition of a constant is a Gaussian. -/ @@ -296,7 +295,7 @@ lemma gaussianReal_map_const_mul (c : ℝ) : ext s' hs' rw [MeasurableEquiv.gaussianReal_map_symm_apply hv e he' hs'] simp only [MeasurableEquiv.coe_mk, Equiv.coe_fn_mk, ne_eq, mul_eq_zero] - rw [gaussianReal_apply_eq_integral _ _ hs'] + rw [gaussianReal_apply_eq_integral _ _ s'] swap · simp only [ne_eq, mul_eq_zero, hv, or_false] rw [← NNReal.coe_eq] diff --git a/Mathlib/Probability/Kernel/Basic.lean b/Mathlib/Probability/Kernel/Basic.lean index 28f9ee4002795a..3057d4c9fc9ea5 100644 --- a/Mathlib/Probability/Kernel/Basic.lean +++ b/Mathlib/Probability/Kernel/Basic.lean @@ -308,6 +308,9 @@ instance isFiniteKernel_seq (κ : kernel α β) [h : IsSFiniteKernel κ] (n : h.tsum_finite.choose_spec.1 n #align probability_theory.kernel.is_finite_kernel_seq ProbabilityTheory.kernel.isFiniteKernel_seq +instance IsSFiniteKernel.sFinite [IsSFiniteKernel κ] (a : α) : SFinite (κ a) := + ⟨⟨fun n ↦ seq κ n a, inferInstance, (measure_sum_seq κ a).symm⟩⟩ + instance IsSFiniteKernel.add (κ η : kernel α β) [IsSFiniteKernel κ] [IsSFiniteKernel η] : IsSFiniteKernel (κ + η) := by refine' ⟨⟨fun n => seq κ n + seq η n, fun n => inferInstance, _⟩⟩ diff --git a/Mathlib/Probability/Kernel/WithDensity.lean b/Mathlib/Probability/Kernel/WithDensity.lean index 9d86218cbec7af..4cecda09f06487 100644 --- a/Mathlib/Probability/Kernel/WithDensity.lean +++ b/Mathlib/Probability/Kernel/WithDensity.lean @@ -66,10 +66,10 @@ protected theorem withDensity_apply (κ : kernel α β) [IsSFiniteKernel κ] rfl #align probability_theory.kernel.with_density_apply ProbabilityTheory.kernel.withDensity_apply -theorem withDensity_apply' (κ : kernel α β) [IsSFiniteKernel κ] - (hf : Measurable (Function.uncurry f)) (a : α) {s : Set β} (hs : MeasurableSet s) : +protected theorem withDensity_apply' (κ : kernel α β) [IsSFiniteKernel κ] + (hf : Measurable (Function.uncurry f)) (a : α) (s : Set β) : withDensity κ f a s = ∫⁻ b in s, f a b ∂κ a := by - rw [kernel.withDensity_apply κ hf, withDensity_apply _ hs] + rw [kernel.withDensity_apply κ hf, withDensity_apply' _ s] #align probability_theory.kernel.with_density_apply' ProbabilityTheory.kernel.withDensity_apply' theorem lintegral_withDensity (κ : kernel α β) [IsSFiniteKernel κ] @@ -117,7 +117,7 @@ theorem withDensity_tsum [Countable ι] (κ : kernel α β) [IsSFiniteKernel κ] have h_sum_a : ∀ a, Summable fun n => f n a := fun a => Pi.summable.mpr fun b => ENNReal.summable have h_sum : Summable fun n => f n := Pi.summable.mpr h_sum_a ext a s hs - rw [sum_apply' _ a hs, withDensity_apply' κ _ a hs] + rw [sum_apply' _ a hs, kernel.withDensity_apply' κ _ a s] swap · have : Function.uncurry (∑' n, f n) = ∑' n, Function.uncurry (f n) := by ext1 p @@ -131,7 +131,7 @@ theorem withDensity_tsum [Countable ι] (κ : kernel α β) [IsSFiniteKernel κ] rw [tsum_apply h_sum, tsum_apply (h_sum_a a)] rw [this, lintegral_tsum fun n => (Measurable.of_uncurry_left (hf n)).aemeasurable] congr with n - rw [withDensity_apply' _ (hf n) a hs] + rw [kernel.withDensity_apply' _ (hf n) a s] #align probability_theory.kernel.with_density_tsum ProbabilityTheory.kernel.withDensity_tsum /-- If a kernel `κ` is finite and a function `f : α → β → ℝ≥0∞` is bounded, then `withDensity κ f` @@ -141,7 +141,7 @@ theorem isFiniteKernel_withDensity_of_bounded (κ : kernel α β) [IsFiniteKerne by_cases hf : Measurable (Function.uncurry f) · exact ⟨⟨B * IsFiniteKernel.bound κ, ENNReal.mul_lt_top hB_top (IsFiniteKernel.bound_ne_top κ), fun a => by - rw [withDensity_apply' κ hf a MeasurableSet.univ] + rw [kernel.withDensity_apply' κ hf a Set.univ] calc ∫⁻ b in Set.univ, f a b ∂κ a ≤ ∫⁻ _ in Set.univ, B ∂κ a := lintegral_mono (hf_B a) _ = B * κ a Set.univ := by