bump to nightly-2023-03-26-02

mathlib commit leanprover-community/mathlib@55d771d

Mathbin/Algebra/Category/Group/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 
 ! This file was ported from Lean 3 source module algebra.category.Group.basic
-! leanprover-community/mathlib commit 524793de15bc4c52ee32d254e7d7867c7176b3af
+! leanprover-community/mathlib commit cb3ceec8485239a61ed51d944cb9a95b68c6bafc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.CategoryTheory.Endomorphism
 /-!
 # Category instances for group, add_group, comm_group, and add_comm_group.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We introduce the bundled categories:
 * `Group`
 * `AddGroup`

Mathbin/Algebra/Star/Free.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Weiser
 
 ! This file was ported from Lean 3 source module algebra.star.free
-! leanprover-community/mathlib commit 07c3cf2d851866ff7198219ed3fedf42e901f25c
+! leanprover-community/mathlib commit cb3ceec8485239a61ed51d944cb9a95b68c6bafc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Algebra.FreeAlgebra
 /-!
 # A *-algebra structure on the free algebra.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Reversing words gives a *-structure on the free monoid or on the free algebra on a type.
 
 ## Implementation note

Mathbin/All.lean

@@ -937,7 +937,6 @@ import Mathbin.CategoryTheory.Limits.Presheaf
 import Mathbin.CategoryTheory.Limits.Shapes.BinaryProducts
 import Mathbin.CategoryTheory.Limits.Shapes.Biproducts
 import Mathbin.CategoryTheory.Limits.Shapes.CommSq
-import Mathbin.CategoryTheory.Limits.Shapes.ConcreteCategory
 import Mathbin.CategoryTheory.Limits.Shapes.Diagonal
 import Mathbin.CategoryTheory.Limits.Shapes.DisjointCoproduct
 import Mathbin.CategoryTheory.Limits.Shapes.Equalizers

Mathbin/Analysis/Calculus/BumpFunctionInner.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Floris van Doorn
 
 ! This file was ported from Lean 3 source module analysis.calculus.bump_function_inner
-! leanprover-community/mathlib commit 8c8c544bf24ced19b1e76c34bb3262bdae620f82
+! leanprover-community/mathlib commit 46b633fd842bef9469441c0209906f6dddd2b4f5
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -341,7 +341,7 @@ def someContDiffBumpBase (E : Type _) [NormedAddCommGroup E] [NormedSpace ℝ E]
 #align some_cont_diff_bump_base someContDiffBumpBase
 
 /-- Any inner product space has smooth bump functions. -/
