bump to nightly-2023-06-12-23

mathlib commit leanprover-community/mathlib@ccdbfb6
leanprover-community · Jun 12, 2023 · d8dd37b · d8dd37b
1 parent ec76327
commit d8dd37b
Show file tree

Hide file tree

Showing 3 changed files with 58 additions and 48 deletions.
diff --git a/Mathbin/Probability/Density.lean b/Mathbin/Probability/Density.lean
@@ -64,38 +64,42 @@ open TopologicalSpace MeasureTheory.Measure
 
 variable {Ω E : Type _} [MeasurableSpace E]
 
+#print MeasureTheory.HasPDF /-
 /-- A random variable `X : Ω → E` is said to `has_pdf` with respect to the measure `ℙ` on `Ω` and
 `μ` on `E` if there exists a measurable function `f` such that the push-forward measure of `ℙ`
 along `X` equals `μ.with_density f`. -/
-class HasPdf {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω)
+class HasPDF {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω)
     (μ : Measure E := by exact MeasureTheory.MeasureSpace.volume) : Prop where
   pdf' : Measurable X ∧ ∃ f : E → ℝ≥0∞, Measurable f ∧ map X ℙ = μ.withDensity f
-#align measure_theory.has_pdf MeasureTheory.HasPdf
+#align measure_theory.has_pdf MeasureTheory.HasPDF
+-/
 
 @[measurability]
-theorem HasPdf.measurable {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω)
-    (μ : Measure E := by exact MeasureTheory.MeasureSpace.volume) [hX : HasPdf X ℙ μ] :
+theorem HasPDF.measurable {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω)
+    (μ : Measure E := by exact MeasureTheory.MeasureSpace.volume) [hX : HasPDF X ℙ μ] :
     Measurable X :=
   hX.pdf'.1
-#align measure_theory.has_pdf.measurable MeasureTheory.HasPdf.measurable
+#align measure_theory.has_pdf.measurable MeasureTheory.HasPDF.measurable
 
+#print MeasureTheory.pdf /-
 /-- If `X` is a random variable that `has_pdf X ℙ μ`, then `pdf X` is the measurable function `f`
 such that the push-forward measure of `ℙ` along `X` equals `μ.with_density f`. -/
 def pdf {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω)
     (μ : Measure E := by exact MeasureTheory.MeasureSpace.volume) :=
-  if hX : HasPdf X ℙ μ then Classical.choose hX.pdf'.2 else 0
+  if hX : HasPDF X ℙ μ then Classical.choose hX.pdf'.2 else 0
 #align measure_theory.pdf MeasureTheory.pdf
+-/
 
 theorem pdf_undef {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E}
-    (h : ¬HasPdf X ℙ μ) : pdf X ℙ μ = 0 := by simp only [pdf, dif_neg h]
+    (h : ¬HasPDF X ℙ μ) : pdf X ℙ μ = 0 := by simp only [pdf, dif_neg h]
 #align measure_theory.pdf_undef MeasureTheory.pdf_undef
 
-theorem hasPdf_of_pdf_ne_zero {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E}
-    (h : pdf X ℙ μ ≠ 0) : HasPdf X ℙ μ := by
+theorem hasPDF_of_pdf_ne_zero {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E} {X : Ω → E}
+    (h : pdf X ℙ μ ≠ 0) : HasPDF X ℙ μ := by
   by_contra hpdf
   rw [pdf, dif_neg hpdf] at h 
   exact hpdf (False.ndrec (has_pdf X ℙ μ) (h rfl))
-#align measure_theory.has_pdf_of_pdf_ne_zero MeasureTheory.hasPdf_of_pdf_ne_zero
+#align measure_theory.has_pdf_of_pdf_ne_zero MeasureTheory.hasPDF_of_pdf_ne_zero
 
 theorem pdf_eq_zero_of_not_measurable {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E}
     {X : Ω → E} (hX : ¬Measurable X) : pdf X ℙ μ = 0 :=
