bump to nightly-2023-12-05-10

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Dynamics/Ergodic/Conservative.lean

@@ -61,7 +61,7 @@ returns back to `s` under some iteration of `f`. -/
 structure Conservative (f : α → α)
     (μ : Measure α := by exact MeasureTheory.MeasureSpace.volume) extends
     QuasiMeasurePreserving f μ μ : Prop where
-  exists_mem_image_mem :
+  exists_mem_iterate_mem :
     ∀ ⦃s⦄, MeasurableSet s → μ s ≠ 0 → ∃ x ∈ s, ∃ (m : _) (_ : m ≠ 0), (f^[m]) x ∈ s
 #align measure_theory.conservative MeasureTheory.Conservative
 -/
@@ -70,7 +70,7 @@ structure Conservative (f : α → α)
 /-- A self-map preserving a finite measure is conservative. -/
 protected theorem MeasurePreserving.conservative [IsFiniteMeasure μ] (h : MeasurePreserving f μ μ) :
     Conservative f μ :=
-  ⟨h.QuasiMeasurePreserving, fun s hsm h0 => h.exists_mem_image_mem hsm h0⟩
+  ⟨h.QuasiMeasurePreserving, fun s hsm h0 => h.exists_mem_iterate_mem hsm h0⟩
 #align measure_theory.measure_preserving.conservative MeasureTheory.MeasurePreserving.conservative
 -/
 
@@ -80,7 +80,7 @@ namespace Conservative
 /-- The identity map is conservative w.r.t. any measure. -/
 protected theorem id (μ : Measure α) : Conservative id μ :=
   { to_quasiMeasurePreserving := QuasiMeasurePreserving.id μ
-    exists_mem_image_mem := fun s hs h0 =>
+    exists_mem_iterate_mem := fun s hs h0 =>
       let ⟨x, hx⟩ := nonempty_of_measure_ne_zero h0
       ⟨x, hx, 1, one_ne_zero, hx⟩ }
 #align measure_theory.conservative.id MeasureTheory.Conservative.id

Mathbin/Dynamics/Ergodic/MeasurePreserving.lean

@@ -174,10 +174,10 @@ protected theorem iterate {f : α → α} (hf : MeasurePreserving f μa μa) :
 
 variable {μ : Measure α} {f : α → α} {s : Set α}
 
-#print MeasureTheory.MeasurePreserving.exists_mem_image_mem_of_volume_lt_mul_volume /-
+#print MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_volume_lt_mul_volume /-
 /-- If `μ univ < n * μ s` and `f` is a map preserving measure `μ`,
 then for some `x ∈ s` and `0 < m < n`, `f^[m] x ∈ s`. -/
-theorem exists_mem_image_mem_of_volume_lt_mul_volume (hf : MeasurePreserving f μ μ)
+theorem exists_mem_iterate_mem_of_volume_lt_mul_volume (hf : MeasurePreserving f μ μ)
     (hs : MeasurableSet s) {n : ℕ} (hvol : μ (univ : Set α) < n * μ s) :
     ∃ x ∈ s, ∃ m ∈ Ioo 0 n, (f^[m]) x ∈ s :=
   by
@@ -192,22 +192,22 @@ theorem exists_mem_image_mem_of_volume_lt_mul_volume (hf : MeasurePreserving f 
   simp only [Set.mem_preimage, Finset.mem_range] at hi hj hxi hxj 
   refine' ⟨(f^[i]) x, hxi, j - i, ⟨tsub_pos_of_lt hlt, lt_of_le_of_lt (j.sub_le i) hj⟩, _⟩
   rwa [← iterate_add_apply, tsub_add_cancel_of_le hlt.le]
-#align measure_theory.measure_preserving.exists_mem_image_mem_of_volume_lt_mul_volume MeasureTheory.MeasurePreserving.exists_mem_image_mem_of_volume_lt_mul_volume
+#align measure_theory.measure_preserving.exists_mem_image_mem_of_volume_lt_mul_volume MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_volume_lt_mul_volume
 -/
 
 /- ./././Mathport/Syntax/Translate/Basic.lean:641:2: warning: expanding binder collection (m «expr ≠ » 0) -/
-#print MeasureTheory.MeasurePreserving.exists_mem_image_mem /-
+#print MeasureTheory.MeasurePreserving.exists_mem_iterate_mem /-
 /-- A self-map preserving a finite measure is conservative: if `μ s ≠ 0`, then at least one point
 `x ∈ s` comes back to `s` under iterations of `f`. Actually, a.e. point of `s` comes back to `s`
 infinitely many times, see `measure_theory.measure_preserving.conservative` and theorems about
 `measure_theory.conservative`. -/
-theorem exists_mem_image_mem [IsFiniteMeasure μ] (hf : MeasurePreserving f μ μ)
+theorem exists_mem_iterate_mem [IsFiniteMeasure μ] (hf : MeasurePreserving f μ μ)
     (hs : MeasurableSet s) (hs' : μ s ≠ 0) : ∃ x ∈ s, ∃ (m : _) (_ : m ≠ 0), (f^[m]) x ∈ s :=
   by
   rcases ENNReal.exists_nat_mul_gt hs' (measure_ne_top μ (univ : Set α)) with ⟨N, hN⟩
   rcases hf.exists_mem_image_mem_of_volume_lt_mul_volume hs hN with ⟨x, hx, m, hm, hmx⟩
   exact ⟨x, hx, m, hm.1.ne', hmx⟩
-#align measure_theory.measure_preserving.exists_mem_image_mem MeasureTheory.MeasurePreserving.exists_mem_image_mem
+#align measure_theory.measure_preserving.exists_mem_image_mem MeasureTheory.MeasurePreserving.exists_mem_iterate_mem
 -/
 
 end MeasurePreserving

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "2e4a3586a8f16713f16b2d2b3af3d8e65f3af087",
+   "rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
+   "rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "c7cff4551258d31c0d2d453b3f9cbca757d445f1",
+   "rev": "3141402ba5a5f0372d2378fd75a481bc79a74ecf",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -49,19 +49,19 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "c72f4d06b1f28f07f7d049118aa2dd1402406346",
+   "rev": "373c9fe4f3de086924aca34042affa7d3bb95475",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "c72f4d06b1f28f07f7d049118aa2dd1402406346",
+   "inputRev": "373c9fe4f3de086924aca34042affa7d3bb95475",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean3port.git",
    "type": "git",
    "subDir": null,
-   "rev": "bd7d116652bdf500a4d1458904bec2948332787b",
+   "rev": "0bc6ffa967946527c6d3dd0bf2ff5b122bce1c4d",
    "name": "lean3port",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "bd7d116652bdf500a4d1458904bec2948332787b",
+   "inputRev": "0bc6ffa967946527c6d3dd0bf2ff5b122bce1c4d",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "mathlib3port",

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-12-03-06"
+def tag : String := "nightly-2023-12-05-10"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"bd7d116652bdf500a4d1458904bec2948332787b"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"0bc6ffa967946527c6d3dd0bf2ff5b122bce1c4d"
 
 @[default_target]
 lean_lib Mathbin where

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.3.0
+leanprover/lean4:v4.4.0-rc1