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

Regenerated from the [port status wiki page](https://github.com/leanprover-community/mathlib/wiki/mathlib4-port-status). Relates to the following files: * `algebra.lie.classical` * `analysis.calculus.bump_function_inner` * `analysis.calculus.monotone` * `analysis.calculus.parametric_interval_integral` * `analysis.normed_space.quaternion_exponential` * `analysis.special_functions.trigonometric.arctan_deriv` * `analysis.special_functions.trigonometric.bounds` * `category_theory.bicategory.coherence_tactic` * `category_theory.monoidal.Mon_` * `category_theory.monoidal.coherence` * `category_theory.monoidal.subcategory` * `category_theory.sites.compatible_plus` * `category_theory.sites.types` * `data.json` * `data.real.pi.leibniz` * `geometry.euclidean.angle.unoriented.right_angle` * `linear_algebra.tensor_algebra.basic` * `measure_theory.covering.density_theorem` * `measure_theory.covering.differentiation` * `measure_theory.covering.liminf_limsup` * `measure_theory.covering.one_dim` * `measure_theory.decomposition.lebesgue` * `measure_theory.decomposition.radon_nikodym` * `measure_theory.function.continuous_map_dense` * `measure_theory.function.l2_space` * `measure_theory.function.special_functions.arctan` * `measure_theory.integral.interval_average` * `measure_theory.integral.interval_integral` * `measure_theory.integral.peak_function` * `measure_theory.measure.finite_measure` * `measure_theory.measure.haar.quotient` * `measure_theory.measure.probability_measure` * `probability.integration` * `ring_theory.class_group` * `ring_theory.roots_of_unity.basic` * `ring_theory.roots_of_unity.complex` * `topology.order.hom.esakia`
leanprover-community · Jun 8, 2023 · 7e5137f · 7e5137f
1 parent b915e93
commit 7e5137f
Show file tree

Hide file tree

Showing 37 changed files with 112 additions and 1 deletion.
diff --git a/src/algebra/lie/classical.lean b/src/algebra/lie/classical.lean
@@ -14,6 +14,9 @@ import linear_algebra.symplectic_group
 /-!
 # Classical Lie algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file is the place to find definitions and basic properties of the classical Lie algebras:
   * Aₗ = sl(l+1)
   * Bₗ ≃ so(l+1, l) ≃ so(2l+1)

diff --git a/src/analysis/calculus/bump_function_inner.lean b/src/analysis/calculus/bump_function_inner.lean
@@ -13,6 +13,9 @@ import measure_theory.integral.set_integral
 /-!
 # Infinitely smooth bump function
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we construct several infinitely smooth functions with properties that an analytic
 function cannot have:
 

diff --git a/src/analysis/calculus/monotone.lean b/src/analysis/calculus/monotone.lean
@@ -10,6 +10,9 @@ import order.monotone.extension
 /-!
 # Differentiability of monotone functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We show that a monotone function `f : ℝ → ℝ` is differentiable almost everywhere, in
 `monotone.ae_differentiable_at`. (We also give a version for a function monotone on a set, in
 `monotone_on.ae_differentiable_within_at`.)

diff --git a/src/analysis/calculus/parametric_interval_integral.lean b/src/analysis/calculus/parametric_interval_integral.lean
@@ -9,6 +9,9 @@ import measure_theory.integral.interval_integral
 /-!
 # Derivatives of interval integrals depending on parameters
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we restate theorems about derivatives of integrals depending on parameters for interval
 integrals.  -/
 

diff --git a/src/analysis/normed_space/quaternion_exponential.lean b/src/analysis/normed_space/quaternion_exponential.lean
@@ -10,6 +10,9 @@ import analysis.special_functions.trigonometric.series
 /-!
 # Lemmas about `exp` on `quaternion`s
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file contains results about `exp` on `quaternion ℝ`.
 
 ## Main results

diff --git a/src/analysis/special_functions/trigonometric/arctan_deriv.lean b/src/analysis/special_functions/trigonometric/arctan_deriv.lean
@@ -9,6 +9,9 @@ import analysis.special_functions.trigonometric.complex_deriv
 /-!
 # Derivatives of the `tan` and `arctan` functions.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Continuity and derivatives of the tangent and arctangent functions.
 -/
 

diff --git a/src/analysis/special_functions/trigonometric/bounds.lean b/src/analysis/special_functions/trigonometric/bounds.lean
@@ -8,6 +8,9 @@ import analysis.special_functions.trigonometric.arctan_deriv
 /-!
 # Polynomial bounds for trigonometric functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 ## Main statements
 
 This file contains upper and lower bounds for real trigonometric functions in terms

diff --git a/src/category_theory/bicategory/coherence_tactic.lean b/src/category_theory/bicategory/coherence_tactic.lean
@@ -8,6 +8,9 @@ import category_theory.bicategory.coherence
 /-!
 # A `coherence` tactic for bicategories, and `⊗≫` (composition up to associators)
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We provide a `coherence` tactic,
 which proves that any two 2-morphisms (with the same source and target)
 in a bicategory which are built out of associators and unitors

diff --git a/src/category_theory/monoidal/Mon_.lean b/src/category_theory/monoidal/Mon_.lean
@@ -12,6 +12,9 @@ import algebra.punit_instances
 /-!
 # The category of monoids in a monoidal category.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define monoids in a monoidal category `C` and show that the category of monoids is equivalent to
 the category of lax monoidal functors from the unit monoidal category to `C`.  We also show that if
 `C` is braided, then the category of monoids is naturally monoidal.

diff --git a/src/category_theory/monoidal/coherence.lean b/src/category_theory/monoidal/coherence.lean
@@ -9,6 +9,9 @@ import category_theory.bicategory.coherence_tactic
 /-!
 # A `coherence` tactic for monoidal categories, and `⊗≫` (composition up to associators)
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We provide a `coherence` tactic,
 which proves equations where the two sides differ by replacing
 strings of monoidal structural morphisms with other such strings.

diff --git a/src/category_theory/monoidal/subcategory.lean b/src/category_theory/monoidal/subcategory.lean
@@ -12,6 +12,9 @@ import category_theory.closed.monoidal
 /-!
 # Full monoidal subcategories
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a monidal category `C` and a monoidal predicate on `C`, that is a function `P : C → Prop`
 closed under `𝟙_` and `⊗`, we can put a monoidal structure on `{X : C // P X}` (the category
 structure is defined in `category_theory.full_subcategory`).

diff --git a/src/category_theory/sites/compatible_plus.lean b/src/category_theory/sites/compatible_plus.lean
@@ -7,6 +7,9 @@ import category_theory.sites.whiskering
 import category_theory.sites.plus
 
 /-!
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 
 In this file, we prove that the plus functor is compatible with functors which
 preserve the correct limits and colimits.

diff --git a/src/category_theory/sites/types.lean b/src/category_theory/sites/types.lean
@@ -9,6 +9,9 @@ import category_theory.sites.canonical
 /-!
 # Grothendieck Topology and Sheaves on the Category of Types
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define a Grothendieck topology on the category of types,
 and construct the canonical functor that sends a type to a sheaf over
 the category of types, and make this an equivalence of categories.

diff --git a/src/data/json.lean b/src/data/json.lean
@@ -8,6 +8,9 @@ import tactic.core
 /-!
 # Json serialization typeclass
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file provides helpers for serializing primitive types to json.
 
 `@[derive non_null_json_serializable]` will make any structure json serializable; for instance,

diff --git a/src/data/real/pi/leibniz.lean b/src/data/real/pi/leibniz.lean
@@ -5,7 +5,10 @@ Authors: Benjamin Davidson
 -/
 import analysis.special_functions.trigonometric.arctan_deriv
 
-/-! ### Leibniz's Series for Pi -/
+/-! ### Leibniz's Series for Pi 
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.-/
 
 namespace real
 

diff --git a/src/geometry/euclidean/angle/unoriented/right_angle.lean b/src/geometry/euclidean/angle/unoriented/right_angle.lean
@@ -9,6 +9,9 @@ import geometry.euclidean.angle.unoriented.affine
 /-!
 # Right-angled triangles
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves basic geometrical results about distances and angles in (possibly degenerate)
 right-angled triangles in real inner product spaces and Euclidean affine spaces.
 

diff --git a/src/linear_algebra/tensor_algebra/basic.lean b/src/linear_algebra/tensor_algebra/basic.lean
@@ -12,6 +12,9 @@ import linear_algebra.multilinear.basic
 /-!
 # Tensor Algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Given a commutative semiring `R`, and an `R`-module `M`, we construct the tensor algebra of `M`.
 This is the free `R`-algebra generated (`R`-linearly) by the module `M`.
 

diff --git a/src/measure_theory/covering/density_theorem.lean b/src/measure_theory/covering/density_theorem.lean
@@ -10,6 +10,9 @@ import measure_theory.covering.differentiation
 /-!
 # Uniformly locally doubling measures and Lebesgue's density theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Lebesgue's density theorem states that given a set `S` in a sigma compact metric space with
 locally-finite uniformly locally doubling measure `μ` then for almost all points `x` in `S`, for any
 sequence of closed balls `B₀, B₁, B₂, ...` containing `x`, the limit `μ (S ∩ Bⱼ) / μ (Bⱼ) → 1` as

diff --git a/src/measure_theory/covering/differentiation.lean b/src/measure_theory/covering/differentiation.lean
@@ -13,6 +13,9 @@ import measure_theory.decomposition.lebesgue
 /-!
 # Differentiation of measures
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 On a second countable metric space with a measure `μ`, consider a Vitali family (i.e., for each `x`
 one has a family of sets shrinking to `x`, with a good behavior with respect to covering theorems).
 Consider also another measure `ρ`. Then, for almost every `x`, the ratio `ρ a / μ a` converges when

diff --git a/src/measure_theory/covering/liminf_limsup.lean b/src/measure_theory/covering/liminf_limsup.lean
@@ -8,6 +8,9 @@ import measure_theory.covering.density_theorem
 /-!
 # Liminf, limsup, and uniformly locally doubling measures.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file is a place to collect lemmas about liminf and limsup for subsets of a metric space
 carrying a uniformly locally doubling measure.
 

diff --git a/src/measure_theory/covering/one_dim.lean b/src/measure_theory/covering/one_dim.lean
@@ -9,6 +9,9 @@ import measure_theory.measure.lebesgue.eq_haar
 /-!
 # Covering theorems for Lebesgue measure in one dimension
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We have a general theory of covering theorems for doubling measures, developed notably
 in `density_theorems.lean`. In this file, we expand the API for this theory in one dimension,
 by showing that intervals belong to the relevant Vitali family.

diff --git a/src/measure_theory/decomposition/lebesgue.lean b/src/measure_theory/decomposition/lebesgue.lean
@@ -12,6 +12,9 @@ import measure_theory.function.ae_eq_of_integral
 /-!
 # Lebesgue decomposition
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves the Lebesgue decomposition theorem. The Lebesgue decomposition theorem states that,
 given two σ-finite measures `μ` and `ν`, there exists a σ-finite measure `ξ` and a measurable
 function `f` such that `μ = ξ + fν` and `ξ` is mutually singular with respect to `ν`.

diff --git a/src/measure_theory/decomposition/radon_nikodym.lean b/src/measure_theory/decomposition/radon_nikodym.lean
@@ -8,6 +8,9 @@ import measure_theory.decomposition.lebesgue
 /-!
 # Radon-Nikodym theorem
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves the Radon-Nikodym theorem. The Radon-Nikodym theorem states that, given measures
 `μ, ν`, if `have_lebesgue_decomposition μ ν`, then `μ` is absolutely continuous with respect to
 `ν` if and only if there exists a measurable function `f : α → ℝ≥0∞` such that `μ = fν`.

diff --git a/src/measure_theory/function/continuous_map_dense.lean b/src/measure_theory/function/continuous_map_dense.lean
@@ -12,6 +12,9 @@ import measure_theory.integral.bochner
 /-!
 # Approximation in Lᵖ by continuous functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file proves that bounded continuous functions are dense in `Lp E p μ`, for `p < ∞`, if the
 domain `α` of the functions is a normal topological space and the measure `μ` is weakly regular.
 It also proves the same results for approximation by continuous functions with compact support

diff --git a/src/measure_theory/function/l2_space.lean b/src/measure_theory/function/l2_space.lean
@@ -9,6 +9,9 @@ import measure_theory.integral.set_integral
 
 /-! # `L^2` space
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 If `E` is an inner product space over `𝕜` (`ℝ` or `ℂ`), then `Lp E 2 μ` (defined in `lp_space.lean`)
 is also an inner product space, with inner product defined as `inner f g = ∫ a, ⟪f a, g a⟫ ∂μ`.
 

diff --git a/src/measure_theory/function/special_functions/arctan.lean b/src/measure_theory/function/special_functions/arctan.lean
@@ -10,6 +10,9 @@ import measure_theory.constructions.borel_space.basic
 /-!
 # Measurability of arctan
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 -/
 
 namespace real

diff --git a/src/measure_theory/integral/interval_average.lean b/src/measure_theory/integral/interval_average.lean
@@ -9,6 +9,9 @@ import measure_theory.integral.average
 /-!
 # Integral average over an interval
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we introduce notation `⨍ x in a..b, f x` for the average `⨍ x in Ι a b, f x` of `f`
 over the interval `Ι a b = set.Ioc (min a b) (max a b)` w.r.t. the Lebesgue measure, then prove
 formulas for this average:

diff --git a/src/measure_theory/integral/interval_integral.lean b/src/measure_theory/integral/interval_integral.lean
@@ -10,6 +10,9 @@ import measure_theory.measure.lebesgue.basic
 /-!
 # Integral over an interval
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we define `∫ x in a..b, f x ∂μ` to be `∫ x in Ioc a b, f x ∂μ` if `a ≤ b` and
 `-∫ x in Ioc b a, f x ∂μ` if `b ≤ a`.
 

diff --git a/src/measure_theory/integral/peak_function.lean b/src/measure_theory/integral/peak_function.lean
@@ -9,6 +9,9 @@ import measure_theory.function.locally_integrable
 /-!
 # Integrals against peak functions
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A sequence of peak functions is a sequence of functions with average one concentrating around
 a point `x₀`. Given such a sequence `φₙ`, then `∫ φₙ g` tends to `g x₀` in many situations, with
 a whole zoo of possible assumptions on `φₙ` and `g`. This file is devoted to such results.

diff --git a/src/measure_theory/measure/finite_measure.lean b/src/measure_theory/measure/finite_measure.lean
@@ -10,6 +10,9 @@ import measure_theory.integral.bochner
 /-!
 # Finite measures
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the type of finite measures on a given measurable space. When the underlying
 space has a topology and the measurable space structure (sigma algebra) is finer than the Borel
 sigma algebra, then the type of finite measures is equipped with the topology of weak convergence

diff --git a/src/measure_theory/measure/haar/quotient.lean b/src/measure_theory/measure/haar/quotient.lean
@@ -11,6 +11,9 @@ import algebra.group.opposite
 /-!
 # Haar quotient measure
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file, we consider properties of fundamental domains and measures for the action of a
 subgroup of a group `G` on `G` itself.
 

diff --git a/src/measure_theory/measure/probability_measure.lean b/src/measure_theory/measure/probability_measure.lean
@@ -9,6 +9,9 @@ import measure_theory.integral.average
 /-!
 # Probability measures
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the type of probability measures on a given measurable space. When the underlying
 space has a topology and the measurable space structure (sigma algebra) is finer than the Borel
 sigma algebra, then the type of probability measures is equipped with the topology of convergence

diff --git a/src/probability/integration.lean b/src/probability/integration.lean
@@ -9,6 +9,9 @@ import probability.independence.basic
 /-!
 # Integration in Probability Theory
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Integration results for independent random variables. Specifically, for two
 independent random variables X and Y over the extended non-negative
 reals, `E[X * Y] = E[X] * E[Y]`, and similar results.

diff --git a/src/ring_theory/class_group.lean b/src/ring_theory/class_group.lean
@@ -10,6 +10,9 @@ import ring_theory.dedekind_domain.ideal
 /-!
 # The ideal class group
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the ideal class group `class_group R` of fractional ideals of `R`
 inside its field of fractions.
 

diff --git a/src/ring_theory/roots_of_unity/basic.lean b/src/ring_theory/roots_of_unity/basic.lean
@@ -18,6 +18,9 @@ import tactic.zify
 /-!
 # Roots of unity and primitive roots of unity
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 We define roots of unity in the context of an arbitrary commutative monoid,
 as a subgroup of the group of units. We also define a predicate `is_primitive_root` on commutative
 monoids, expressing that an element is a primitive root of unity.

diff --git a/src/ring_theory/roots_of_unity/complex.lean b/src/ring_theory/roots_of_unity/complex.lean
@@ -9,6 +9,9 @@ import ring_theory.roots_of_unity.basic
 /-!
 # Complex roots of unity
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we show that the `n`-th complex roots of unity
 are exactly the complex numbers `e ^ (2 * real.pi * complex.I * (i / n))` for `i ∈ finset.range n`.
 

diff --git a/src/topology/order/hom/esakia.lean b/src/topology/order/hom/esakia.lean
@@ -9,6 +9,9 @@ import topology.order.hom.basic
 /-!
 # Esakia morphisms
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines pseudo-epimorphisms and Esakia morphisms.
 
 We use the `fun_like` design, so each type of morphisms has a companion typeclass which is meant to