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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status).
Relates to the following files:
* `algebraic_geometry.locally_ringed_space.has_colimits`
* `analysis.bounded_variation`
* `analysis.fourier.add_circle`
* `analysis.fourier.poisson_summation`
* `probability.borel_cantelli`
* `probability.kernel.disintegration`
* `probability.martingale.borel_cantelli`
* `probability.martingale.convergence`
* `probability.martingale.optional_stopping`
* `probability.martingale.upcrossing`
* `ring_theory.dedekind_domain.integral_closure`
* `ring_theory.localization.norm`
* `ring_theory.norm`
* `ring_theory.polynomial.eisenstein.is_integral`
* `ring_theory.trace`

src/algebraic_geometry/locally_ringed_space/has_colimits.lean

@@ -11,6 +11,9 @@ import category_theory.limits.constructions.limits_of_products_and_equalizers
 /-!
 # Colimits of LocallyRingedSpace
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We construct the explicit coproducts and coequalizers of `LocallyRingedSpace`.
 It then follows that `LocallyRingedSpace` has all colimits, and
 `forget_to_SheafedSpace` preserves them.

src/analysis/bounded_variation.lean

@@ -14,6 +14,9 @@ import tactic.wlog
 /-!
 # Functions of bounded variation
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We study functions of bounded variation. In particular, we show that a bounded variation function
 is a difference of monotone functions, and differentiable almost everywhere. This implies that
 Lipschitz functions from the real line into finite-dimensional vector space are also differentiable

src/analysis/fourier/add_circle.lean

@@ -17,6 +17,9 @@ import measure_theory.integral.fund_thm_calculus
 
 # Fourier analysis on the additive circle
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains basic results on Fourier series for functions on the additive circle
 `add_circle T = ℝ / ℤ • T`.
 

src/analysis/fourier/poisson_summation.lean

@@ -12,6 +12,9 @@ import measure_theory.measure.lebesgue.integral
 /-!
 # Poisson's summation formula
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We prove Poisson's summation formula `∑ (n : ℤ), f n = ∑ (n : ℤ), 𝓕 f n`, where `𝓕 f` is the
 Fourier transform of `f`, under the following hypotheses:
 * `f` is a continuous function `ℝ → ℂ`.

src/probability/borel_cantelli.lean

@@ -11,6 +11,9 @@ import probability.independence.basic
 
 # The second Borel-Cantelli lemma
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains the second Borel-Cantelli lemma which states that, given a sequence of
 independent sets `(sₙ)` in a probability space, if `∑ n, μ sₙ = ∞`, then the limsup of `sₙ` has
 measure 1. We employ a proof using Lévy's generalized Borel-Cantelli by choosing an appropriate

src/probability/kernel/disintegration.lean

@@ -10,6 +10,9 @@ import probability.kernel.integral_comp_prod
 /-!
 # Disintegration of measures on product spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Let `ρ` be a finite measure on `α × Ω`, where `Ω` is a standard Borel space. In mathlib terms, `Ω`
 verifies `[nonempty Ω] [topological_space Ω] [polish_space Ω] [measurable_space Ω] [borel_space Ω]`.
 Then there exists a kernel `ρ.cond_kernel : kernel α Ω` such that for any measurable set

src/probability/martingale/borel_cantelli.lean

@@ -11,6 +11,9 @@ import probability.martingale.centering
 
 # Generalized Borel-Cantelli lemma
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves Lévy's generalized Borel-Cantelli lemma which is a generalization of the
 Borel-Cantelli lemmas. With this generalization, one can easily deduce the Borel-Cantelli lemmas
 by choosing appropriate filtrations. This file also contains the one sided martingale bound which

src/probability/martingale/convergence.lean

@@ -11,6 +11,9 @@ import measure_theory.constructions.polish
 
 # Martingale convergence theorems
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The martingale convergence theorems are a collection of theorems characterizing the convergence
 of a martingale provided it satisfies some boundedness conditions. This file contains the
 almost everywhere martingale convergence theorem which provides an almost everywhere limit to

src/probability/martingale/optional_stopping.lean

@@ -8,6 +8,9 @@ import probability.martingale.basic
 
 /-! # Optional stopping theorem (fair game theorem)
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The optional stopping theorem states that an adapted integrable process `f` is a submartingale if
 and only if for all bounded stopping times `τ` and `π` such that `τ ≤ π`, the
 stopped value of `f` at `τ` has expectation smaller than its stopped value at `π`.

src/probability/martingale/upcrossing.lean

@@ -11,6 +11,9 @@ import probability.martingale.basic
 
 # Doob's upcrossing estimate
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a discrete real-valued submartingale $(f_n)_{n \in \mathbb{N}}$, denoting $U_N(a, b)$ the
 number of times $f_n$ crossed from below $a$ to above $b$ before time $N$, Doob's upcrossing
 estimate (also known as Doob's inequality) states that

src/ring_theory/dedekind_domain/integral_closure.lean

@@ -11,6 +11,9 @@ import ring_theory.trace
 /-!
 # Integral closure of Dedekind domains
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file shows the integral closure of a Dedekind domain (in particular, the ring of integers
 of a number field) is a Dedekind domain.
 

src/ring_theory/localization/norm.lean

@@ -11,6 +11,9 @@ import ring_theory.norm
 
 # Field/algebra norm and localization
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains results on the combination of `algebra.norm` and `is_localization`.
 
 ## Main results

src/ring_theory/norm.lean

@@ -15,6 +15,9 @@ import field_theory.galois
 /-!
 # Norm for (finite) ring extensions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Suppose we have an `R`-algebra `S` with a finite basis. For each `s : S`,
 the determinant of the linear map given by multiplying by `s` gives information
 about the roots of the minimal polynomial of `s` over `R`.

src/ring_theory/polynomial/eisenstein/is_integral.lean

@@ -10,6 +10,9 @@ import ring_theory.polynomial.cyclotomic.expand
 
 /-!
 # Eisenstein polynomials
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 In this file we gather more miscellaneous results about Eisenstein polynomials
 
 ## Main results

src/ring_theory/trace.lean

@@ -18,6 +18,9 @@ import ring_theory.power_basis
 /-!
 # Trace for (finite) ring extensions.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Suppose we have an `R`-algebra `S` with a finite basis. For each `s : S`,
 the trace of the linear map given by multiplying by `s` gives information about
 the roots of the minimal polynomial of `s` over `R`.