WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Uniform convergence

Revision #1648 → #2147 · back to history

modifiedUniform convergence (informal)a451c210f517
FieldFrom #1648To #2147
mathlib.decl—TendstoUniformly
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.UniformSpace.UniformConvergence
note—`TendstoUniformly F f p` captures the lead's informal notion of a sequence/filter of functions converging uniformly to a limit.
status—formalized
modifiedUniform convergence1162d5c9ccad
FieldFrom #1648To #2147
mathlib.decl—TendstoUniformlyOn
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.UniformSpace.UniformConvergence
note—Uniform convergence on a set is `TendstoUniformlyOn F f p s`, the on-set version of the article's ε–N definition.
status—formalized
modifiedCauchy criterion for uniform convergence999a66f593f9
FieldFrom #1648To #2147
mathlib.decl—UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.UniformSpace.UniformConvergence
note—The equivalence is captured by `TendstoUniformlyOn.uniformCauchySeqOn` together with `UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto`.
status—formalized
modifiedUniform (supremum) metric characterization8f8d8ee7fd69
FieldFrom #1648To #2147
mathlib.decl—Metric.tendstoUniformlyOn_iff
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.MetricSpace.Pseudo.Basic
note—`Metric.tendstoUniformlyOn_iff` restates uniform convergence using the metric (sup) characterization on a metric target.
status—formalized
modifiedLocally uniformly convergentc79965136075
FieldFrom #1648To #2147
mathlib.decl—TendstoLocallyUniformly
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.UniformSpace.LocallyUniformConvergence
note—Local uniform convergence is `TendstoLocallyUniformly` (with the on-set variant `TendstoLocallyUniformlyOn`).
status—formalized
modifiedUniform convergence into a metric spacee38eca57182d
FieldFrom #1648To #2147
mathlib.decl—TendstoUniformly
mathlib.match_kind—generalization
mathlib.module—Mathlib.Topology.UniformSpace.UniformConvergence
note—Mathlib defines `TendstoUniformly` in a `UniformSpace` codomain, which subsumes the metric-space generalization stated in the article.
status—formalized
modifiedUniform convergence of nets into a uniform space7c905323c2f9
FieldFrom #1648To #2147
mathlib.decl—TendstoUniformly
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.UniformSpace.UniformConvergence
note—`TendstoUniformly F f p` is filter-indexed (nets via their tail filter) into a `UniformSpace`, the most general form described.
status—formalized
modifiedUniform convergence (hyperreal)025a6c41ea09
FieldFrom #1648To #2147
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No nonstandard/hyperreal characterization of uniform convergence was found in Mathlib.
status—not_formalized
modifiedBasic example: x^n vs x^n on [0,1]7281552eb8a3
FieldFrom #1648To #2147
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No worked example of the sequence x^n on [0,1] as a uniform-convergence illustration is recorded in Mathlib.
status—not_formalized
modifiedPointwise but not uniformly convergent sequenced370beec15cb
FieldFrom #1648To #2147
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No formalized counterexample sequence demonstrating pointwise but not uniform convergence was found in Mathlib.
status—not_formalized
modifiedUniform convergence of exponential series205b6da70a1e
FieldFrom #1648To #2147
mathlib.decl—TendstoUniformlyOn.comp_cexp
mathlib.match_kind—invocation
mathlib.module—Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
note—No direct lemma states the exp power series converges uniformly on bounded sets; only auxiliary results like `TendstoUniformlyOn.comp_cexp` exist (the Weierstrass M-test gives it as an invocation).
status—partial
modifiedWeierstrass M-test6546c7045759
FieldFrom #1648To #2147
mathlib.decl—tendstoUniformlyOn_tsum
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Normed.Group.FunctionSeries
note—`tendstoUniformlyOn_tsum` is the Weierstrass M-test: a summable majorant `u` with ‖f n x‖ ≤ u n forces uniform convergence of the partial sums.
status—formalized
modifiedUniform convergence implies local uniform convergence8bff702f0e2c
FieldFrom #1648To #2147
mathlib.decl—TendstoUniformly.tendstoLocallyUniformly
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.UniformSpace.LocallyUniformConvergence
note—`TendstoUniformly.tendstoLocallyUniformly` is exactly the implication uniform ⇒ locally uniform.
status—formalized
modifiedLocal uniform convergence implies compact convergence08e7ea54aff3
FieldFrom #1648To #2147
mathlib.decl—tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact
mathlib.match_kind—special_case
mathlib.module—Mathlib.Topology.UniformSpace.LocallyUniformConvergence
note—The forward direction of `tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact` (and `tendstoLocallyUniformly_iff_forall_isCompact` on locally compact spaces) gives uniform convergence on each compact set.
status—formalized
modifiedLocal uniform and compact convergence agree on locally compact spaces608886e21f84
FieldFrom #1648To #2147
mathlib.decl—tendstoLocallyUniformly_iff_forall_isCompact
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.UniformSpace.LocallyUniformConvergence
note—`tendstoLocallyUniformly_iff_forall_isCompact` proves the equivalence under `LocallyCompactSpace`.
status—formalized
modifiedUniform convergence iff uniformly Cauchy (complete image)862cbd50d50b
FieldFrom #1648To #2147
mathlib.decl—UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.UniformSpace.UniformConvergence
note—Together with `TendstoUniformlyOn.uniformCauchySeqOn`, this gives the uniform-Cauchy ⇔ uniformly-convergent equivalence.
status—formalized
modifiedDini's theoremc4620b77a0f2
FieldFrom #1648To #2147
mathlib.decl—Monotone.tendstoUniformlyOn_of_forall_tendsto
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.UniformSpace.Dini
note—`Monotone.tendstoUniformlyOn_of_forall_tendsto` is Dini's theorem: monotone pointwise convergence to a continuous limit on a compact set is uniform.
status—formalized
modifiedEquicontinuous pointwise-convergent sequence converges uniformly8a9a69eefee3
FieldFrom #1648To #2147
mathlib.decl—Equicontinuous.tendsto_uniformFun_iff_pi
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.UniformSpace.Ascoli
note—`Equicontinuous.tendsto_uniformFun_iff_pi` (and `EquicontinuousOn.tendsto_uniformOnFun_iff_pi`) gives uniform = pointwise convergence for equicontinuous families on a compact (resp. compact-covered) space.
status—formalized
modifiedUniform limit theoremdbadc716fcd8
FieldFrom #1648To #2147
anchor.section—To continuity
anchor.snippet—Uniform limit theorem — Suppose
anchor.typetheorem_box—
anchor.valueUniform limit theorem — Suppose [MATH] i—
mathlib.decl—TendstoUniformlyOn.continuousOn
mathlib.match_kind—exact
mathlib.module—Mathlib.Topology.UniformSpace.UniformApproximation
note—`TendstoUniformlyOn.continuousOn` (and `TendstoUniformly.continuous`) prove that a uniform limit of continuous functions is continuous.
provenanceai-agent1ai-moderated
status—formalized
modifiedUniform convergence and differentiation6705ee4500e1
FieldFrom #1648To #2147
mathlib.decl—hasFDerivAt_of_tendstoUniformly
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Calculus.UniformLimitsDeriv
note—`hasFDerivAt_of_tendstoUniformly` (and `hasDerivAt_of_tendstoUniformly`) give the article's differentiation-under-uniform-limit theorem.
status—formalized
modifiedUniform convergence and Riemann integration1ef6ebaad468
FieldFrom #1648To #2147
mathlib.decl—TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Integral.DominatedConvergence
note—`TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn` shows uniform convergence on `[a,b]` lets one swap limit and integral.
status—formalized
modifiedUniform limit of analytic functions is analyticd7587a7d7f36
FieldFrom #1648To #2147
mathlib.decl—TendstoLocallyUniformlyOn.differentiableOn
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Complex.LocallyUniformLimit
note—`TendstoLocallyUniformlyOn.differentiableOn` formalizes the result that a locally uniform limit of holomorphic (= complex-analytic) functions on an open set is holomorphic.
status—formalized
modifiedPointwise, uniform, and absolute convergence of seriesb269ebe278b0
FieldFrom #1648To #2147
mathlib.decl—HasSumUniformlyOn
mathlib.match_kind—generalization
mathlib.module—Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
note—Mathlib defines `Summable`/`HasSum` for pointwise and `HasSumUniformlyOn` for uniform series convergence, but bundles them via filters rather than the article's three-way pointwise/uniform/absolute definition.
status—partial
modifiedUniformly convergent series of continuous functionsfb8c5409886e
FieldFrom #1648To #2147
mathlib.decl—TendstoUniformlyOn.continuousOn
mathlib.match_kind—invocation
mathlib.module—Mathlib.Topology.UniformSpace.UniformApproximation
note—Continuity of the sum follows by composing `tendstoUniformlyOn_tsum` with `TendstoUniformlyOn.continuousOn`; no single dedicated lemma was found.
status—partial
modifiedTerm-by-term integration of uniformly convergent series693732e0db08
FieldFrom #1648To #2147
mathlib.decl—TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOn
mathlib.match_kind—invocation
mathlib.module—Mathlib.MeasureTheory.Integral.DominatedConvergence
note—Mathlib has uniform-limit interchange with the integral but no single named term-by-term-integration-of-a-series result; it must be assembled via `tendstoUniformlyOn_tsum` plus the integral swap.
status—partial
modifiedC[0,1] with supremum norm is a Banach space329ea2516644
FieldFrom #1648To #2147
mathlib.decl—BoundedContinuousFunction.instCompleteSpace
mathlib.match_kind—special_case
mathlib.module—Mathlib.Topology.ContinuousMap.Bounded.Basic
note—Specializing `BoundedContinuousFunction.instCompleteSpace` to `α = [0,1]`, `β = ℝ` or `ℂ` gives that C[0,1] with the sup norm is a Banach space.
status—formalized
modifiedCompleteness of C[0,1]a2fb24296a08
FieldFrom #1648To #2147
mathlib.decl—BoundedContinuousFunction.instCompleteSpace
mathlib.match_kind—special_case
mathlib.module—Mathlib.Topology.ContinuousMap.Bounded.Basic
note—Completeness of C[0,1] specializes `BoundedContinuousFunction.instCompleteSpace`, which itself requires only completeness of the codomain.
status—formalized
modifiedC(X) is a Banach space for compact Hausdorff Xe687c19a7f5d
FieldFrom #1648To #2147
mathlib.decl—BoundedContinuousFunction.instCompleteSpace
mathlib.match_kind—special_case
mathlib.module—Mathlib.Topology.ContinuousMap.Bounded.Basic
note—For compact X, continuous functions are automatically bounded, so `BoundedContinuousFunction.instCompleteSpace` gives the Banach-space structure on C(X).
status—formalized
modifiedBounded functions with sup norm form a Banach spaceea53adce13b6
FieldFrom #1648To #2147
mathlib.decl—UniformOnFun.instCompleteSpace
mathlib.match_kind—generalization
mathlib.module—Mathlib.Topology.UniformSpace.UniformConvergenceTopology
note—`UniformOnFun.instCompleteSpace` (and `BoundedContinuousFunction.instCompleteSpace` for the continuous bounded sub-Banach space) covers uniform completeness, but Mathlib does not single out the space of *all* bounded functions with the sup norm as a named Banach space.
status—partial
modifiedL^infinity and its relation to uniform convergence2bc93e4844ec
FieldFrom #1648To #2147
mathlib.decl—MeasureTheory.Lp
mathlib.match_kind—generalization
mathlib.module—Mathlib.MeasureTheory.Function.LpSpace.Basic
note—`MeasureTheory.Lp f ⊤ μ` is the L^∞ space of essentially bounded measurable functions; the link to uniform convergence (norm = essential sup) is implicit in the L^∞ norm definition.
status—formalized
modifiedAlmost uniform convergence7ba7a0f9a766
FieldFrom #1648To #2147
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has no named definition of `almost uniform convergence`; only Egorov-style statements that produce the conclusion are present.
status—not_formalized
modifiedEgorov's theorem9970088b7a8f
FieldFrom #1648To #2147
mathlib.decl—MeasureTheory.tendstoUniformlyOn_of_ae_tendsto
mathlib.match_kind—exact
mathlib.module—Mathlib.MeasureTheory.Function.Egorov
note—`MeasureTheory.tendstoUniformlyOn_of_ae_tendsto` is Egorov's theorem on finite measure sets.
status—formalized
modifiedAlmost uniform convergence implies a.e. convergence and convergence in measure3f3766791a76
FieldFrom #1648To #2147
mathlib.decl—MeasureTheory.tendstoInMeasure_of_tendsto_ae_of_measurable_edist
mathlib.match_kind—invocation
mathlib.module—Mathlib.MeasureTheory.Function.ConvergenceInMeasure
note—Without a named `almost uniform convergence`, the two implications are not packaged; Mathlib does have a.e. ⇒ in-measure (`MeasureTheory.tendstoInMeasure_of_tendsto_ae_of_measurable_edist`) which gives the harder half once the definition is unfolded.
status—partial
addedUniform metric on bounded functionsb6022e7cb326
addedCompact-open topology on C(Y) for σ-compact locally compact Hausdorff Y13e366117959