@@ -119,15 +123,15 @@ theorem measurable_pdf {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω
 #align measure_theory.measurable_pdf MeasureTheory.measurable_pdf
 
 theorem map_eq_withDensity_pdf {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω)
-    (μ : Measure E := by exact MeasureTheory.MeasureSpace.volume) [hX : HasPdf X ℙ μ] :
+    (μ : Measure E := by exact MeasureTheory.MeasureSpace.volume) [hX : HasPDF X ℙ μ] :
     Measure.map X ℙ = μ.withDensity (pdf X ℙ μ) :=
   by
   rw [pdf, dif_pos hX]
   exact (Classical.choose_spec hX.pdf'.2).2
 #align measure_theory.map_eq_with_density_pdf MeasureTheory.map_eq_withDensity_pdf
 
 theorem map_eq_set_lintegral_pdf {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω)
-    (μ : Measure E := by exact MeasureTheory.MeasureSpace.volume) [hX : HasPdf X ℙ μ] {s : Set E}
+    (μ : Measure E := by exact MeasureTheory.MeasureSpace.volume) [hX : HasPDF X ℙ μ] {s : Set E}
     (hs : MeasurableSet s) : Measure.map X ℙ s = ∫⁻ x in s, pdf X ℙ μ x ∂μ := by
   rw [← with_density_apply _ hs, map_eq_with_density_pdf X ℙ μ]
 #align measure_theory.map_eq_set_lintegral_pdf MeasureTheory.map_eq_set_lintegral_pdf
@@ -136,7 +140,7 @@ namespace Pdf
 
 variable {m : MeasurableSpace Ω} {ℙ : Measure Ω} {μ : Measure E}
 
-theorem lintegral_eq_measure_univ {X : Ω → E} [HasPdf X ℙ μ] : ∫⁻ x, pdf X ℙ μ x ∂μ = ℙ Set.univ :=
+theorem lintegral_eq_measure_univ {X : Ω → E} [HasPDF X ℙ μ] : ∫⁻ x, pdf X ℙ μ x ∂μ = ℙ Set.univ :=
   by
   rw [← set_lintegral_univ, ← map_eq_set_lintegral_pdf X ℙ μ MeasurableSet.univ,
     measure.map_apply (has_pdf.measurable X ℙ μ) MeasurableSet.univ, Set.preimage_univ]
@@ -158,7 +162,7 @@ theorem ofReal_toReal_ae_eq [IsFiniteMeasure ℙ] {X : Ω → E} :
   ofReal_toReal_ae_eq ae_lt_top
 #align measure_theory.pdf.of_real_to_real_ae_eq MeasureTheory.pdf.ofReal_toReal_ae_eq
 
-theorem integrable_iff_integrable_mul_pdf [IsFiniteMeasure ℙ] {X : Ω → E} [HasPdf X ℙ μ] {f : E → ℝ}
+theorem integrable_iff_integrable_mul_pdf [IsFiniteMeasure ℙ] {X : Ω → E} [HasPDF X ℙ μ] {f : E → ℝ}
     (hf : Measurable f) :
     Integrable (fun x => f (X x)) ℙ ↔ Integrable (fun x => f x * (pdf X ℙ μ x).toReal) μ :=
   by
@@ -170,7 +174,7 @@ theorem integrable_iff_integrable_mul_pdf [IsFiniteMeasure ℙ] {X : Ω → E} [
 /-- **The Law of the Unconscious Statistician**: Given a random variable `X` and a measurable
 function `f`, `f ∘ X` is a random variable with expectation `∫ x, f x * pdf X ∂μ`
 where `μ` is a measure on the codomain of `X`. -/
-theorem integral_fun_mul_eq_integral [IsFiniteMeasure ℙ] {X : Ω → E} [HasPdf X ℙ μ] {f : E → ℝ}
+theorem integral_fun_mul_eq_integral [IsFiniteMeasure ℙ] {X : Ω → E} [HasPDF X ℙ μ] {f : E → ℝ}
     (hf : Measurable f) : ∫ x, f x * (pdf X ℙ μ x).toReal ∂μ = ∫ x, f (X x) ∂ℙ :=
   by
   by_cases hpdf : integrable (fun x => f x * (pdf X ℙ μ x).toReal) μ
@@ -218,25 +222,25 @@ theorem integral_fun_mul_eq_integral [IsFiniteMeasure ℙ] {X : Ω → E} [HasPd
     all_goals infer_instance
 #align measure_theory.pdf.integral_fun_mul_eq_integral MeasureTheory.pdf.integral_fun_mul_eq_integral
 
-theorem map_absolutelyContinuous {X : Ω → E} [HasPdf X ℙ μ] : map X ℙ ≪ μ := by
+theorem map_absolutelyContinuous {X : Ω → E} [HasPDF X ℙ μ] : map X ℙ ≪ μ := by
   rw [map_eq_with_density_pdf X ℙ μ]; exact with_density_absolutely_continuous _ _
 #align measure_theory.pdf.map_absolutely_continuous MeasureTheory.pdf.map_absolutelyContinuous
 
 /-- A random variable that `has_pdf` is quasi-measure preserving. -/
-theorem to_quasiMeasurePreserving {X : Ω → E} [HasPdf X ℙ μ] : QuasiMeasurePreserving X ℙ μ :=
-  { Measurable := HasPdf.measurable X ℙ μ
+theorem to_quasiMeasurePreserving {X : Ω → E} [HasPDF X ℙ μ] : QuasiMeasurePreserving X ℙ μ :=
+  { Measurable := HasPDF.measurable X ℙ μ
     AbsolutelyContinuous := map_absolutelyContinuous }
 #align measure_theory.pdf.to_quasi_measure_preserving MeasureTheory.pdf.to_quasiMeasurePreserving
 
-theorem haveLebesgueDecomposition_of_hasPdf {X : Ω → E} [hX' : HasPdf X ℙ μ] :
+theorem haveLebesgueDecomposition_of_hasPDF {X : Ω → E} [hX' : HasPDF X ℙ μ] :
     (map X ℙ).HaveLebesgueDecomposition μ :=
   ⟨⟨⟨0, pdf X ℙ μ⟩, by
       simp only [zero_add, measurable_pdf X ℙ μ, true_and_iff, mutually_singular.zero_left,
         map_eq_with_density_pdf X ℙ μ]⟩⟩
-#align measure_theory.pdf.have_lebesgue_decomposition_of_has_pdf MeasureTheory.pdf.haveLebesgueDecomposition_of_hasPdf
+#align measure_theory.pdf.have_lebesgue_decomposition_of_has_pdf MeasureTheory.pdf.haveLebesgueDecomposition_of_hasPDF
 
-theorem hasPdf_iff {X : Ω → E} :
-    HasPdf X ℙ μ ↔ Measurable X ∧ (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ :=
+theorem hasPDF_iff {X : Ω → E} :
+    HasPDF X ℙ μ ↔ Measurable X ∧ (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ :=
   by
   constructor
   · intro hX'
@@ -245,12 +249,12 @@ theorem hasPdf_iff {X : Ω → E} :
     haveI := h_decomp
     refine' ⟨⟨hX, (measure.map X ℙ).rnDeriv μ, measurable_rn_deriv _ _, _⟩⟩
     rwa [with_density_rn_deriv_eq]
-#align measure_theory.pdf.has_pdf_iff MeasureTheory.pdf.hasPdf_iff
+#align measure_theory.pdf.has_pdf_iff MeasureTheory.pdf.hasPDF_iff
 
-theorem hasPdf_iff_of_measurable {X : Ω → E} (hX : Measurable X) :
-    HasPdf X ℙ μ ↔ (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ := by rw [has_pdf_iff];
+theorem hasPDF_iff_of_measurable {X : Ω → E} (hX : Measurable X) :
+    HasPDF X ℙ μ ↔ (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ := by rw [has_pdf_iff];
   simp only [hX, true_and_iff]
-#align measure_theory.pdf.has_pdf_iff_of_measurable MeasureTheory.pdf.hasPdf_iff_of_measurable
+#align measure_theory.pdf.has_pdf_iff_of_measurable MeasureTheory.pdf.hasPDF_iff_of_measurable
 
 section
 
@@ -261,9 +265,9 @@ map also `has_pdf` if `(map g (map X ℙ)).have_lebesgue_decomposition μ`.
 
 `quasi_measure_preserving_has_pdf'` is more useful in the case we are working with a
 probability measure and a real-valued random variable. -/
-theorem quasiMeasurePreserving_hasPdf {X : Ω → E} [HasPdf X ℙ μ] {g : E → F}
+theorem quasiMeasurePreserving_hasPDF {X : Ω → E} [HasPDF X ℙ μ] {g : E → F}
     (hg : QuasiMeasurePreserving g μ ν) (hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν) :
-    HasPdf (g ∘ X) ℙ ν :=
+    HasPDF (g ∘ X) ℙ ν :=
   by
   rw [has_pdf_iff, ← map_map hg.measurable (has_pdf.measurable X ℙ μ)]
   refine' ⟨hg.measurable.comp (has_pdf.measurable X ℙ μ), hmap, _⟩
@@ -273,39 +277,43 @@ theorem quasiMeasurePreserving_hasPdf {X : Ω → E} [HasPdf X ℙ μ] {g : E
   have := hg.absolutely_continuous hs
   rw [map_apply hg.measurable hsm] at this 
   exact set_lintegral_measure_zero _ _ this
-#align measure_theory.pdf.quasi_measure_preserving_has_pdf MeasureTheory.pdf.quasiMeasurePreserving_hasPdf
+#align measure_theory.pdf.quasi_measure_preserving_has_pdf MeasureTheory.pdf.quasiMeasurePreserving_hasPDF
 
-theorem quasiMeasurePreserving_has_pdf' [IsFiniteMeasure ℙ] [SigmaFinite ν] {X : Ω → E}
-    [HasPdf X ℙ μ] {g : E → F} (hg : QuasiMeasurePreserving g μ ν) : HasPdf (g ∘ X) ℙ ν :=
-  quasiMeasurePreserving_hasPdf hg inferInstance
-#align measure_theory.pdf.quasi_measure_preserving_has_pdf' MeasureTheory.pdf.quasiMeasurePreserving_has_pdf'
+theorem quasiMeasurePreserving_hasPDF' [IsFiniteMeasure ℙ] [SigmaFinite ν] {X : Ω → E}
+    [HasPDF X ℙ μ] {g : E → F} (hg : QuasiMeasurePreserving g μ ν) : HasPDF (g ∘ X) ℙ ν :=
+  quasiMeasurePreserving_hasPDF hg inferInstance
+#align measure_theory.pdf.quasi_measure_preserving_has_pdf' MeasureTheory.pdf.quasiMeasurePreserving_hasPDF'
 
 end
 
 section Real
 
 variable [IsFiniteMeasure ℙ] {X : Ω → ℝ}
 
+#print Real.hasPDF_iff_of_measurable /-
 /-- A real-valued random variable `X` `has_pdf X ℙ λ` (where `λ` is the Lebesgue measure) if and
 only if the push-forward measure of `ℙ` along `X` is absolutely continuous with respect to `λ`. -/
-theorem Real.hasPdf_iff_of_measurable (hX : Measurable X) : HasPdf X ℙ ↔ map X ℙ ≪ volume :=
+theorem Real.hasPDF_iff_of_measurable (hX : Measurable X) : HasPDF X ℙ ↔ map X ℙ ≪ volume :=
   by
   rw [has_pdf_iff_of_measurable hX, and_iff_right_iff_imp]
   exact fun h => inferInstance
-#align measure_theory.pdf.real.has_pdf_iff_of_measurable MeasureTheory.pdf.Real.hasPdf_iff_of_measurable
+#align measure_theory.pdf.real.has_pdf_iff_of_measurable Real.hasPDF_iff_of_measurable
+-/
 
-theorem Real.hasPdf_iff : HasPdf X ℙ ↔ Measurable X ∧ map X ℙ ≪ volume :=
+#print Real.hasPDF_iff /-
+theorem Real.hasPDF_iff : HasPDF X ℙ ↔ Measurable X ∧ map X ℙ ≪ volume :=
   by
   by_cases hX : Measurable X
   · rw [real.has_pdf_iff_of_measurable hX, iff_and_self]
     exact fun h => hX
     infer_instance
   · exact ⟨fun h => False.elim (hX h.pdf'.1), fun h => False.elim (hX h.1)⟩
-#align measure_theory.pdf.real.has_pdf_iff MeasureTheory.pdf.Real.hasPdf_iff
+#align measure_theory.pdf.real.has_pdf_iff Real.hasPDF_iff
+-/
 
 /-- If `X` is a real-valued random variable that has pdf `f`, then the expectation of `X` equals
 `∫ x, x * f x ∂λ` where `λ` is the Lebesgue measure. -/
-theorem integral_mul_eq_integral [HasPdf X ℙ] : ∫ x, x * (pdf X ℙ volume x).toReal = ∫ x, X x ∂ℙ :=
+theorem integral_mul_eq_integral [HasPDF X ℙ] : ∫ x, x * (pdf X ℙ volume x).toReal = ∫ x, X x ∂ℙ :=
   integral_fun_mul_eq_integral measurable_id
 #align measure_theory.pdf.integral_mul_eq_integral MeasureTheory.pdf.integral_mul_eq_integral
 
@@ -335,18 +343,20 @@ section
 /-! **Uniform Distribution** -/
 
 
+#print MeasureTheory.pdf.IsUniform /-
 /-- A random variable `X` has uniform distribution if it has a probability density function `f`
 with support `s` such that `f = (μ s)⁻¹ 1ₛ` a.e. where `1ₛ` is the indicator function for `s`. -/
 def IsUniform {m : MeasurableSpace Ω} (X : Ω → E) (support : Set E) (ℙ : Measure Ω)
     (μ : Measure E := by exact MeasureTheory.MeasureSpace.volume) :=
   pdf X ℙ μ =ᵐ[μ] support.indicator ((μ support)⁻¹ • 1)
 #align measure_theory.pdf.is_uniform MeasureTheory.pdf.IsUniform
+-/
 
 namespace IsUniform
 
-theorem hasPdf {m : MeasurableSpace Ω} {X : Ω → E} {ℙ : Measure Ω} {μ : Measure E} {s : Set E}
-    (hns : μ s ≠ 0) (hnt : μ s ≠ ∞) (hu : IsUniform X s ℙ μ) : HasPdf X ℙ μ :=
-  hasPdf_of_pdf_ne_zero
+theorem hasPDF {m : MeasurableSpace Ω} {X : Ω → E} {ℙ : Measure Ω} {μ : Measure E} {s : Set E}
+    (hns : μ s ≠ 0) (hnt : μ s ≠ ∞) (hu : IsUniform X s ℙ μ) : HasPDF X ℙ μ :=
+  hasPDF_of_pdf_ne_zero
     (by
       intro hpdf
       rw [is_uniform, hpdf] at hu 
@@ -360,7 +370,7 @@ theorem hasPdf {m : MeasurableSpace Ω} {X : Ω → E} {ℙ : Measure Ω} {μ :
         rw [HEq, Set.inter_univ] at this 
         exact hns this
       exact MeasureTheory.Set.indicator_ae_eq_zero hu.symm)
-#align measure_theory.pdf.is_uniform.has_pdf MeasureTheory.pdf.IsUniform.hasPdf
+#align measure_theory.pdf.is_uniform.has_pdf MeasureTheory.pdf.IsUniform.hasPDF
 
 theorem pdf_toReal_ae_eq {m : MeasurableSpace Ω} {X : Ω → E} {ℙ : Measure Ω} {μ : Measure E}
     {s : Set E} (hX : IsUniform X s ℙ μ) :

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "5a62651346dbc79a3ac8192fb4a198b166c5bd55",
+    "rev": "a24022e2ef96b24f6cb313e072a790d208024bbf",
     "name": "lean3port",
-    "inputRev?": "5a62651346dbc79a3ac8192fb4a198b166c5bd55"}},
+    "inputRev?": "a24022e2ef96b24f6cb313e072a790d208024bbf"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "f16a40917bde07e357c8d1c3500ec8ede96a8750",
+    "rev": "42b5fd46df82c0caa63c84fd3d8098bf307ed3d7",
     "name": "mathlib",
-    "inputRev?": "f16a40917bde07e357c8d1c3500ec8ede96a8750"}},
+    "inputRev?": "42b5fd46df82c0caa63c84fd3d8098bf307ed3d7"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

diff --git a/lakefile.lean b/lakefile.lean
@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-06-12-21"
+def tag : String := "nightly-2023-06-12-23"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"5a62651346dbc79a3ac8192fb4a198b166c5bd55"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"a24022e2ef96b24f6cb313e072a790d208024bbf"
 
 @[default_target]
 lean_lib Mathbin where