Detecting weak derivatives on relatively compact subdomains

A weak derivative on an open domain can be detected on all open subdomains whose closures are compact and contained in the domain. No boundary regularity or boundedness of the domain is needed. Thus completeness, local integrability, and the test-function identities defining the weak derivative can be verified on relatively compact subdomains.

Main results

• hasWeakLineDerivOn_iff_forall_isCompact_closure: detection of weak directional derivatives.
• hasWeakFDerivOn_iff_forall_isCompact_closure: detection of weak Fréchet derivatives.

Attribution

The reduction to relatively compact subdomains follows Mathlib's exists_open_between_and_isCompact_closure, which places each test function's compact support inside a single testing subdomain.

theorem TauCeti.hasWeakLineDerivOn_iff_forall_isCompact_closure {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [LocallyCompactSpace E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u u' : E → F} {v : E} : HasWeakLineDerivOn μ Ω u u' v ↔ ∀ (V : TopologicalSpace.Opens E), IsCompact (closure ↑V) → closure ↑V ⊆ ↑Ω → HasWeakLineDerivOn μ V u u' v

Weak directional derivatives are detected on relatively compact open subdomains. The closure of each testing subdomain must lie inside Ω. Completeness and local integrability need not be assumed separately: they follow from the subdomain hypotheses, including the empty subdomain when Ω is empty.

theorem TauCeti.hasWeakFDerivOn_iff_forall_isCompact_closure {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [LocallyCompactSpace E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {u : E → F} {U : E → E →L[ℝ] F} : HasWeakFDerivOn μ Ω u U ↔ ∀ (V : TopologicalSpace.Opens E), IsCompact (closure ↑V) → closure ↑V ⊆ ↑Ω → HasWeakFDerivOn μ V u U

Weak Fréchet derivatives are detected on relatively compact open subdomains. The equivalence holds for arbitrary real normed codomain and measure, without assumptions on the boundary of the domain.