chore(*): add mathlib4 synchronization comments (#19218)

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebraic_geometry.elliptic_curve.weierstrass`
* `analysis.complex.upper_half_plane.basic`
* `analysis.complex.upper_half_plane.functions_bounded_at_infty`
* `analysis.complex.upper_half_plane.metric`
* `analysis.complex.upper_half_plane.topology`
* `analysis.fourier.riemann_lebesgue_lemma`
* `analysis.inner_product_space.linear_pmap`
* `analysis.special_functions.gamma.beta`
* `category_theory.closed.ideal`
* `category_theory.monad.equiv_mon`
* `control.random`
* `geometry.euclidean.monge_point`
* `geometry.manifold.complex`
* `geometry.manifold.partition_of_unity`
* `logic.equiv.array`
* `number_theory.legendre_symbol.jacobi_symbol`
* `number_theory.modular`
* `number_theory.modular_forms.jacobi_theta.basic`
* `number_theory.modular_forms.slash_actions`
* `number_theory.modular_forms.slash_invariant_forms`
* `ring_theory.witt_vector.compare`
* `ring_theory.witt_vector.discrete_valuation_ring`
* `ring_theory.witt_vector.domain`
* `ring_theory.witt_vector.frobenius`
* `ring_theory.witt_vector.identities`
* `ring_theory.witt_vector.init_tail`
* `ring_theory.witt_vector.mul_coeff`
* `ring_theory.witt_vector.truncated`
* `ring_theory.witt_vector.verschiebung`
* `set_theory.game.birthday`
* `set_theory.game.impartial`
* `set_theory.surreal.basic`
* `testing.slim_check.gen`
* `testing.slim_check.sampleable`
* `testing.slim_check.testable`

src/algebraic_geometry/elliptic_curve/weierstrass.lean

@@ -11,6 +11,9 @@ import tactic.linear_combination
 /-!
 # Weierstrass equations of elliptic curves
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the structure of an elliptic curve as a nonsingular Weierstrass curve given by a
 Weierstrass equation, which is mathematically accurate in many cases but also good for computation.
 

src/analysis/complex/upper_half_plane/basic.lean

@@ -13,6 +13,9 @@ import tactic.linear_combination
 /-!
 # The upper half plane and its automorphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines `upper_half_plane` to be the upper half plane in `ℂ`.
 
 We furthermore equip it with the structure of an `GL_pos 2 ℝ` action by

src/analysis/complex/upper_half_plane/functions_bounded_at_infty.lean

@@ -11,6 +11,9 @@ import order.filter.zero_and_bounded_at_filter
 /-!
 # Bounded at infinity
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 For complex valued functions on the upper half plane, this file defines the filter `at_im_infty`
 required for defining when functions are bounded at infinity and zero at infinity.
 Both of which are relevant for defining modular forms.

src/analysis/complex/upper_half_plane/metric.lean

@@ -10,6 +10,9 @@ import geometry.euclidean.inversion
 /-!
 # Metric on the upper half-plane
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define a `metric_space` structure on the `upper_half_plane`. We use hyperbolic
 (Poincaré) distance given by
 `dist z w = 2 * arsinh (dist (z : ℂ) w / (2 * real.sqrt (z.im * w.im)))` instead of the induced

src/analysis/complex/upper_half_plane/topology.lean

@@ -13,6 +13,9 @@ import topology.homotopy.contractible
 /-!
 # Topology on the upper half plane
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we introduce a `topological_space` structure on the upper half plane and provide
 various instances.
 -/

src/analysis/fourier/riemann_lebesgue_lemma.lean

@@ -16,6 +16,9 @@ import topology.metric_space.emetric_paracompact
 /-!
 # The Riemann-Lebesgue Lemma
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove the Riemann-Lebesgue lemma, for functions on finite-dimensional real vector
 spaces `V`: if `f` is a function on `V` (valued in a complete normed space `E`), then the
 Fourier transform of `f`, viewed as a function on the dual space of `V`, tends to 0 along the

src/analysis/inner_product_space/linear_pmap.lean

@@ -12,6 +12,9 @@ import topology.algebra.module.basic
 
 # Partially defined linear operators on Hilbert spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We will develop the basics of the theory of unbounded operators on Hilbert spaces.
 
 ## Main definitions

src/analysis/special_functions/gamma/beta.lean

@@ -11,6 +11,9 @@ import analysis.analytic.isolated_zeros
 /-!
 # The Beta function, and further properties of the Gamma function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define the Beta integral, relate Beta and Gamma functions, and prove some
 refined properties of the Gamma function using these relations.
 

src/category_theory/closed/ideal.lean

@@ -14,6 +14,9 @@ import category_theory.subterminal
 /-!
 # Exponential ideals
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 An exponential ideal of a cartesian closed category `C` is a subcategory `D ⊆ C` such that for any
 `B : D` and `A : C`, the exponential `A ⟹ B` is in `D`: resembling ring theoretic ideals. We
 define the notion here for inclusion functors `i : D ⥤ C` rather than explicit subcategories to

src/category_theory/monad/equiv_mon.lean

@@ -11,6 +11,9 @@ import category_theory.monoidal.Mon_
 
 # The equivalence between `Monad C` and `Mon_ (C ⥤ C)`.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A monad "is just" a monoid in the category of endofunctors.
 
 # Definitions/Theorems

src/control/random.lean

@@ -13,6 +13,9 @@ import tactic.norm_num
 /-!
 # Rand Monad and Random Class
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This module provides tools for formulating computations guided by randomness and for
 defining objects that can be created randomly.
 

src/geometry/euclidean/monge_point.lean

@@ -8,6 +8,9 @@ import geometry.euclidean.circumcenter
 /-!
 # Monge point and orthocenter
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the orthocenter of a triangle, via its n-dimensional
 generalization, the Monge point of a simplex.
 

src/geometry/manifold/complex.lean

@@ -10,6 +10,9 @@ import topology.locally_constant.basic
 
 /-! # Holomorphic functions on complex manifolds
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Thanks to the rigidity of complex-differentiability compared to real-differentiability, there are
 many results about complex manifolds with no analogue for manifolds over a general normed field. For
 now, this file contains just two (closely related) such results:

src/geometry/manifold/partition_of_unity.lean

@@ -11,6 +11,9 @@ import topology.shrinking_lemma
 /-!
 # Smooth partition of unity
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define two structures, `smooth_bump_covering` and `smooth_partition_of_unity`. Both
 structures describe coverings of a set by a locally finite family of supports of smooth functions
 with some additional properties. The former structure is mostly useful as an intermediate step in

src/logic/equiv/array.lean

@@ -10,6 +10,9 @@ import control.traversable.equiv
 /-!
 # Equivalences involving `array`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We keep this separate from the file containing `list`-like equivalences as those have no future
 in mathlib4.
 -/

src/number_theory/legendre_symbol/jacobi_symbol.lean

@@ -8,6 +8,9 @@ import number_theory.legendre_symbol.quadratic_reciprocity
 /-!
 # The Jacobi Symbol
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the Jacobi symbol and prove its main properties.
 
 ## Main definitions

src/number_theory/modular.lean

@@ -12,6 +12,9 @@ import linear_algebra.matrix.general_linear_group
 /-!
 # The action of the modular group SL(2, ℤ) on the upper half-plane
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the action of `SL(2,ℤ)` on `ℍ` (via restriction of the `SL(2,ℝ)` action in
 `analysis.complex.upper_half_plane`). We then define the standard fundamental domain
 (`modular_group.fd`, `𝒟`) for this action and show

src/number_theory/modular_forms/jacobi_theta/basic.lean

@@ -10,6 +10,9 @@ import analysis.complex.upper_half_plane.topology
 
 /-! # Jacobi's theta function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the Jacobi theta function
 
 $$\theta(\tau) = \sum_{n \in \mathbb{Z}} \exp (i \pi n ^ 2 \tau),$$

src/number_theory/modular_forms/slash_actions.lean

@@ -9,6 +9,9 @@ import linear_algebra.matrix.special_linear_group
 /-!
 # Slash actions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines a class of slash actions, which are families of right actions of a given group
 parametrized by some Type. This is modeled on the slash action of `GL_pos (fin 2) ℝ` on the space
 of modular forms.

src/number_theory/modular_forms/slash_invariant_forms.lean

@@ -8,6 +8,9 @@ import number_theory.modular_forms.slash_actions
 /-!
 # Slash invariant forms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines functions that are invariant under a `slash_action` which forms the basis for
 defining `modular_form` and `cusp_form`. We prove several instances for such spaces, in particular
 that they form a module.

src/ring_theory/witt_vector/compare.lean

@@ -12,6 +12,9 @@ import number_theory.padics.ring_homs
 
 # Comparison isomorphism between `witt_vector p (zmod p)` and `ℤ_[p]`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We construct a ring isomorphism between `witt_vector p (zmod p)` and `ℤ_[p]`.
 This isomorphism follows from the fact that both satisfy the universal property
 of the inverse limit of `zmod (p^n)`.

src/ring_theory/witt_vector/discrete_valuation_ring.lean

@@ -13,6 +13,9 @@ import tactic.linear_combination
 
 # Witt vectors over a perfect ring
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file establishes that Witt vectors over a perfect field are a discrete valuation ring.
 When `k` is a perfect ring, a nonzero `a : 𝕎 k` can be written as `p^m * b` for some `m : ℕ` and
 `b : 𝕎 k` with nonzero 0th coefficient.

src/ring_theory/witt_vector/domain.lean

@@ -10,6 +10,9 @@ import ring_theory.witt_vector.identities
 
 # Witt vectors over a domain
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file builds to the proof `witt_vector.is_domain`,
 an instance that says if `R` is an integral domain, then so is `𝕎 R`.
 It depends on the API around iterated applications

src/ring_theory/witt_vector/frobenius.lean

@@ -14,6 +14,9 @@ import field_theory.perfect_closure
 /-!
 ## The Frobenius operator
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If `R` has characteristic `p`, then there is a ring endomorphism `frobenius R p`
 that raises `r : R` to the power `p`.
 By applying `witt_vector.map` to `frobenius R p`, we obtain a ring endomorphism `𝕎 R →+* 𝕎 R`.

src/ring_theory/witt_vector/identities.lean

@@ -11,6 +11,9 @@ import ring_theory.witt_vector.mul_p
 /-!
 ## Identities between operations on the ring of Witt vectors
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we derive common identities between the Frobenius and Verschiebung operators.
 
 ## Main declarations

src/ring_theory/witt_vector/init_tail.lean

@@ -11,6 +11,9 @@ import ring_theory.witt_vector.is_poly
 
 # `init` and `tail`
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a Witt vector `x`, we are sometimes interested
 in its components before and after an index `n`.
 This file defines those operations, proves that `init` is polynomial,

src/ring_theory/witt_vector/mul_coeff.lean

@@ -10,6 +10,9 @@ import data.mv_polynomial.supported
 /-!
 # Leading terms of Witt vector multiplication
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The goal of this file is to study the leading terms of the formula for the `n+1`st coefficient
 of a product of Witt vectors `x` and `y` over a ring of characteristic `p`.
 We aim to isolate the `n+1`st coefficients of `x` and `y`, and express the rest of the product

src/ring_theory/witt_vector/truncated.lean

@@ -10,6 +10,9 @@ import ring_theory.witt_vector.init_tail
 
 # Truncated Witt vectors
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The ring of truncated Witt vectors (of length `n`) is a quotient of the ring of Witt vectors.
 It retains the first `n` coefficients of each Witt vector.
 In this file, we set up the basic quotient API for this ring.

src/ring_theory/witt_vector/verschiebung.lean

@@ -11,6 +11,9 @@ import ring_theory.witt_vector.is_poly
 /-!
 ## The Verschiebung operator
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## References
 
 * [Hazewinkel, *Witt Vectors*][Haze09]

src/set_theory/game/birthday.lean

@@ -10,6 +10,9 @@ import set_theory.ordinal.natural_ops
 /-!
 # Birthdays of games
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The birthday of a game is an ordinal that represents at which "step" the game was constructed. We
 define it recursively as the least ordinal larger than the birthdays of its left and right games. We
 prove the basic properties about these.

src/set_theory/game/impartial.lean

@@ -10,6 +10,9 @@ import tactic.nth_rewrite
 /-!
 # Basic definitions about impartial (pre-)games
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We will define an impartial game, one in which left and right can make exactly the same moves.
 Our definition differs slightly by saying that the game is always equivalent to its negative,
 no matter what moves are played. This allows for games such as poker-nim to be classifed as

src/set_theory/surreal/basic.lean

@@ -10,6 +10,9 @@ import set_theory.game.ordinal
 /-!
 # Surreal numbers
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The basic theory of surreal numbers, built on top of the theory of combinatorial (pre-)games.
 
 A pregame is `numeric` if all the Left options are strictly smaller than all the Right options, and

src/testing/slim_check/gen.lean

@@ -11,6 +11,9 @@ import data.list.perm
 /-!
 # `gen` Monad
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This monad is used to formulate randomized computations with a parameter
 to specify the desired size of the result.
 

src/testing/slim_check/sampleable.lean

@@ -14,6 +14,9 @@ import tactic.linarith
 /-!
 # `sampleable` Class
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This class permits the creation samples of a given type
 controlling the size of those values using the `gen` monad`. It also
 helps minimize examples by creating smaller versions of given values.

src/testing/slim_check/testable.lean

@@ -9,6 +9,9 @@ import testing.slim_check.sampleable
 /-!
 # `testable` Class
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Testable propositions have a procedure that can generate counter-examples
 together with a proof that they invalidate the proposition.