Merge pull request #17157 from leanprover-community/master

sync to master

.github/workflows/nightly_detect_failure.yml

@@ -210,7 +210,7 @@ jobs:
             bump_branch_suffix = bump_branch.replace('bump/', '')
             payload = f"🛠️: it looks like it's time to create a new bump/nightly-{current_version} branch from nightly-testing (specifically {sha}), and then PR that to {bump_branch}. "
             payload += "To do so semi-automatically, run the following script from mathlib root:\n\n"
-            payload += f"```bash\n./scripts/create-adaptation-pr.sh {bump_branch_suffix} {current_version}\n```\n"
+            payload += f"```bash\n./scripts/create-adaptation-pr.sh --bumpversion={bump_branch_suffix} --nightlydate={current_version} --nightlysha={sha}\n```\n"
             # Only post if the message is different
             # We compare the first 160 characters, since that includes the date and bump version
             if not messages or messages[0]['content'][:160] != payload[:160]:

Archive/Hairer.lean

@@ -100,7 +100,7 @@ lemma inj_L : Injective (L ι) :=
         fun g hg _h2g g_supp ↦ by
           simpa [mul_comm (g _), L] using congr($hp ⟨g, g_supp.trans ball_subset_closedBall, hg⟩)
     simp_rw [MvPolynomial.funext_iff, map_zero]
-    refine fun x ↦ AnalyticOn.eval_linearMap (EuclideanSpace.equiv ι ℝ).toLinearMap p
+    refine fun x ↦ AnalyticOnNhd.eval_linearMap (EuclideanSpace.equiv ι ℝ).toLinearMap p
       |>.eqOn_zero_of_preconnected_of_eventuallyEq_zero
       (preconnectedSpace_iff_univ.mp inferInstance) (z₀ := 0) trivial
       (Filter.mem_of_superset (Metric.ball_mem_nhds 0 zero_lt_one) ?_) trivial

Mathlib.lean

@@ -56,7 +56,6 @@ import Mathlib.Algebra.BigOperators.Ring.Multiset
 import Mathlib.Algebra.BigOperators.Ring.Nat
 import Mathlib.Algebra.BigOperators.RingEquiv
 import Mathlib.Algebra.BigOperators.WithTop
-import Mathlib.Algebra.Bounds
 import Mathlib.Algebra.Category.AlgebraCat.Basic
 import Mathlib.Algebra.Category.AlgebraCat.Limits
 import Mathlib.Algebra.Category.AlgebraCat.Monoidal
@@ -566,6 +565,7 @@ import Mathlib.Algebra.Order.Field.Canonical.Defs
 import Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Algebra.Order.Field.InjSurj
 import Mathlib.Algebra.Order.Field.Pi
+import Mathlib.Algebra.Order.Field.Pointwise
 import Mathlib.Algebra.Order.Field.Power
 import Mathlib.Algebra.Order.Field.Rat
 import Mathlib.Algebra.Order.Field.Subfield
@@ -577,6 +577,7 @@ import Mathlib.Algebra.Order.Group.Action
 import Mathlib.Algebra.Order.Group.Action.Synonym
 import Mathlib.Algebra.Order.Group.Basic
 import Mathlib.Algebra.Order.Group.Bounds
+import Mathlib.Algebra.Order.Group.CompleteLattice
 import Mathlib.Algebra.Order.Group.Cone
 import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Order.Group.DenselyOrdered
@@ -589,6 +590,8 @@ import Mathlib.Algebra.Order.Group.MinMax
 import Mathlib.Algebra.Order.Group.Nat
 import Mathlib.Algebra.Order.Group.OrderIso
 import Mathlib.Algebra.Order.Group.PiLex
+import Mathlib.Algebra.Order.Group.Pointwise.Bounds
+import Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Algebra.Order.Group.Prod
 import Mathlib.Algebra.Order.Group.Synonym
@@ -644,7 +647,6 @@ import Mathlib.Algebra.Order.Nonneg.Floor
 import Mathlib.Algebra.Order.Nonneg.Module
 import Mathlib.Algebra.Order.Nonneg.Ring
 import Mathlib.Algebra.Order.Pi
-import Mathlib.Algebra.Order.Pointwise
 import Mathlib.Algebra.Order.Positive.Field
 import Mathlib.Algebra.Order.Positive.Ring
 import Mathlib.Algebra.Order.Rearrangement

Mathlib/Algebra/Order/CompleteField.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex J. Best, Yaël Dillies
 -/
 import Mathlib.Algebra.Order.Archimedean.Hom
-import Mathlib.Algebra.Order.Pointwise
+import Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 
 /-!

Mathlib/Algebra/Order/Field/Pointwise.lean

