Fixed two typos in Blog, (#84)

leanprover-community · Jul 1, 2024 · f7d4acf · f7d4acf
1 parent 4f7d251
commit f7d4acf
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/posts/month-in-mathlib/2024/mim-2024-05.md b/posts/month-in-mathlib/2024/mim-2024-05.md
@@ -28,7 +28,7 @@ There were 667 PRs merged in May 2024.
     * [PR #12917](https://github.com/leanprover-community/mathlib4/pull/12917) by Jonas van der Schaaf, Amelia Livingston and later Christian Merten defines closed immersions.
 
 * Analysis.
-    * Jireh Loreaux and Anatole Dedecker completed the development of the non-unital continuous functional calculus. Although the generic API has been in place for a few months, the relevant instances for C⋆-algebras were missing. Work progressed in a piecemeal fashion, but [PR #13326](https://github.com/leanprover-community/mathlib4/pull/13326) provides a version of the Stone-Weiertrass theorem for continuous functions vanishing at zero, namely that the non-unital star subalgebra generated by the identity function is dense. This is essential for [PR #13363](https://github.com/leanprover-community/mathlib4/pull/13363) which provides uniqueness instances for the non-unital continuous functional calculus. Then [PR #13327](https://github.com/leanprover-community/mathlib4/pull/13327) and [PR #13365](https://github.com/leanprover-community/mathlib4/pull/13365) provide instances of the non-unital continuous functional calculus for non-unital C⋆-algebras and generic restriction lemmas for scalar subrings. These are obtained by first considering the unitization of the algebra, obtaining a unital functional calculus there, and then realizing a non-unital functional calculus by appropriately restricting the unital one to functions vanishing at zero. Finally, [PR #13541](https://github.com/leanprover-community/mathlib4/pull/13541) obtains a non-unital continuous functional calculus from a unital one, which will be necessary to get a non-unital instance on matrices, for example.
+    * Jireh Loreaux and Anatole Dedecker completed the development of the non-unital continuous functional calculus. Although the generic API has been in place for a few months, the relevant instances for C⋆-algebras were missing. Work progressed in a piecemeal fashion, but [PR #13326](https://github.com/leanprover-community/mathlib4/pull/13326) provides a version of the Stone-Weierstrass theorem for continuous functions vanishing at zero, namely that the non-unital star subalgebra generated by the identity function is dense. This is essential for [PR #13363](https://github.com/leanprover-community/mathlib4/pull/13363) which provides uniqueness instances for the non-unital continuous functional calculus. Then [PR #13327](https://github.com/leanprover-community/mathlib4/pull/13327) and [PR #13365](https://github.com/leanprover-community/mathlib4/pull/13365) provide instances of the non-unital continuous functional calculus for non-unital C⋆-algebras and generic restriction lemmas for scalar subrings. These are obtained by first considering the unitization of the algebra, obtaining a unital functional calculus there, and then realizing a non-unital functional calculus by appropriately restricting the unital one to functions vanishing at zero. Finally, [PR #13541](https://github.com/leanprover-community/mathlib4/pull/13541) obtains a non-unital continuous functional calculus from a unital one, which will be necessary to get a non-unital instance on matrices, for example.
     * Sébastien Gouëzel completed the proof that the Fourier transform is well defined on the Schwartz space of a Euclidean space. [PR #12769](https://github.com/leanprover-community/mathlib4/pull/12769) shows how one can bound derivatives of the Fourier transform of a function (multiplied by a power function) in terms of derivatives of the initial function (multiplied by a power function) and [PR #11937](https://github.com/leanprover-community/mathlib4/pull/11937) proves a version of integration by parts for line/Fréchet derivatives. [PR #12144](https://github.com/leanprover-community/mathlib4/pull/12144) puts these results together to define the Fourier transform as a continuous linear equivalence on Schwartz space (taking advantage of the Fourier inversion formula to get the inverse direction from the forward direction). Note that the Schwartz space is a Fréchet space but not a normed space, so this builds on a lot of analysis on Fréchet spaces in terms of families of seminorms.
     * Chris Birkbeck proved that Eisenstein series converge uniformly in [PR #10377](https://github.com/leanprover-community/mathlib4/pull/10377) and that they are holomorphic in [PR #11013](https://github.com/leanprover-community/mathlib4/pull/11013). This will soon be used to show that they are modular forms.
     * Xavier Généreux proved the Hadamard three-lines theorem in the special case of the unit vertical strip in [PR #7919](https://github.com/leanprover-community/mathlib4/pull/7919). This will be used to interpolate norms.
@@ -74,7 +74,7 @@ There were 667 PRs merged in May 2024.
     * Vasily Nesterov implemented a simplex algorithm oracle in [PR #12014](https://github.com/leanprover-community/mathlib4/pull/12014). This is now the default oracle for `linarith` instead of the much slower Fourier-Motzkin oracle.
     * [PR #13190](https://github.com/leanprover-community/mathlib4/pull/13190) and [PR #13293](https://github.com/leanprover-community/mathlib4/pull/13293) by Michael Rothgang and Damiano Testa neuters a very pernicious footgun: Contrary to expectations, `attribute [non_local_attribute] decl in` would **globally** tag `decl` with attribute `non_local_attribute`.
 
-* General library maintainance.
+* General library maintenance.
     * We are slowly getting rid of Lean 3-inspired syntax in Mathlib. New uses will soon be linted against in Mathlib and we encourage downstream projects to follow suit and adopt the new syntax.
         * `refine'` is a tactic that mimics the Lean 3 behavior of `refine`, mostly useful when porting Lean 3 code. It was decided to avoid using it in favor of the more declarative `refine`, or of `apply` in the rare cases where `refine` handles metavariables suboptimally. The following PRs started replacing `refine'` with `refine` or `apply`: [PR #12755](https://github.com/leanprover-community/mathlib4/pull/12755), [PR #12851](https://github.com/leanprover-community/mathlib4/pull/12851), [PR #12997](https://github.com/leanprover-community/mathlib4/pull/12997), [PR #13059](https://github.com/leanprover-community/mathlib4/pull/13059), [PR #13062](https://github.com/leanprover-community/mathlib4/pull/13062), [PR #13166](https://github.com/leanprover-community/mathlib4/pull/13166), [PR #13234](https://github.com/leanprover-community/mathlib4/pull/13234), [PR #13287](https://github.com/leanprover-community/mathlib4/pull/13287), [PR #13357](https://github.com/leanprover-community/mathlib4/pull/13357), [PR #13383](https://github.com/leanprover-community/mathlib4/pull/13383), [PR #13472](https://github.com/leanprover-community/mathlib4/pull/13472), [PR #13474](https://github.com/leanprover-community/mathlib4/pull/13474), [PR #13490](https://github.com/leanprover-community/mathlib4/pull/13490), [PR #13385](https://github.com/leanprover-community/mathlib4/pull/13385).
         * "Stream-of-consciousness `obtain`" is now deprecated. [PR #12850](https://github.com/leanprover-community/mathlib4/pull/12850) and [PR #13219](https://github.com/leanprover-community/mathlib4/pull/13219) removed all occurrences of this syntax in Mathlib.
@@ -86,4 +86,4 @@ There were 667 PRs merged in May 2024.
         * In a similar fashion, some simp lemmas accidentally had a lambda on their LHS, meaning that their key in simp's discrimination tree was maximally general and that simp would try rewriting with them in every location. Some such lemmas were unsimped in [PR #13164](https://github.com/leanprover-community/mathlib4/pull/13164).
     * A sustained effort has started to reduce spurious dependencies between files. There are two lines of work:
         * Reducing the long pole: Assuming Mathlib is built on an infinitely parallelizing machine, there is some sequence of files, each importing the previous, that takes the longest to build. We call this sequence the "long pole". As it is a cap on performance, it is natural to try shortening it. After [PR #12777](https://github.com/leanprover-community/mathlib4/pull/12777), [PR #12401](https://github.com/leanprover-community/mathlib4/pull/12401), the long pole has left the `RingTheory` folder entirely.
-        * Reducing imports to basic files: The theory of basic algebra, order theory and data structures feed into each other at various points. For example, we need to know some order properties of addition and multiplication on `Nat` and `Int` to talk about powers in a group, and we need finite sets to define finite sums and finite suprema/infima. It is overwhelmingly easy to create an almost-circular import graph ricocheting between those three areas. The `Nat`- and `Int`-specific lemmas in Core and Batteries are an opportunity to cut the knot: These lemmas do not depend on Mathlib's algebraic order hierarchy, hence can be used in basic algebra and data structures without over-importing. The following PRs are steps towards that: [PR #11986](https://github.com/leanprover-community/mathlib4/pull/11986), [PR #12710](https://github.com/leanprover-community/mathlib4/pull/12710), [PR #12828](https://github.com/leanprover-community/mathlib4/pull/12828), [PR #12736](https://github.com/leanprover-community/mathlib4/pull/12736), [PR #12825](https://github.com/leanprover-community/mathlib4/pull/12825), [PR #12817](https://github.com/leanprover-community/mathlib4/pull/12817), [PR #12823](https://github.com/leanprover-community/mathlib4/pull/12823), [PR #12872](https://github.com/leanprover-community/mathlib4/pull/12872), [PR #12829](https://github.com/leanprover-community/mathlib4/pull/12829), [PR #12862](https://github.com/leanprover-community/mathlib4/pull/12862), [PR #12835](https://github.com/leanprover-community/mathlib4/pull/12835), [PR #12821](https://github.com/leanprover-community/mathlib4/pull/12821), [PR #12818](https://github.com/leanprover-community/mathlib4/pull/12818), [PR #12836](https://github.com/leanprover-community/mathlib4/pull/12836), [PR #12832](https://github.com/leanprover-community/mathlib4/pull/12832), [PR #12882](https://github.com/leanprover-community/mathlib4/pull/12882), [PR #12975](https://github.com/leanprover-community/mathlib4/pull/12975), [PR #11855](https://github.com/leanprover-community/mathlib4/pull/11855), [PR #13029](https://github.com/leanprover-community/mathlib4/pull/13029), [PR #12985](https://github.com/leanprover-community/mathlib4/pull/12985), [PR #13008](https://github.com/leanprover-community/mathlib4/pull/13008), [PR #13033](https://github.com/leanprover-community/mathlib4/pull/13033), [PR #12845](https://github.com/leanprover-community/mathlib4/pull/12845), [PR #12974](https://github.com/leanprover-community/mathlib4/pull/12974), [PR #11863](https://github.com/leanprover-community/mathlib4/pull/11863), [PR #12959](https://github.com/leanprover-community/mathlib4/pull/12959), [PR #13030](https://github.com/leanprover-community/mathlib4/pull/13030), [PR #13031](https://github.com/leanprover-community/mathlib4/pull/13031), [PR #13005](https://github.com/leanprover-community/mathlib4/pull/13005), [PR #13140](https://github.com/leanprover-community/mathlib4/pull/13140), [PR #13139](https://github.com/leanprover-community/mathlib4/pull/13139), [PR #12990](https://github.com/leanprover-community/mathlib4/pull/12990), [PR #13184](https://github.com/leanprover-community/mathlib4/pull/13184), [PR #13197](https://github.com/leanprover-community/mathlib4/pull/13197), [PR #13138](https://github.com/leanprover-community/mathlib4/pull/13138), [PR #12957](https://github.com/leanprover-community/mathlib4/pull/12957), [PR #13222](https://github.com/leanprover-community/mathlib4/pull/13222), [PR #13224](https://github.com/leanprover-community/mathlib4/pull/13224), [PR #13242](https://github.com/leanprover-community/mathlib4/pull/13242), [PR #13288](https://github.com/leanprover-community/mathlib4/pull/13288), [PR #13003](https://github.com/leanprover-community/mathlib4/pull/13003), [PR #13205](https://github.com/leanprover-community/mathlib4/pull/13205), [PR #13289](https://github.com/leanprover-community/mathlib4/pull/13289), [PR #13244](https://github.com/leanprover-community/mathlib4/pull/13244), [PR #13305](https://github.com/leanprover-community/mathlib4/pull/13305), [PR #13274](https://github.com/leanprover-community/mathlib4/pull/13274), [PR #13253](https://github.com/leanprover-community/mathlib4/pull/13253), [PR #13268](https://github.com/leanprover-community/mathlib4/pull/13268), [PR #13147](https://github.com/leanprover-community/mathlib4/pull/13147), [PR #13243](https://github.com/leanprover-community/mathlib4/pull/13243).
+        * Reducing imports to basic files: The theory of basic algebra, order theory and data structures feed into each other at various points. For example, we need to know some order properties of addition and multiplication on `Nat` and `Int` to talk about powers in a group, and we need finite sets to define finite sums and finite suprema/infima. It is overwhelmingly easy to create an almost-circular import graph ricocheting between those three areas. The `Nat`- and `Int`-specific lemmas in Core and Batteries are an opportunity to cut the knot: These lemmas do not depend on Mathlib's algebraic order hierarchy, hence can be used in basic algebra and data structures without over-importing. The following PRs are steps towards that: [PR #11986](https://github.com/leanprover-community/mathlib4/pull/11986), [PR #12710](https://github.com/leanprover-community/mathlib4/pull/12710), [PR #12828](https://github.com/leanprover-community/mathlib4/pull/12828), [PR #12736](https://github.com/leanprover-community/mathlib4/pull/12736), [PR #12825](https://github.com/leanprover-community/mathlib4/pull/12825), [PR #12817](https://github.com/leanprover-community/mathlib4/pull/12817), [PR #12823](https://github.com/leanprover-community/mathlib4/pull/12823), [PR #12872](https://github.com/leanprover-community/mathlib4/pull/12872), [PR #12829](https://github.com/leanprover-community/mathlib4/pull/12829), [PR #12862](https://github.com/leanprover-community/mathlib4/pull/12862), [PR #12835](https://github.com/leanprover-community/mathlib4/pull/12835), [PR #12821](https://github.com/leanprover-community/mathlib4/pull/12821), [PR #12818](https://github.com/leanprover-community/mathlib4/pull/12818), [PR #12836](https://github.com/leanprover-community/mathlib4/pull/12836), [PR #12832](https://github.com/leanprover-community/mathlib4/pull/12832), [PR #12882](https://github.com/leanprover-community/mathlib4/pull/12882), [PR #12975](https://github.com/leanprover-community/mathlib4/pull/12975), [PR #11855](https://github.com/leanprover-community/mathlib4/pull/11855), [PR #13029](https://github.com/leanprover-community/mathlib4/pull/13029), [PR #12985](https://github.com/leanprover-community/mathlib4/pull/12985), [PR #13008](https://github.com/leanprover-community/mathlib4/pull/13008), [PR #13033](https://github.com/leanprover-community/mathlib4/pull/13033), [PR #12845](https://github.com/leanprover-community/mathlib4/pull/12845), [PR #12974](https://github.com/leanprover-community/mathlib4/pull/12974), [PR #11863](https://github.com/leanprover-community/mathlib4/pull/11863), [PR #12959](https://github.com/leanprover-community/mathlib4/pull/12959), [PR #13030](https://github.com/leanprover-community/mathlib4/pull/13030), [PR #13031](https://github.com/leanprover-community/mathlib4/pull/13031), [PR #13005](https://github.com/leanprover-community/mathlib4/pull/13005), [PR #13140](https://github.com/leanprover-community/mathlib4/pull/13140), [PR #13139](https://github.com/leanprover-community/mathlib4/pull/13139), [PR #12990](https://github.com/leanprover-community/mathlib4/pull/12990), [PR #13184](https://github.com/leanprover-community/mathlib4/pull/13184), [PR #13197](https://github.com/leanprover-community/mathlib4/pull/13197), [PR #13138](https://github.com/leanprover-community/mathlib4/pull/13138), [PR #12957](https://github.com/leanprover-community/mathlib4/pull/12957), [PR #13222](https://github.com/leanprover-community/mathlib4/pull/13222), [PR #13224](https://github.com/leanprover-community/mathlib4/pull/13224), [PR #13242](https://github.com/leanprover-community/mathlib4/pull/13242), [PR #13288](https://github.com/leanprover-community/mathlib4/pull/13288), [PR #13003](https://github.com/leanprover-community/mathlib4/pull/13003), [PR #13205](https://github.com/leanprover-community/mathlib4/pull/13205), [PR #13289](https://github.com/leanprover-community/mathlib4/pull/13289), [PR #13244](https://github.com/leanprover-community/mathlib4/pull/13244), [PR #13305](https://github.com/leanprover-community/mathlib4/pull/13305), [PR #13274](https://github.com/leanprover-community/mathlib4/pull/13274), [PR #13253](https://github.com/leanprover-community/mathlib4/pull/13253), [PR #13268](https://github.com/leanprover-community/mathlib4/pull/13268), [PR #13147](https://github.com/leanprover-community/mathlib4/pull/13147), [PR #13243](https://github.com/leanprover-community/mathlib4/pull/13243).