-instance (priority := 100) hasContDiffBump_of_innerProductSpace (E : Type _)
+instance (priority := 100) hasContDiffBump_of_innerProductSpace (E : Type _) [NormedAddCommGroup E]
     [InnerProductSpace ℝ E] : HasContDiffBump E :=
   let e : ContDiffBumpBase E :=
     { toFun := fun R x => Real.smoothTransition ((R - ‖x‖) / (R - 1))
@@ -372,7 +372,7 @@ instance (priority := 100) hasContDiffBump_of_innerProductSpace (E : Type _)
           exact cont_diff_at_const.congr_of_eventually_eq this
         · refine' real.smooth_transition.cont_diff_at.comp _ _
           refine' ContDiffAt.div _ _ (sub_pos.2 hR).ne'
-          · exact cont_diff_at_fst.sub (cont_diff_at_snd.norm hx)
+          · exact cont_diff_at_fst.sub (cont_diff_at_snd.norm ℝ hx)
           · exact cont_diff_at_fst.sub contDiffAt_const
       eq_one := fun R hR x hx =>
         Real.smoothTransition.one_of_one_le <| (one_le_div (sub_pos.2 hR)).2 (sub_le_sub_left hx _)

Mathbin/Analysis/Calculus/Conformal/InnerProduct.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yourong Zang
 
 ! This file was ported from Lean 3 source module analysis.calculus.conformal.inner_product
-! leanprover-community/mathlib commit 51ad06e5a86554fc42398b6f90b021685ce36665
+! leanprover-community/mathlib commit 46b633fd842bef9469441c0209906f6dddd2b4f5
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -21,7 +21,11 @@ is conformal at `x` iff the derivative preserves inner products up to a scalar m
 
 noncomputable section
 
-variable {E F : Type _} [InnerProductSpace ℝ E] [InnerProductSpace ℝ F]
+variable {E F : Type _}
+
+variable [NormedAddCommGroup E] [NormedAddCommGroup F]
+
+variable [InnerProductSpace ℝ E] [InnerProductSpace ℝ F]
 
 open RealInnerProductSpace
 

Mathbin/Analysis/Convex/Cone/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Frédéric Dupuis
 
 ! This file was ported from Lean 3 source module analysis.convex.cone.basic
-! leanprover-community/mathlib commit c78cad350eb321c81e1eacf68d14e3d3ba1e17f7
+! leanprover-community/mathlib commit 46b633fd842bef9469441c0209906f6dddd2b4f5
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -901,7 +901,7 @@ theorem exists_extension_of_le_sublinear (f : E →ₗ.[ℝ] ℝ) (N : E → ℝ
 
 section Dual
 
-variable {H : Type _} [InnerProductSpace ℝ H] (s t : Set H)
+variable {H : Type _} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (s t : Set H)
 
 open RealInnerProductSpace
 

Mathbin/Analysis/Convex/Segment.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, Yury Kudryashov, Yaël Dillies
 
 ! This file was ported from Lean 3 source module analysis.convex.segment
-! leanprover-community/mathlib commit c5773405394e073885e2a144c9ca14637e8eb963
+! leanprover-community/mathlib commit cb3ceec8485239a61ed51d944cb9a95b68c6bafc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -17,6 +17,9 @@ import Mathbin.Tactic.Positivity
 /-!
 # Segments in vector spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In a 𝕜-vector space, we define the following objects and properties.
 * `segment 𝕜 x y`: Closed segment joining `x` and `y`.
 * `open_segment 𝕜 x y`: Open segment joining `x` and `y`.

Mathbin/Analysis/Convex/Star.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 
 ! This file was ported from Lean 3 source module analysis.convex.star
-! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! leanprover-community/mathlib commit cb3ceec8485239a61ed51d944cb9a95b68c6bafc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.Analysis.Convex.Segment
 /-!
 # Star-convex sets
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This files defines star-convex sets (aka star domains, star-shaped set, radially convex set).
 
 A set is star-convex at `x` if every segment from `x` to a point in the set is contained in the set.

Mathbin/Analysis/Convex/Topology.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, Yury Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.convex.topology
-! leanprover-community/mathlib commit a63928c34ec358b5edcda2bf7513c50052a5230f
+! leanprover-community/mathlib commit 0e3aacdc98d25e0afe035c452d876d28cbffaa7e
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -28,12 +28,12 @@ We prove the following facts:
 
 assert_not_exists Norm
 
-variable {ι : Type _} {E : Type _}
-
 open Metric Set
 
 open Pointwise Convex
 
+variable {ι 𝕜 E : Type _}
+
 theorem Real.convex_iff_isPreconnected {s : Set ℝ} : Convex ℝ s ↔ IsPreconnected s :=
   convex_iff_ordConnected.trans isPreconnected_iff_ordConnected.symm
 #align real.convex_iff_is_preconnected Real.convex_iff_isPreconnected
@@ -82,9 +82,40 @@ end stdSimplex
 /-! ### Topological vector space -/
 
 
+section TopologicalSpace
+
+variable [LinearOrderedRing 𝕜] [DenselyOrdered 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜]
+  [AddCommGroup E] [TopologicalSpace E] [ContinuousAdd E] [Module 𝕜 E] [ContinuousSMul 𝕜 E]
+  {x y : E}
+
+theorem segment_subset_closure_openSegment : [x -[𝕜] y] ⊆ closure (openSegment 𝕜 x y) :=
+  by
+  rw [segment_eq_image, openSegment_eq_image, ← closure_Ioo (zero_ne_one' 𝕜)]
+  exact image_closure_subset_closure_image (by continuity)
+#align segment_subset_closure_open_segment segment_subset_closure_openSegment
+
+end TopologicalSpace
+
+section PseudoMetricSpace
+
+variable [LinearOrderedRing 𝕜] [DenselyOrdered 𝕜] [PseudoMetricSpace 𝕜] [OrderTopology 𝕜]
+  [ProperSpace 𝕜] [CompactIccSpace 𝕜] [AddCommGroup E] [TopologicalSpace E] [T2Space E]
+  [ContinuousAdd E] [Module 𝕜 E] [ContinuousSMul 𝕜 E]
+
+@[simp]
+theorem closure_openSegment (x y : E) : closure (openSegment 𝕜 x y) = [x -[𝕜] y] :=
+  by
+  rw [segment_eq_image, openSegment_eq_image, ← closure_Ioo (zero_ne_one' 𝕜)]
+  exact
+    (image_closure_of_isCompact (bounded_Ioo _ _).isCompact_closure <|
+        Continuous.continuousOn <| by continuity).symm
+#align closure_open_segment closure_openSegment
+
+end PseudoMetricSpace
+
 section ContinuousConstSMul
 
-variable {𝕜 : Type _} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
+variable [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
   [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
 
 /-- If `s` is a convex set, then `a • interior s + b • closure s ⊆ interior s` for all `0 < a`,

Mathbin/Analysis/Fourier/AddCircle.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Heather Macbeth, David Loeffler
 
 ! This file was ported from Lean 3 source module analysis.fourier.add_circle
-! leanprover-community/mathlib commit 8cce17e5783303db93df6810de9d85dd0f9e402a
+! leanprover-community/mathlib commit 46b633fd842bef9469441c0209906f6dddd2b4f5
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -483,7 +483,7 @@ theorem tsum_sq_fourierCoeff (f : lp ℂ 2 <| @haarAddCircle T hT) :
     exact_mod_cast lp.norm_rpow_eq_tsum _ (fourier_basis.repr f)
     norm_num
   have H₂ : ‖fourier_basis.repr f‖ ^ 2 = ‖f‖ ^ 2 := by simp
-  have H₃ := congr_arg IsROrC.re (@L2.inner_def (AddCircle T) ℂ ℂ _ _ _ _ f f)
+  have H₃ := congr_arg IsROrC.re (@L2.inner_def (AddCircle T) ℂ ℂ _ _ _ _ _ f f)
   rw [← integral_re] at H₃
   · simp only [← norm_sq_eq_inner] at H₃
     rw [← H₁, H₂, H₃]

Mathbin/Analysis/InnerProductSpace/Adjoint.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Frédéric Dupuis, Heather Macbeth
 
 ! This file was ported from Lean 3 source module analysis.inner_product_space.adjoint
-! leanprover-community/mathlib commit 9f0d61b4475e3c3cba6636ab51cdb1f3949d2e1d
+! leanprover-community/mathlib commit 46b633fd842bef9469441c0209906f6dddd2b4f5
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -52,6 +52,8 @@ open ComplexConjugate
 
 variable {𝕜 E F G : Type _} [IsROrC 𝕜]
 
+variable [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G]
+
 variable [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [InnerProductSpace 𝕜 G]
 
 -- mathport name: «expr⟪ , ⟫»
@@ -259,7 +261,11 @@ instance : CstarRing (E →L[𝕜] E) :=
 
 section Real
 
-variable {E' : Type _} {F' : Type _} [InnerProductSpace ℝ E'] [InnerProductSpace ℝ F']
+variable {E' : Type _} {F' : Type _}
+
+variable [NormedAddCommGroup E'] [NormedAddCommGroup F']
+
+variable [InnerProductSpace ℝ E'] [InnerProductSpace ℝ F']
 
 variable [CompleteSpace E'] [CompleteSpace F']
 
@@ -486,7 +492,11 @@ theorem isSymmetric_iff_isSelfAdjoint (A : E →ₗ[𝕜] E) : IsSymmetric A ↔
 
 section Real
 
-variable {E' : Type _} {F' : Type _} [InnerProductSpace ℝ E'] [InnerProductSpace ℝ F']
+variable {E' : Type _} {F' : Type _}
+
+variable [NormedAddCommGroup E'] [NormedAddCommGroup F']
+
+variable [InnerProductSpace ℝ E'] [InnerProductSpace ℝ F']
 
 variable [FiniteDimensional ℝ E'] [FiniteDimensional ℝ F']