@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2021 Alex J. Best. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Alex J. Best, Yaël Dillies
+-/
+import Mathlib.Algebra.Group.Pointwise.Set
+import Mathlib.Algebra.Order.Field.Basic
+import Mathlib.Algebra.SMulWithZero
+
+/-!
+# Pointwise operations on ordered algebraic objects
+
+This file contains lemmas about the effect of pointwise operations on sets with an order structure.
+-/
+
+open Function Set
+open scoped Pointwise
+
+variable {α : Type*}
+
+namespace LinearOrderedField
+
+variable {K : Type*} [LinearOrderedField K] {a b r : K} (hr : 0 < r)
+include hr
+
+theorem smul_Ioo : r • Ioo a b = Ioo (r • a) (r • b) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Ioo]
+  constructor
+  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
+    constructor
+    · exact (mul_lt_mul_left hr).mpr a_h_left_left
+    · exact (mul_lt_mul_left hr).mpr a_h_left_right
+  · rintro ⟨a_left, a_right⟩
+    use x / r
+    refine ⟨⟨(lt_div_iff' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, ?_⟩
+    rw [mul_div_cancel₀ _ (ne_of_gt hr)]
+
+theorem smul_Icc : r • Icc a b = Icc (r • a) (r • b) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Icc]
+  constructor
+  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
+    constructor
+    · exact (mul_le_mul_left hr).mpr a_h_left_left
+    · exact (mul_le_mul_left hr).mpr a_h_left_right
+  · rintro ⟨a_left, a_right⟩
+    use x / r
+    refine ⟨⟨(le_div_iff₀' hr).mpr a_left, (div_le_iff₀' hr).mpr a_right⟩, ?_⟩
+    rw [mul_div_cancel₀ _ (ne_of_gt hr)]
+
+theorem smul_Ico : r • Ico a b = Ico (r • a) (r • b) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Ico]
+  constructor
+  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
+    constructor
+    · exact (mul_le_mul_left hr).mpr a_h_left_left
+    · exact (mul_lt_mul_left hr).mpr a_h_left_right
+  · rintro ⟨a_left, a_right⟩
+    use x / r
+    refine ⟨⟨(le_div_iff₀' hr).mpr a_left, (div_lt_iff' hr).mpr a_right⟩, ?_⟩
+    rw [mul_div_cancel₀ _ (ne_of_gt hr)]
+
+theorem smul_Ioc : r • Ioc a b = Ioc (r • a) (r • b) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Ioc]
+  constructor
+  · rintro ⟨a, ⟨a_h_left_left, a_h_left_right⟩, rfl⟩
+    constructor
+    · exact (mul_lt_mul_left hr).mpr a_h_left_left
+    · exact (mul_le_mul_left hr).mpr a_h_left_right
+  · rintro ⟨a_left, a_right⟩
+    use x / r
+    refine ⟨⟨(lt_div_iff' hr).mpr a_left, (div_le_iff₀' hr).mpr a_right⟩, ?_⟩
+    rw [mul_div_cancel₀ _ (ne_of_gt hr)]
+
+theorem smul_Ioi : r • Ioi a = Ioi (r • a) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Ioi]
+  constructor
+  · rintro ⟨a_w, a_h_left, rfl⟩
+    exact (mul_lt_mul_left hr).mpr a_h_left
+  · rintro h
+    use x / r
+    constructor
+    · exact (lt_div_iff' hr).mpr h
+    · exact mul_div_cancel₀ _ (ne_of_gt hr)
+
+theorem smul_Iio : r • Iio a = Iio (r • a) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Iio]
+  constructor
+  · rintro ⟨a_w, a_h_left, rfl⟩
+    exact (mul_lt_mul_left hr).mpr a_h_left
+  · rintro h
+    use x / r
+    constructor
+    · exact (div_lt_iff' hr).mpr h
+    · exact mul_div_cancel₀ _ (ne_of_gt hr)
+
+theorem smul_Ici : r • Ici a = Ici (r • a) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Ioi]
+  constructor
+  · rintro ⟨a_w, a_h_left, rfl⟩
+    exact (mul_le_mul_left hr).mpr a_h_left
+  · rintro h
+    use x / r
+    constructor
+    · exact (le_div_iff₀' hr).mpr h
+    · exact mul_div_cancel₀ _ (ne_of_gt hr)
+
+theorem smul_Iic : r • Iic a = Iic (r • a) := by
+  ext x
+  simp only [mem_smul_set, smul_eq_mul, mem_Iio]
+  constructor
+  · rintro ⟨a_w, a_h_left, rfl⟩
+    exact (mul_le_mul_left hr).mpr a_h_left
+  · rintro h
+    use x / r
+    constructor
+    · exact (div_le_iff₀' hr).mpr h
+    · exact mul_div_cancel₀ _ (ne_of_gt hr)
+
+end LinearOrderedField