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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebraic_geometry.stalks` * `algebraic_geometry.structure_sheaf` * `analysis.analytic.basic` * `analysis.calculus.cont_diff_def` * `analysis.calculus.iterated_deriv` * `analysis.calculus.mean_value` * `analysis.inner_product_space.adjoint` * `analysis.inner_product_space.positive` * `analysis.normed_space.lp_equiv` * `analysis.normed_space.lp_space` * `measure_theory.constructions.pi` * `measure_theory.function.convergence_in_measure` * `measure_theory.function.locally_integrable` * `measure_theory.measure.haar.of_basis` * `probability.probability_mass_function.uniform` * `ring_theory.filtration` * `topology.algebra.valued_field` * `topology.metric_space.kuratowski`
leanprover-community · Jun 2, 2023 · 2ebc1d6 · 2ebc1d6
1 parent a166656
commit 2ebc1d6
Show file tree

Hide file tree

Showing 18 changed files with 54 additions and 0 deletions.
diff --git a/src/algebraic_geometry/stalks.lean b/src/algebraic_geometry/stalks.lean
@@ -10,6 +10,9 @@ import topology.sheaves.stalks
 /-!
 # Stalks for presheaved spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file lifts constructions of stalks and pushforwards of stalks to work with
 the category of presheafed spaces. Additionally, we prove that restriction of
 presheafed spaces does not change the stalks.

diff --git a/src/algebraic_geometry/structure_sheaf.lean b/src/algebraic_geometry/structure_sheaf.lean
@@ -13,6 +13,9 @@ import ring_theory.subring.basic
 /-!
 # The structure sheaf on `prime_spectrum R`.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the structure sheaf on `Top.of (prime_spectrum R)`, for a commutative ring `R` and prove
 basic properties about it. We define this as a subsheaf of the sheaf of dependent functions into the
 localizations, cut out by the condition that the function must be locally equal to a ratio of

diff --git a/src/analysis/analytic/basic.lean b/src/analysis/analytic/basic.lean
@@ -11,6 +11,9 @@ import topology.algebra.infinite_sum.module
 /-!
 # Analytic functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A function is analytic in one dimension around `0` if it can be written as a converging power series
 `Σ pₙ zⁿ`. This definition can be extended to any dimension (even in infinite dimension) by
 requiring that `pₙ` is a continuous `n`-multilinear map. In general, `pₙ` is not unique (in two

diff --git a/src/analysis/calculus/cont_diff_def.lean b/src/analysis/calculus/cont_diff_def.lean
@@ -12,6 +12,9 @@ import analysis.calculus.formal_multilinear_series
 /-!
 # Higher differentiability
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A function is `C^1` on a domain if it is differentiable there, and its derivative is continuous.
 By induction, it is `C^n` if it is `C^{n-1}` and its (n-1)-th derivative is `C^1` there or,
 equivalently, if it is `C^1` and its derivative is `C^{n-1}`.

diff --git a/src/analysis/calculus/iterated_deriv.lean b/src/analysis/calculus/iterated_deriv.lean
@@ -9,6 +9,9 @@ import analysis.calculus.cont_diff_def
 /-!
 # One-dimensional iterated derivatives
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define the `n`-th derivative of a function `f : 𝕜 → F` as a function
 `iterated_deriv n f : 𝕜 → F`, as well as a version on domains `iterated_deriv_within n f s : 𝕜 → F`,
 and prove their basic properties.

diff --git a/src/analysis/calculus/mean_value.lean b/src/analysis/calculus/mean_value.lean
@@ -13,6 +13,9 @@ import topology.instances.real_vector_space
 /-!
 # The mean value inequality and equalities
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove the following facts:
 
 * `convex.norm_image_sub_le_of_norm_deriv_le` : if `f` is differentiable on a convex set `s`

diff --git a/src/analysis/inner_product_space/adjoint.lean b/src/analysis/inner_product_space/adjoint.lean
@@ -10,6 +10,9 @@ import analysis.inner_product_space.pi_L2
 /-!
 # Adjoint of operators on Hilbert spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given an operator `A : E →L[𝕜] F`, where `E` and `F` are Hilbert spaces, its adjoint
 `adjoint A : F →L[𝕜] E` is the unique operator such that `⟪x, A y⟫ = ⟪adjoint A x, y⟫` for all
 `x` and `y`.

diff --git a/src/analysis/inner_product_space/positive.lean b/src/analysis/inner_product_space/positive.lean
@@ -8,6 +8,9 @@ import analysis.inner_product_space.adjoint
 /-!
 # Positive operators
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define positive operators in a Hilbert space. We follow Bourbaki's choice
 of requiring self adjointness in the definition.
 

diff --git a/src/analysis/normed_space/lp_equiv.lean b/src/analysis/normed_space/lp_equiv.lean
@@ -10,6 +10,9 @@ import topology.continuous_function.bounded
 /-!
 # Equivalences among $L^p$ spaces
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we collect a variety of equivalences among various $L^p$ spaces.  In particular,
 when `α` is a `fintype`, given `E : α → Type u` and `p : ℝ≥0∞`, there is a natural linear isometric
 equivalence `lp_pi_Lpₗᵢ : lp E p ≃ₗᵢ pi_Lp p E`. In addition, when `α` is a discrete topological

diff --git a/src/analysis/normed_space/lp_space.lean b/src/analysis/normed_space/lp_space.lean
@@ -11,6 +11,9 @@ import topology.algebra.order.liminf_limsup
 /-!
 # ℓp space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file describes properties of elements `f` of a pi-type `Π i, E i` with finite "norm",
 defined for `p:ℝ≥0∞` as the size of the support of `f` if `p=0`, `(∑' a, ‖f a‖^p) ^ (1/p)` for
 `0 < p < ∞` and `⨆ a, ‖f a‖` for `p=∞`.

diff --git a/src/measure_theory/constructions/pi.lean b/src/measure_theory/constructions/pi.lean
@@ -10,6 +10,9 @@ import topology.constructions
 /-!
 # Product measures
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define and prove properties about finite products of measures
 (and at some point, countable products of measures).
 

diff --git a/src/measure_theory/function/convergence_in_measure.lean b/src/measure_theory/function/convergence_in_measure.lean
@@ -10,6 +10,9 @@ import measure_theory.function.lp_space
 /-!
 # Convergence in measure
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define convergence in measure which is one of the many notions of convergence in probability.
 A sequence of functions `f` is said to converge in measure to some function `g`
 if for all `ε > 0`, the measure of the set `{x | ε ≤ dist (f i x) (g x)}` tends to 0 as `i`

diff --git a/src/measure_theory/function/locally_integrable.lean b/src/measure_theory/function/locally_integrable.lean
@@ -8,6 +8,9 @@ import measure_theory.integral.integrable_on
 /-!
 # Locally integrable functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A function is called *locally integrable* (`measure_theory.locally_integrable`) if it is integrable
 on a neighborhood of every point. More generally, it is *locally integrable on `s`* if it is
 locally integrable on a neighbourhood within `s` of any point of `s`.

diff --git a/src/measure_theory/measure/haar/of_basis.lean b/src/measure_theory/measure/haar/of_basis.lean
@@ -9,6 +9,9 @@ import analysis.inner_product_space.pi_L2
 /-!
 # Additive Haar measure constructed from a basis
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a basis of a finite-dimensional real vector space, we define the corresponding Lebesgue
 measure, which gives measure `1` to the parallelepiped spanned by the basis.
 

diff --git a/src/probability/probability_mass_function/uniform.lean b/src/probability/probability_mass_function/uniform.lean
@@ -8,6 +8,9 @@ import probability.probability_mass_function.constructions
 /-!
 # Uniform Probability Mass Functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines a number of uniform `pmf` distributions from various inputs,
   uniformly drawing from the corresponding object.
 

diff --git a/src/ring_theory/filtration.lean b/src/ring_theory/filtration.lean
@@ -14,6 +14,9 @@ import order.hom.lattice
 
 # `I`-filtrations of modules
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains the definitions and basic results around (stable) `I`-filtrations of modules.
 
 ## Main results

diff --git a/src/topology/algebra/valued_field.lean b/src/topology/algebra/valued_field.lean
@@ -11,6 +11,9 @@ import topology.algebra.uniform_field
 /-!
 # Valued fields and their completions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we study the topology of a field `K` endowed with a valuation (in our application
 to adic spaces, `K` will be the valuation field associated to some valuation on a ring, defined in
 valuation.basic).

diff --git a/src/topology/metric_space/kuratowski.lean b/src/topology/metric_space/kuratowski.lean
@@ -9,6 +9,9 @@ import topology.sets.compacts
 /-!
 # The Kuratowski embedding
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Any separable metric space can be embedded isometrically in `ℓ^∞(ℝ)`.
 -/