Weak derivatives on an open set #
Lane A of the PDE roadmap builds the Sobolev spaces W^{k,p}(Ω) of a domain out of weak
derivatives, rather than out of Mathlib's whole-space Bessel-potential scale. This file supplies
the underlying differentiation notion: for an open set Ω in a real normed space E, a measure
μ on E, functions u, u' : E → F and a direction v : E,
TauCeti.HasWeakLineDerivOn μ Ω u u' v
says that the codomain F is complete, that u and u' are locally integrable on Ω, and that
∫ (∂_v φ) • u ∂μ = - ∫ φ • u' ∂μ
for every test function φ ∈ 𝓓(Ω, ℝ); for the intended μ, an additive Haar measure, this says
that u' represents the distributional derivative ∂_v u on Ω (see The measure below). The
bundled test-function type TestFunction of Mathlib/Analysis/Distribution/TestFunction.lean is
the class of admissible φ, so the test objects are exactly the distributional ones;
TauCeti.hasWeakLineDerivOn_iff restates the identity in terms of unbundled smooth compactly
supported functions when that is more convenient.
Assembling the directions gives TauCeti.HasWeakFDerivOn μ Ω u U for a candidate weak derivative
U : E → E →L[ℝ] F, the object whose Lᵖ integrability cuts out W^{1,p}(Ω).
Two facts make the notion usable, and both are proved here.
- Uniqueness. Two weak derivatives of the same function in the same direction agree almost
everywhere on
Ω(TauCeti.HasWeakLineDerivOn.ae_eqandTauCeti.HasWeakFDerivOn.ae_eq). This is the fundamental lemma of the calculus of variations, consumed from Mathlib in the formIsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero. - Consistency. For a Haar measure
μ, a classical derivative that is locally integrable onΩis a weak derivative (TauCeti.hasWeakLineDerivOn_of_hasLineDerivAt,TauCeti.hasWeakFDerivOn_of_differentiableOn), by integration by parts. Differentiability alone is not enough: local integrability ofuand of its derivative is part of what it means to have a weak derivative, so both are hypotheses of these theorems and of the comparison theoremsTauCeti.HasWeakLineDerivOn.ae_eq_lineDerivandTauCeti.HasWeakFDerivOn.ae_eq_fderiv. Together with uniqueness this pins the notion down: on aC¹function whose derivative is locally integrable onΩ, the weak derivative is the classical one almost everywhere.
Nothing here assumes that Ω is bounded or that its boundary is regular: the weak derivative is a
purely interior notion, and boundary hypotheses enter only with traces and extensions.
Local integrability #
LocallyIntegrableOn u Ω μ and LocallyIntegrableOn u' Ω μ are part of the definition rather
than side hypotheses on the theorems. That is the textbook statement — a weak derivative is a
relation between two members of L¹_loc(Ω) — and in Lean it is also what makes the predicate say
what it claims: MeasureTheory.integral is 0 on a function that is not integrable, so the bare
integration-by-parts identity is satisfied spuriously by junk-valued pairs, for instance by any
u with a non-integrable singularity inside Ω together with u' = 0. Mathlib guards the same
corner in TestFunction.integralAgainstBilinCLM, which pairs against a function only when it is
locally integrable on Ω and is the zero map otherwise.
The components are projected out by TauCeti.HasWeakLineDerivOn.completeSpace,
TauCeti.HasWeakLineDerivOn.locallyIntegrableOn,
TauCeti.HasWeakLineDerivOn.locallyIntegrableOn_deriv and
TauCeti.HasWeakLineDerivOn.integral_lineDeriv_smul_eq_neg_integral_smul, so a proof never has to
unfold the definition.
The codomain #
CompleteSpace F is a component of the definition, for the same reason local integrability is.
MeasureTheory.integral is defined to be 0 on an incomplete codomain, so for an incomplete
F the identity above would read 0 = -0 and the predicate would degenerate into local
integrability of u and u', making every locally integrable function a weak derivative of every
other. Carrying completeness makes the predicate say what its name claims for every F, and
TauCeti.HasWeakLineDerivOn.completeSpace recovers the instance — usually as
have := h.completeSpace — so the results that consume it, such as the fundamental lemma of the
calculus of variations behind TauCeti.HasWeakLineDerivOn.ae_eq, get it from the hypothesis.
The measure #
The defining identity is not the distributional derivative for an arbitrary μ, and is not
advertised as one. Integrating against μ produces the adjoint of ∂_v relative to μ: for a
weighted μ = volume.withDensity w, the identity reads ∂_v (w • u) = w • u' in the sense of
distributions, a condition on u and u' in which the weight cannot be cancelled: it constrains
w • u', not u', so a constant u need not have weak derivative 0. Exactly when μ is
translation invariant — an additive Haar measure, hence a positive multiple of Lebesgue measure
on a finite-dimensional E — does the identity say that u' represents ∂_v u as a
distribution on Ω, and that is the μ out of which W^{k,p}(Ω) will be built.
Accordingly [μ.IsAddHaarMeasure] is a hypothesis of every result below that ties the notion to
the classical derivative: TauCeti.hasWeakLineDerivOn_of_hasLineDerivAt,
TauCeti.hasWeakLineDerivOn_const, TauCeti.hasWeakFDerivOn_of_differentiableOn,
TauCeti.HasWeakLineDerivOn.ae_eq_lineDeriv and TauCeti.HasWeakFDerivOn.ae_eq_fderiv. It is
carried by those results rather than built into the definition, following Mathlib's own treatment
of MeasureTheory.convolution, whose definition takes a bare μ and whose group-invariance
hypotheses sit on the lemmas that need them: locality, linearity and almost-everywhere uniqueness
are true of the adjoint relation for every μ, and stating them for a Haar measure only would
weaken them for no gain.
Main declarations #
TauCeti.HasWeakLineDerivOn:u'is a weak derivative ofuin the directionvonΩ, relative toμ.TauCeti.HasWeakFDerivOn:Uis a weak (Fréchet) derivative ofuonΩ.TauCeti.HasWeakLineDerivOn.completeSpace,TauCeti.HasWeakLineDerivOn.locallyIntegrableOn,TauCeti.HasWeakLineDerivOn.locallyIntegrableOn_derivandTauCeti.HasWeakLineDerivOn.integral_lineDeriv_smul_eq_neg_integral_smul: the components of the definition.TauCeti.hasWeakLineDerivOn_iff: the unbundled restatement of the defining identity.TauCeti.integrable_smul_of_locallyIntegrableOnandTauCeti.integrable_lineDeriv_smul_of_locallyIntegrableOn: the two integrability facts that make the defining integrals honest.TauCeti.setIntegral_smul_eq_integral_smulandTauCeti.setIntegral_lineDeriv_smul_eq_integral_lineDeriv_smul: a test function onΩand its directional derivative vanish offΩ, so the defining integrals may equivalently be taken overΩ.TauCeti.HasWeakLineDerivOn.monoandTauCeti.HasWeakFDerivOn.mono: a weak derivative onΩis one on every smaller open set.TauCeti.HasWeakLineDerivOn.congr_aeand.congr_ae_deriv, together with theirTauCeti.HasWeakFDerivOncounterparts: the notion only sees the function and its weak derivative up to almost-everywhere equality onΩ.TauCeti.hasWeakLineDerivOn_zeroandTauCeti.hasWeakFDerivOn_zero: the zero function has weak derivative0.TauCeti.HasWeakLineDerivOn.add,.neg,.sub,.const_smul,.sumand theirTauCeti.HasWeakFDerivOncounterparts: linearity in the function.TauCeti.HasWeakLineDerivOn.clm_comp: a continuous linear map on the codomain passes through the weak derivative, which is how a vector-valued weak derivative is read off its scalar components.TauCeti.HasWeakLineDerivOn.add_direction,.smul_direction,.sum_directionandTauCeti.hasWeakLineDerivOn_zero_direction: linearity in the direction, which is what makes theTauCeti.HasWeakFDerivOnpackaging the right one.Module.Basis.hasWeakFDerivOn_of_forall: a candidate weak derivative need only be checked in the directions of a basis.TauCeti.hasWeakLineDerivOn_of_hasLineDerivAtandTauCeti.hasWeakFDerivOn_of_differentiableOn: classical derivatives that are locally integrable onΩare weak derivatives.TauCeti.hasWeakLineDerivOn_const: against a Haar measure, a constant has weak derivative0.TauCeti.hasWeakFDerivOn_testFunction: a test function has weak derivative the linear functional represented by its gradient.TauCeti.HasWeakLineDerivOn.ae_eqandTauCeti.HasWeakFDerivOn.ae_eq: uniqueness almost everywhere onΩ.TauCeti.HasWeakLineDerivOn.ae_eq_lineDerivandTauCeti.HasWeakFDerivOn.ae_eq_fderiv: where the classical derivative exists and is locally integrable onΩ, the weak one agrees with it almost everywhere.
Derivatives of test functions #
Outside its support, the directional derivative of a test function vanishes.
The definitions #
HasWeakLineDerivOn μ Ω u u' v says that u' is a weak derivative of u in the
direction v on the open set Ω, relative to the measure μ: the codomain F is complete, both
functions are locally integrable on Ω, and the integration-by-parts identity
∫ (∂_v φ) • u ∂μ = - ∫ φ • u' ∂μ
holds for every test function φ : 𝓓(Ω, ℝ), that is, for every smooth φ : E → ℝ whose support
is compact and contained in Ω.
Local integrability and completeness of F are part of the definition because without them the
identity is a statement about junk-valued integrals — MeasureTheory.integral is 0 on a
non-integrable function, and 0 outright on an incomplete codomain — and would be satisfied by
pairs that are not weakly differentiable at all; see the module docstring. They are recovered by
TauCeti.HasWeakLineDerivOn.locallyIntegrableOn, .locallyIntegrableOn_deriv and
.completeSpace, the last of which is how a proof gets the CompleteSpace F instance.
For the intended μ, an additive Haar measure, this says exactly that u' represents the
distributional derivative ∂_v u on Ω, and [μ.IsAddHaarMeasure] is the hypothesis of every
result identifying the two (TauCeti.hasWeakLineDerivOn_of_hasLineDerivAt and
TauCeti.hasWeakLineDerivOn_const among them). For a μ that is not translation invariant the
identity is instead the adjoint of ∂_v relative to μ — with a weight w it describes
∂_v (w • u), so a constant need not have weak derivative 0; see the module docstring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The constructor-and-eliminator form of HasWeakLineDerivOn, using bundled test functions.
The definition is sealed by the module system, so downstream modules use this theorem rather than
unfolding it.
The codomain of a weak derivative is complete; use as have := h.completeSpace.
A function that has a weak derivative on Ω is locally integrable on Ω.
A weak derivative on Ω is locally integrable on Ω.
The integration-by-parts identity defining a weak derivative.
HasWeakFDerivOn μ Ω u U says that U : E → E →L[ℝ] F is a weak (Fréchet) derivative of
u on the open set Ω: for every direction v, the function x ↦ U x v is a weak derivative of
u in the direction v. In particular F is complete and u and each x ↦ U x v are locally
integrable on Ω.
Requiring u and U to be Lᵖ on Ω is what cuts out the first-order Sobolev space
W^{1,p}(Ω).
Equations
- TauCeti.HasWeakFDerivOn μ Ω u U = ∀ (v : E), TauCeti.HasWeakLineDerivOn μ Ω u (fun (x : E) => (U x) v) v
Instances For
A weak Fréchet derivative is equivalently a weak directional derivative in every direction.
This is the constructor-and-eliminator form of HasWeakFDerivOn; its sealed definition cannot be
unfolded from a downstream module.
The codomain of a weak Fréchet derivative is complete; use as have := h.completeSpace.
A function that has a weak Fréchet derivative on Ω is locally integrable on Ω.
The defining identity of a weak derivative, stated for unbundled test functions: for a complete
F and locally integrable u and u', weak differentiability is exactly the
integration-by-parts identity against every smooth compactly supported function with support
inside Ω.
A weak derivative on Ω is a weak derivative on every smaller open set: weak
differentiability is a local notion.
A weak Fréchet derivative on Ω is one on every smaller open set.
Every direction of a weak Fréchet derivative is a weak directional derivative.
The zero function has weak derivative 0 in every direction, for every μ: no translation
invariance is needed, since both sides of the defining identity vanish. Completeness of F is
assumed because it is part of TauCeti.HasWeakLineDerivOn. This is the zero of the vector space
structure that TauCeti.HasWeakLineDerivOn.add, .neg and .const_smul supply.
The zero function has weak Fréchet derivative 0, for every μ.
Weak differentiation commutes with negation.
Weak Fréchet differentiation commutes with negation.
Weak differentiation commutes with multiplication by a real scalar.
Weak Fréchet differentiation commutes with multiplication by a real scalar.
Integrability of the defining integrands #
A test function on Ω scales a function locally integrable on Ω to a globally integrable
one: this is TestFunction.integrable_bilin for scalar multiplication.
The direction-v derivative of a test function on Ω is again a test function on Ω, so it
too scales a function locally integrable on Ω to a globally integrable one.
A test function on Ω vanishes off Ω, so integrating φ • w over Ω is the same as
integrating it over the whole space.
The direction-v derivative of a test function on Ω vanishes off Ω too, so the same
truncation holds for (∂_v φ) • w.
Replacing u by a function agreeing with it almost everywhere on Ω preserves the weak
derivative: only the restriction of u to Ω is seen.
Replacing u' by a function agreeing with it almost everywhere on Ω preserves the weak
derivative.
Replacing u by a function agreeing with it almost everywhere on Ω preserves the weak
Fréchet derivative.
Replacing U by a map agreeing with it almost everywhere on Ω preserves the weak Fréchet
derivative.
Extending a function and its weak directional derivative by zero preserves the weak
derivative on the original domain Ω.
Extending a function and its weak Fréchet derivative field by zero preserves the weak
derivative on the original domain Ω.
Linearity #
Weak differentiation is additive.
Weak differentiation is compatible with subtraction.
Weak differentiation commutes with a finite sum of functions.
Weak differentiation commutes with a continuous linear map on the codomain.
Weak Fréchet differentiation is additive.
Weak Fréchet differentiation is compatible with subtraction.
In the direction 0 every locally integrable function has weak derivative 0.
The weak derivative is additive in the direction of differentiation. Together with
TauCeti.HasWeakLineDerivOn.smul_direction this is what makes packaging the directional weak
derivatives into a single continuous linear map, as TauCeti.HasWeakFDerivOn does, the right
move.
The weak derivative is additive over a finite sum of directions.
Scaling the direction #
The weak derivative is homogeneous in the direction of differentiation.
Assembling the directions of a basis #
A weak Fréchet derivative is detected on a basis of directions. If a candidate
U : E → E →L[ℝ] F is a weak derivative of u in each direction of a basis of E, it is a
weak derivative of u in every direction, since every vector is a finite linear combination
of basis vectors. Local integrability of u is a separate hypothesis because it is not implied
by the basis directions when E is trivial.
Classical derivatives are weak derivatives #
This is where the measure has to be an additive Haar measure: integration by parts is available
only for a translation-invariant μ, and it is what makes the weak derivative of this section
the classical one.
A classical derivative is a weak derivative. If u has line derivative u' x in the
direction v at every point of the open set Ω, and both u and u' are locally integrable
on Ω, then u' is a weak derivative of u in the direction v on Ω. Completeness of F is
assumed because it is part of TauCeti.HasWeakLineDerivOn.
The proof is Mathlib's integration by parts applied to u against a test function; the boundary
term is absent because the test function has compact support inside Ω.
A constant function has weak derivative 0 in every direction, for μ an additive Haar
measure: the first sanity check that TauCeti.HasWeakLineDerivOn is not vacuous. Translation
invariance of μ is needed — against a weighted measure a constant pairs with ∂_v of the
weight.
A classical Fréchet derivative is a weak one. If u is differentiable at every point of
the open set Ω, and both u and fderiv ℝ u are locally integrable on Ω, then fderiv ℝ u
is a weak derivative of u on Ω.
Test functions are weakly differentiable #
A test function is the basic example: it is smooth, so its classical derivative is also a weak one. On an inner product space the derivative is recorded through its Riesz representative, the gradient, which is the form in which the Sobolev spaces consume it.
A test function is weakly differentiable, with weak derivative the continuous linear functional represented by its gradient.
Uniqueness #
A weak derivative is unique almost everywhere. Two weak derivatives of u in the same
direction on Ω agree almost everywhere on Ω.
This is the fundamental lemma of the calculus of variations: their difference integrates to zero
against every test function supported in Ω, and both are locally integrable on Ω because that
is part of TauCeti.HasWeakLineDerivOn. Completeness of F, which that lemma needs, comes from
h₁ for the same reason.
A weak Fréchet derivative is unique almost everywhere. Two weak derivatives of u on Ω
agree almost everywhere on Ω.
The directional statement TauCeti.HasWeakLineDerivOn.ae_eq is applied along the finitely many
vectors of a basis of E, and the resulting almost-everywhere statements are intersected.
The weak derivative of a classically differentiable function #
The weak derivative of a classically differentiable function is the classical one. If u
has a line derivative in the direction v at every point of Ω, and that line derivative is
locally integrable on Ω, then any weak derivative of u in that direction agrees with it almost
everywhere on Ω. Local integrability of u itself and completeness of F are not hypotheses
here: they are already part of h.
Combined with TauCeti.hasWeakLineDerivOn_of_hasLineDerivAt, this says that the weak derivative
extends the classical one without changing it where the classical one exists.
The weak Fréchet derivative of a differentiable function is fderiv. If u is
differentiable at every point of Ω and fderiv ℝ u is locally integrable on Ω, then any weak
Fréchet derivative of u agrees with fderiv ℝ u almost everywhere on Ω. Local integrability
of u itself and completeness of F are not hypotheses here: they are already part of h.