Merge branch 'leanprover-community:master' into main

Author: CoolRmal

Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean

@@ -142,7 +142,7 @@ lemma ball_eq_singleton {n : ℕ} : Metric.ball n ((2 : ℝ) ^ (-n - 1 : ℤ)) =
 
 
 theorem TopIsDiscrete : DiscreteTopology ℕ := by
-  apply singletons_open_iff_discrete.mp
+  apply discreteTopology_iff_isOpen_singleton.mpr
   intro
   simpa only [← ball_eq_singleton] using isOpen_ball
 

Counterexamples/SorgenfreyLine.lean

@@ -231,8 +231,8 @@ theorem isClosed_of_subset_antidiagonal {s : Set (ℝₗ × ℝₗ)} {c : ℝₗ
 
 open Subtype in
 instance (c : ℝₗ) : DiscreteTopology {x : ℝₗ × ℝₗ | x.1 + x.2 = c} :=
-  forall_open_iff_discrete.1 fun U ↦ isClosed_compl_iff.1 <| isClosed_induced_iff.2
-    ⟨val '' Uᶜ, isClosed_of_subset_antidiagonal <| coe_image_subset _ Uᶜ,
+  discreteTopology_iff_forall_isClosed.2 fun C ↦ isClosed_induced_iff.2
+    ⟨val '' C, isClosed_of_subset_antidiagonal <| coe_image_subset _ C,
       preimage_image_eq _ val_injective⟩
 
 /-- The Sorgenfrey plane `ℝₗ × ℝₗ` is not a normal space. -/

Mathlib.lean

@@ -1706,6 +1706,7 @@ import Mathlib.Analysis.InnerProductSpace.Convex
 import Mathlib.Analysis.InnerProductSpace.Defs
 import Mathlib.Analysis.InnerProductSpace.Dual
 import Mathlib.Analysis.InnerProductSpace.EuclideanDist
+import Mathlib.Analysis.InnerProductSpace.GramMatrix
 import Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
 import Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
 import Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
@@ -2884,6 +2885,7 @@ import Mathlib.CategoryTheory.Triangulated.TriangleShift
 import Mathlib.CategoryTheory.Triangulated.Triangulated
 import Mathlib.CategoryTheory.Triangulated.Yoneda
 import Mathlib.CategoryTheory.Types.Basic
+import Mathlib.CategoryTheory.Types.Monomorphisms
 import Mathlib.CategoryTheory.Types.Set
 import Mathlib.CategoryTheory.UnivLE
 import Mathlib.CategoryTheory.Whiskering
@@ -5585,6 +5587,7 @@ import Mathlib.RingTheory.Grassmannian
 import Mathlib.RingTheory.HahnSeries.Addition
 import Mathlib.RingTheory.HahnSeries.Basic
 import Mathlib.RingTheory.HahnSeries.HEval
+import Mathlib.RingTheory.HahnSeries.HahnEmbedding
 import Mathlib.RingTheory.HahnSeries.Lex
 import Mathlib.RingTheory.HahnSeries.Multiplication
 import Mathlib.RingTheory.HahnSeries.PowerSeries

Mathlib/Algebra/Algebra/Equiv.lean

@@ -817,3 +817,25 @@ def ULift.algEquiv {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Alge
     ULift.{w} A ≃ₐ[R] A where
   __ := ULift.ringEquiv
   commutes' _ := rfl
+
+/-- If an `R`-algebra `A` is isomorphic to `R` as `R`-module, then the canonical map `R → A` is an
+equivalence of `R`-algebras.
+
+Note that if `e : R ≃ₗ[R] A` is the linear equivalence, then this is not the same as the equivalence
+of algebras provided here unless `e 1 = 1`. -/
+@[simps] def LinearEquiv.algEquivOfRing
+    {R A : Type*} [CommSemiring R] [CommSemiring A] [Algebra R A]
+    (e : R ≃ₗ[R] A) : R ≃ₐ[R] A where
+  __ := Algebra.ofId R A
+  invFun x := e.symm (e 1 * x)
+  left_inv x := calc
+    e.symm (e 1 * (algebraMap R A) x)
+      = e.symm (x • e 1) := by rw [Algebra.smul_def, mul_comm]
+    _ = x := by rw [map_smul, e.symm_apply_apply, smul_eq_mul, mul_one]
+  right_inv x := calc
+    (algebraMap R A) (e.symm (e 1 * x))
+      = (algebraMap R A) (e.symm (e 1 * x)) * e (e.symm 1 • 1) := by
+          rw [smul_eq_mul, mul_one, e.apply_symm_apply, mul_one]
+    _ = x := by rw [map_smul, Algebra.smul_def, mul_left_comm, ← Algebra.smul_def _ (e 1),
+          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, ← mul_assoc, ← Algebra.smul_def,
+          ← map_smul, smul_eq_mul, mul_one, e.apply_symm_apply, one_mul]

Mathlib/Algebra/Order/Module/HahnEmbedding.lean

@@ -28,7 +28,7 @@ under `ArchimedeanClass.closedBall K c`. The embeddings from these submodules ar
 `HahnEmbedding.Seed K M R`.
 
 By setting `K = ℚ` and `R = ℝ`, the condition can be trivially satisfied, leading
-to a proof of the classic Hahn embedding theorem. (TODO: implement this)
+to a proof of the classic Hahn embedding theorem. (See `hahnEmbedding_isOrderedAddMonoid`)
 
 ## Main theorem
 

Mathlib/Analysis/Analytic/IsolatedZeros.lean

@@ -342,8 +342,8 @@ theorem AnalyticAt.map_nhdsNE {x : 𝕜} {f : 𝕜 → E} (hfx : AnalyticAt 𝕜
 Preimages of codiscrete sets: if `f` is analytic on a neighbourhood of `U` and not locally constant,
 then the preimage of any subset codiscrete within `f '' U` is codiscrete within `U`.
 
-See `AnalyticOnNhd.preimage_zero_codiscreteWithin` for the special case that `s` is the complement
-of zero. Applications might want to use the theorem `Filter.codiscreteWithin.mono`.
+See `AnalyticOnNhd.preimage_zero_mem_codiscreteWithin` for the special case that `s` is the
+complement of zero. Applications might want to use the theorem `Filter.codiscreteWithin.mono`.
 -/
 theorem AnalyticOnNhd.preimage_mem_codiscreteWithin {U : Set 𝕜} {s : Set E} {f : 𝕜 → E}
     (hfU : AnalyticOnNhd 𝕜 f U) (h₂f : ∀ x ∈ U, ¬EventuallyConst f (𝓝 x))

Mathlib/Analysis/Calculus/TangentCone.lean

@@ -591,22 +591,25 @@ end Normed
 section RealNormed
 variable [NormedAddCommGroup G] [NormedSpace ℝ G]
 
-/-- In a real vector space, a convex set with nonempty interior is a set of unique
-differentiability at every point of its closure. -/
-theorem uniqueDiffWithinAt_convex {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty)
-    {x : G} (hx : x ∈ closure s) : UniqueDiffWithinAt ℝ s x := by
+theorem Convex.span_tangentConeAt {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty)
+    {x : G} (hx : x ∈ closure s) : Submodule.span ℝ (tangentConeAt ℝ s x) = ⊤ := by
   rcases hs with ⟨y, hy⟩
   suffices y - x ∈ interior (tangentConeAt ℝ s x) by
-    refine ⟨Dense.of_closure ?_, hx⟩
-    simp [(Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
-        ⟨y - x, interior_mono Submodule.subset_span this⟩]
+    apply (Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
+    exact ⟨y - x, interior_mono Submodule.subset_span this⟩
   rw [mem_interior_iff_mem_nhds]
   replace hy : interior s ∈ 𝓝 y := IsOpen.mem_nhds isOpen_interior hy
   apply mem_of_superset ((isOpenMap_sub_right x).image_mem_nhds hy)
   rintro _ ⟨z, zs, rfl⟩
   refine mem_tangentConeAt_of_openSegment_subset (Subset.trans ?_ interior_subset)
   exact conv.openSegment_closure_interior_subset_interior hx zs
 
+/-- In a real vector space, a convex set with nonempty interior is a set of unique
+differentiability at every point of its closure. -/
+theorem uniqueDiffWithinAt_convex {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty)
+    {x : G} (hx : x ∈ closure s) : UniqueDiffWithinAt ℝ s x := by
+  simp [uniqueDiffWithinAt_iff, conv.span_tangentConeAt hs hx, hx]
+
 /-- In a real vector space, a convex set with nonempty interior is a set of unique
 differentiability. -/
 theorem uniqueDiffOn_convex {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty) :

Mathlib/Analysis/InnerProductSpace/GramMatrix.lean

@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2025 Peter Pfaffelhuber. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Peter Pfaffelhuber
+-/
+
+import Mathlib.LinearAlgebra.Matrix.PosDef
+
+/-! # Gram Matrices
+
+This file defines Gram matrices and proves their positive semidefiniteness.
+Results require `RCLike 𝕜`.
+
+## Main definition
+
+* `Matrix.gram` : the `Matrix n n 𝕜` with `⟪v i, v j⟫` at `i j : n`, where `v : n → E` for an
+  `Inner 𝕜 E`.
+
+## Main results
+
+* `Matrix.posSemidef_gram`: Gram matrices are positive semidefinite.
+* `Matrix.posDef_gram_iff_linearIndependent`: Linear independence of `v` is
+  equivalent to positive definiteness of `gram 𝕜 v`.
+-/
+
+open RCLike Real Matrix
+
+open scoped InnerProductSpace ComplexOrder ComplexConjugate
+
+variable {E n α 𝕜 : Type*}
+namespace Matrix
+
+/-- The entries of a Gram matrix are inner products of vectors in an inner product space. -/
+def gram (𝕜 : Type*) [Inner 𝕜 E] (v : n → E) : Matrix n n 𝕜 := of fun i j ↦ ⟪v i, v j⟫_𝕜
+
+@[simp]
+lemma gram_apply [Inner 𝕜 E] (v : n → E) (i j : n) :
+    (gram 𝕜 v) i j = ⟪v i, v j⟫_𝕜 := rfl
+
+variable [RCLike 𝕜]
+
+section SemiInnerProductSpace
+variable [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E]
+
+@[simp]
+lemma gram_zero : gram 𝕜 (0 : n → E) = 0 := Matrix.ext fun _ _ ↦ inner_zero_left _
+
+@[simp]
+lemma gram_single [DecidableEq n] (i : n) (x : E) :
+    gram 𝕜 (Pi.single i x) = Matrix.single i i ⟪x, x⟫_𝕜 := by
+  ext j k
+  obtain hij | rfl := ne_or_eq i j
+  · simp [hij]
+  obtain hik | rfl := ne_or_eq i k
+  · simp [hik]
+  simp
+
+lemma submatrix_gram (v : n → E) {m : Set n} (f : m → n) :
+  (gram 𝕜 v).submatrix f f = gram 𝕜 (v ∘ f) := rfl
+
+variable (𝕜) in
+/-- A Gram matrix is Hermitian. -/
+lemma isHermitian_gram (v : n → E) : (gram 𝕜 v).IsHermitian :=
+  Matrix.ext fun _ _ ↦ inner_conj_symm _ _
+
+variable [Fintype n]
+
+theorem star_dotProduct_gram_mulVec (v : n → E) (x y : n → 𝕜) :
+    star x ⬝ᵥ (gram 𝕜 v) *ᵥ y = ⟪∑ i, x i • v i, ∑ i, y i • v i⟫_𝕜 := by
+  trans ∑ i, ∑ j, conj (x i) * y j * ⟪v i, v j⟫_𝕜
+  · simp_rw [dotProduct, mul_assoc, ← Finset.mul_sum, mulVec, dotProduct, mul_comm, ← star_def,
+      gram_apply, Pi.star_apply]
+  · simp_rw [sum_inner, inner_sum, inner_smul_left, inner_smul_right, mul_assoc]
+
+variable (𝕜) in
+/-- A Gram matrix is positive semidefinite. -/
+theorem posSemidef_gram (v : n → E) :
+    PosSemidef (gram 𝕜 v) := by
+  refine ⟨isHermitian_gram _ _, fun x ↦ ?_⟩
+  rw [star_dotProduct_gram_mulVec, le_iff_re_im]
+  simp [inner_self_nonneg]
+
+/-- In a normed space, positive definiteness of `gram 𝕜 v` implies linear independence of `v`. -/
+theorem linearIndependent_of_posDef_gram {v : n → E} (h_gram : PosDef (gram 𝕜 v)) :
+    LinearIndependent 𝕜 v := by
+  rw [Fintype.linearIndependent_iff]
+  intro y hy
+  obtain ⟨h1, h2⟩ := h_gram
+  specialize h2 y
+  simp_all [star_dotProduct_gram_mulVec]
+
+end SemiInnerProductSpace
+
+section NormedInnerProductSpace
+variable [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype n]
+
+/-- In a normed space, linear independence of `v` implies positive definiteness of `gram 𝕜 v`. -/
+theorem posDef_gram_of_linearIndependent
+    {v : n → E} (h_li : LinearIndependent 𝕜 v) : PosDef (gram 𝕜 v) := by
+  rw [Fintype.linearIndependent_iff] at h_li
+  obtain ⟨h0, h1⟩ := posSemidef_gram 𝕜 v
+  refine ⟨h0, fun x hx ↦ (h1 x).lt_of_ne' ?_⟩
+  rw [star_dotProduct_gram_mulVec, inner_self_eq_zero.ne]
+  exact mt (h_li x) (mt funext hx)
+
+/-- In a normed space, linear independence of `v` is equivalent to positive definiteness of
+`gram 𝕜 v`. -/
+theorem posDef_gram_iff_linearIndependent {v : n → E} :
+    PosDef (gram 𝕜 v) ↔ LinearIndependent 𝕜 v :=
+  ⟨linearIndependent_of_posDef_gram, posDef_gram_of_linearIndependent⟩
+
+end NormedInnerProductSpace
+
+end Matrix

Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean

@@ -76,6 +76,10 @@ theorem log_of_nat_eq_posLog {n : ℕ} : log⁺ n = log n := by
   · simp [hn, posLog]
   · simp [posLog_eq_log, Nat.one_le_iff_ne_zero.2 hn]
 
+/-- The function `log⁺` equals `log (max 1 _)` for non-negative real numbers. -/
+theorem posLog_eq_log_max_one {x : ℝ} (hx : 0 ≤ x) : log⁺ x = log (max 1 x) := by
+  grind [le_abs, posLog_eq_log, log_one, max_eq_left, log_nonpos, posLog_def]
+
 /-- The function `log⁺` is monotone on the positive axis. -/
 theorem monotoneOn_posLog : MonotoneOn log⁺ (Set.Ici 0) := by
   intro x hx y hy hxy

Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

@@ -791,6 +791,10 @@ theorem of_bot' {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ :
     IsPullback h₁₁ (t.lift (h₁₁ ≫ v₁₂) v₃₁ (by rw [Category.assoc, s.w])) v₁₂ h₂₁ :=
   of_bot ((t.lift_snd _ _ _) ▸ s) (by simp only [lift_fst]) t
 
+instance [HasPullbacksAlong f] (h : P ⟶ Y) : HasPullback h (pullback.fst g f) :=
+  IsPullback.hasPullback (IsPullback.of_bot' (IsPullback.of_hasPullback (h ≫ g) f)
+    (IsPullback.of_hasPullback g f))
+
 section
 
 variable [HasZeroObject C] [HasZeroMorphisms C]