Abel's theorem to Rademacher's theorem

TheoremAbel's theorem#

Mathlib records this with 2 declarations.

Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzCone: Abel's limit theorem. Given a power series converging at 1, the corresponding function is continuous at 1 when approaching 1 within any fixed Stolz cone.

Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzCone {f : ℕ → ℂ} {l : ℂ}
  (h : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l)) {s : ℝ}
  (hs : 0 < s) :
  Filter.Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (nhdsWithin 1 (Complex.stolzCone s)) (nhds l)

Real.tendsto_tsum_powerSeries_nhdsWithin_lt: Abel's limit theorem. Given a real power series converging at 1, the corresponding function is continuous at 1 when approaching 1 from the left.

Real.tendsto_tsum_powerSeries_nhdsWithin_lt {f : ℕ → ℝ} {l : ℝ}
  (h : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l)) :
  Filter.Tendsto (fun x => ∑' (n : ℕ), f n * x ^ n) (nhdsWithin 1 (Set.Iio 1)) (nhds l)
Sources
MathlibComplex.tendsto_tsum_powerSeries_nhdsWithin_stolzCone · Real.tendsto_tsum_powerSeries_nhdsWithin_lt
Uses 14 · Used by 1
Statement usesComplex number · Infinite sum · Metric space
Proof usesAssociative algebra over a commutative ring · Characteristic zero · Completeness of R · Continuous linear map · Field \(\C\) of complex numbers · Hausdorff space · Limits of sequences · Normed vector space over a normed field · Ring structure \(\Z\) · The Triangle Inequality · Topological ring
Used byLeibniz’s Series for Pi

TheoremBesicovitch covering theorem#

The measurable Besicovitch covering theorem.

Assume that, for any x in a set s, one is given a set of admissible closed balls centered at x, with arbitrarily small radii. Then there exists a disjoint covering of almost all s by admissible closed balls centered at some points of s. We can even require that the radius at x is bounded by a given function R x. (Take R = 1 if you don't need this additional feature).

This version requires the underlying measure to be sigma-finite, and the space to have the Besicovitch covering property (which is satisfied for instance by normed real vector spaces).

Besicovitch.exists_disjoint_closedBall_covering_ae.{u_1} {α : Type u_1} [MetricSpace α]
  [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α]
  [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (f : α → Set ℝ)
  (s : Set α) (hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) (R : α → ℝ)
  (hR : ∀ x ∈ s, 0 < R x) :
  ∃ t r,
    t.Countable ∧
      t ⊆ s ∧
        (∀ x ∈ t, r x ∈ f x ∩ Set.Ioo 0 (R x)) ∧
          μ (s \ ⋃ x ∈ t, Metric.closedBall x (r x)) = 0 ∧
            t.PairwiseDisjoint fun x => Metric.closedBall x (r x)
Sources
MathlibBesicovitch.exists_disjoint_closedBall_covering_ae
Uses 8 · Used by 1
Statement usesCarathéodory's theorem (measure theory) · Metric space · Positive measure
Proof usesCharacteristic zero · Closure · Order topology · Ordinal · Topology of a metric space
Used byChange of variables formula

TheoremBolzano–Weierstrass theorem (1000+ theorems)#

Mathlib records this with 2 declarations.

tendsto_subseq_of_frequently_bounded: A version of Bolzano-Weierstrass: in a proper metric space (e.g. \(ℝ^n\)), every bounded sequence has a converging subsequence. This version assumes only that the sequence is frequently in some bounded set.

tendsto_subseq_of_frequently_bounded.{u_1} {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X]
  {s : Set X} (hs : Bornology.IsBounded s) {x : ℕ → X} (hx : ∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s) :
  ∃ a ∈ closure s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)

tendsto_subseq_of_bounded: A version of Bolzano-Weierstrass: in a proper metric space (e.g. \(ℝ^n\)), every bounded sequence has a converging subsequence.

tendsto_subseq_of_bounded.{u_1} {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] {s : Set X}
  (hs : Bornology.IsBounded s) {x : ℕ → X} (hx : ∀ (n : ℕ), x n ∈ s) :
  ∃ a ∈ closure s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
Sources
Mathlibtendsto_subseq_of_frequently_bounded · tendsto_subseq_of_bounded
Uses 5 · Used by 1
Statement usesBornology · Closure · Compactness in terms of filters · Order
Proof usesOrdered ring
Used byBolzano-Weierstrass theorem (Topology of R)

TheoremCantor's intersection theorem#

Cantor's intersection theorem for sInter: the intersection of a directed family of nonempty compact closed sets is nonempty.

IsCompact.nonempty_sInter_of_directed_nonempty_isCompact_isClosed.{u} {X : Type u}
  [TopologicalSpace X] {S : Set (Set X)} [hS : Nonempty ↑S]
  (hSd : DirectedOn (fun x1 x2 => x1 ⊇ x2) S) (hSn : ∀ U ∈ S, U.Nonempty)
  (hSc : ∀ U ∈ S, IsCompact U) (hScl : ∀ U ∈ S, IsClosed U) : (⋂₀ S).Nonempty
Sources
MathlibIsCompact.nonempty_sInter_of_directed_nonempty_isCompact_isClosed
Uses 1
Statement usesCompactness in terms of filters

TheoremDarboux's theorem (analysis)#

Mathlib records this with 10 declarations.

exists_hasDerivWithinAt_eq_of_gt_of_lt: Darboux's theorem: if a ≤ b and f' a < m < f' b, then f' c = m for some c ∈ (a, b).

exists_hasDerivWithinAt_eq_of_gt_of_lt {a b : ℝ} {f f' : ℝ → ℝ} (hab : a ≤ b)
  (hf : ∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) {m : ℝ} (hma : f' a < m)
  (hmb : m < f' b) : m ∈ f' '' Set.Ioo a b

exists_hasDerivWithinAt_eq_of_lt_of_gt: Darboux's theorem: if a ≤ b and f' b < m < f' a, then f' c = m for some c ∈ (a, b).

exists_hasDerivWithinAt_eq_of_lt_of_gt {a b : ℝ} {f f' : ℝ → ℝ} (hab : a ≤ b)
  (hf : ∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) {m : ℝ} (hma : m < f' a)
  (hmb : f' b < m) : m ∈ f' '' Set.Ioo a b

Set.OrdConnected.image_hasDerivWithinAt: Darboux's theorem: the image of a Set.OrdConnected set under f' is a Set.OrdConnected set, HasDerivWithinAt version.

Set.OrdConnected.image_hasDerivWithinAt {f f' : ℝ → ℝ} {s : Set ℝ} (hs : s.OrdConnected)
  (hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) : (f' '' s).OrdConnected

Set.OrdConnected.image_derivWithin: Darboux's theorem: the image of a Set.OrdConnected set under f' is a Set.OrdConnected set, derivWithin version.

Set.OrdConnected.image_derivWithin {f : ℝ → ℝ} {s : Set ℝ} (hs : s.OrdConnected)
  (hf : DifferentiableOn ℝ f s) : (derivWithin f s '' s).OrdConnected

Set.OrdConnected.image_deriv: Darboux's theorem: the image of a Set.OrdConnected set under f' is a Set.OrdConnected set, deriv version.

Set.OrdConnected.image_deriv {f : ℝ → ℝ} {s : Set ℝ} (hs : s.OrdConnected)
  (hf : ∀ x ∈ s, DifferentiableAt ℝ f x) : (deriv f '' s).OrdConnected

Convex.image_hasDerivWithinAt: Darboux's theorem: the image of a convex set under f' is a convex set, HasDerivWithinAt version.

Convex.image_hasDerivWithinAt {f f' : ℝ → ℝ} {s : Set ℝ} (hs : Convex ℝ s)
  (hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) : Convex ℝ (f' '' s)

Convex.image_derivWithin: Darboux's theorem: the image of a convex set under f' is a convex set, derivWithin version.

Convex.image_derivWithin {f : ℝ → ℝ} {s : Set ℝ} (hs : Convex ℝ s) (hf : DifferentiableOn ℝ f s) :
  Convex ℝ (derivWithin f s '' s)

Convex.image_deriv: Darboux's theorem: the image of a convex set under f' is a convex set, deriv version.

Convex.image_deriv {f : ℝ → ℝ} {s : Set ℝ} (hs : Convex ℝ s)
  (hf : ∀ x ∈ s, DifferentiableAt ℝ f x) : Convex ℝ (deriv f '' s)

exists_hasDerivWithinAt_eq_of_ge_of_le: Darboux's theorem: if a ≤ b and f' a ≤ m ≤ f' b, then f' c = m for some c ∈ [a, b].

exists_hasDerivWithinAt_eq_of_ge_of_le {a b : ℝ} {f f' : ℝ → ℝ} (hab : a ≤ b)
  (hf : ∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) {m : ℝ} (hma : f' a ≤ m)
  (hmb : m ≤ f' b) : m ∈ f' '' Set.Icc a b

exists_hasDerivWithinAt_eq_of_le_of_ge: Darboux's theorem: if a ≤ b and f' b ≤ m ≤ f' a, then f' c = m for some c ∈ [a, b].

exists_hasDerivWithinAt_eq_of_le_of_ge {a b : ℝ} {f f' : ℝ → ℝ} (hab : a ≤ b)
  (hf : ∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) {m : ℝ} (hma : m ≤ f' a)
  (hmb : f' b ≤ m) : m ∈ f' '' Set.Icc a b
Sources
Mathlibexists_hasDerivWithinAt_eq_of_gt_of_lt · exists_hasDerivWithinAt_eq_of_lt_of_gt · Set.OrdConnected.image_hasDerivWithinAt · Set.OrdConnected.image_derivWithin · Set.OrdConnected.image_deriv · Convex.image_hasDerivWithinAt · Convex.image_derivWithin · Convex.image_deriv · exists_hasDerivWithinAt_eq_of_ge_of_le · exists_hasDerivWithinAt_eq_of_le_of_ge
Uses 14
Statement usesConvex subsets · Differentiable function between normed vector spaces · Differentials (linear tangent functions) · Finite set · Holomorphic functions · Normed vector space over a normed field · Topological module
Proof usesAssociative algebra over a commutative ring · Derivative at a point · Dual of a normed space · Extreme value theorem · Field \(\R\) of real numbers · Order topology · Ordered ring

TheoremDini's theorem#

Dini's theorem: if F n is a monotone increasing collection of continuous functions converging pointwise to a continuous function f, then F n converges locally uniformly to f.

Monotone.tendstoLocallyUniformly_of_forall_tendsto.{u_1, u_2, u_3} {ι : Type u_1} {α : Type u_2}
  {G : Type u_3} [Preorder ι] [TopologicalSpace α] [NormedAddCommGroup G] [Lattice G]
  [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G} {f : α → G}
  (hF_cont : ∀ (i : ι), Continuous (F i)) (hF_mono : Monotone F) (hf : Continuous f)
  (h_tendsto : ∀ (x : α), Filter.Tendsto (fun x_1 => F x_1 x) Filter.atTop (nhds (f x))) :
  TendstoLocallyUniformly F f Filter.atTop
Sources
MathlibMonotone.tendstoLocallyUniformly_of_forall_tendsto
Uses 2
Statement usesContinuous function · Metric space

TheoremFermat's theorem (stationary points)#

Mathlib records this with 2 declarations.

IsLocalExtr.deriv_eq_zero: Fermat's Theorem: the derivative of a function at a local extremum equals zero.

IsLocalExtr.deriv_eq_zero {f : ℝ → ℝ} {a : ℝ} (h : IsLocalExtr f a) : deriv f a = 0

IsLocalExtr.fderiv_eq_zero: Fermat's Theorem: the derivative of a function at a local extremum equals zero.

IsLocalExtr.fderiv_eq_zero.{u} {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ}
  {a : E} (h : IsLocalExtr f a) : fderiv ℝ f a = 0
Sources
MathlibIsLocalExtr.deriv_eq_zero · IsLocalExtr.fderiv_eq_zero
Uses 4 · Used by 1
Statement usesDifferentials (linear tangent functions) · Normed vector space over a normed field
Proof usesDerivative at a point · Local extrema
Used byRolle's theorem

TheoremLebesgue differentiation theorem#

Mathlib states this as VitaliFamily.ae_tendsto_lintegral_div.

VitaliFamily.ae_tendsto_lintegral_div.{u_1} {α : Type u_1} [PseudoMetricSpace α]
  {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ)
  [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {f : α → ENNReal} (hf : AEMeasurable f μ) (h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤) :
  ∀ᵐ (x : α) ∂μ,
    Filter.Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (nhds (f x))
Sources
MathlibVitaliFamily.ae_tendsto_lintegral_div
Uses 10
Statement usesAlmost sure convergence · Associative algebra over a commutative ring · Borel sigma-algebra · Bornology · Carathéodory's theorem (measure theory) · Integral of positive measurable functions · Linear map · Measurable function · Order
Proof usesLebesgue's decomposition theorem

TheoremMonotone convergence theorem (1000+ theorems)#

Mathlib records this with 2 declarations.

MeasureTheory.integral_tendsto_of_tendsto_of_antitone: Monotone convergence theorem for real-valued functions and Bochner integrals

MeasureTheory.integral_tendsto_of_tendsto_of_antitone.{u_1} {α : Type u_1} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : ℕ → α → ℝ} {F : α → ℝ}
  (hf : ∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) (hF : MeasureTheory.Integrable F μ)
  (h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x)
  (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (F x))) :
  Filter.Tendsto (fun n => ∫ (x : α), f n x ∂μ) Filter.atTop (nhds (∫ (x : α), F x ∂μ))

MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone: Monotone convergence theorem expressed with limits.

MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone.{u_1} {α : Type u_1} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} {F : α → ENNReal}
  (hf : ∀ (n : ℕ), AEMeasurable (f n) μ) (h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n => f n x)
  (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (F x))) :
  Filter.Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) Filter.atTop (nhds (∫⁻ (x : α), F x ∂μ))
Sources
MathlibMeasureTheory.integral_tendsto_of_tendsto_of_antitone · MeasureTheory.lintegral_tendsto_of_tendsto_of_monotone
Uses 11 · Used by 1
Statement usesBochner integral · Measurable function
Proof usesBorel sigma-algebra · Cluster point · Completeness of R · Hausdorff space · Lipschitz continuity · Metric structure · Order topology · Topological ring · Topology on a normed vector space
Used byLebesgue's decomposition theorem

TheoremRademacher's theorem#

Rademacher's theorem: a function between finite-dimensional real vector spaces which is Lipschitz on a set is differentiable almost everywhere in this set.

LipschitzOnWith.ae_differentiableWithinAt.{u_1, u_2} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace ℝ F] {C : NNReal} {s : Set E} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E]
  [FiniteDimensional ℝ F] [μ.IsAddHaarMeasure] {f : E → F} (hf : LipschitzOnWith C f s)
  (hs : MeasurableSet s) : ∀ᵐ (x : E) ∂μ.restrict s, DifferentiableWithinAt ℝ f s x
Sources
MathlibLipschitzOnWith.ae_differentiableWithinAt
Uses 29
Statement usesAlmost sure convergence · Associative algebra over a commutative ring · Borel sigma-algebra · Carathéodory's theorem (measure theory) · Compactness in terms of filters · Continuous linear map · Finite-dimensionality · Measurable function · Normed vector space over a normed field · Positive measure
Proof uses\(C^k\) function · Characteristic zero · Complementary subspaces · Completeness of R · Derivative at a point · Derivative of a composition of functions (Analysis) · Differentiable functions · Directional derivative · Dominated convergence theorem · Dual of a normed space · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Homeomorphisms · Isomorphism with \(K^n\) · Lebesgue measure (Measures and integral calculus) · Lipschitz continuity · Metric structure · Order topology · The Triangle Inequality · Topology of a metric space

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.