Skip to main content

Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.

All topics

Showing 751 to 756 of 2,569 results.

Project-declaredLean 4.29.0-rc6

Deriv eq zero ae on zero Set

DeGiorgi.deriv_eq_zero_ae_on_zeroSet

Mathematical statement

1D Stampacchia (a.e.): for f differentiable a.e., f' = 0 a.e. on {f = 0}. Proof: {f=0 ∧ f'≠0 ∧ f differentiable} ⊆ {isolated points of {f=0}}, which is countable (hence measure 0). The remaining set {f not differentiable} has measure 0 by hypothesis.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

Deriv ne zero implies isolated zero

DeGiorgi.deriv_ne_zero_implies_isolated_zero

Project documentation

Core lemma: if f is differentiable at x with f(x) = 0 and f'(x) ≠ 0, then f(x+h) ≠ 0 for all sufficiently small h ≠ 0. Proof: the little-o condition gives |f(x+h) - c·h| ≤ (|c|/2)·|h| for small h. Since f(x) = 0, triangle inequality gives |f(x+h)| ≥ |c|·|h|/2 > 0.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

Dirichlet Problem exists of divergence Data

DeGiorgi.dirichletProblem_exists_of_divergenceData

Mathematical statement

Existence of weak solutions to the inhomogeneous Dirichlet problem with boundary datum u₀ and divergence-form right-hand side div F.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record
Project-declaredLean 4.29.0-rc6

Dirichlet Problem unique of divergence Data

DeGiorgi.dirichletProblem_unique_of_divergenceData

Mathematical statement

Inhomogeneous Dirichlet solutions are unique up to a.e. equality.

partial differential equationsregularity theoryanalysis

Source project: DeGiorgi

Person-level attribution pending.

View proof record