Documentation

TauCeti.Analysis.Sobolev.WeakDeriv.Limit

Weak derivatives pass to L¹ limits #

The weak-derivative relation of TauCeti/Analysis/Sobolev/WeakDeriv/Basic.lean is a family of integral identities against test functions, so it survives any limit that is strong enough to pass under those integrals. Convergence in L¹(Ω) is enough: a test function and its directional derivatives are bounded and supported inside Ω, so

∫ (∂_v φ) • uᵢ → ∫ (∂_v φ) • u and ∫ φ • uᵢ' → ∫ φ • u'

as soon as ‖uᵢ - u‖_{L¹(Ω)} → 0 and ‖uᵢ' - u'‖_{L¹(Ω)} → 0. Local integrability of the two limits is not automatic from the convergence and is therefore a hypothesis.

This is the step that transports a derivative computation from smooth functions to a general Sobolev function: the smooth approximations have classical derivatives, and the limit inherits them weakly. It is stated for an arbitrary filter of approximations, and with the L¹ distance written as a lower Lebesgue integral so that no integrability of the differences is needed.

Main declarations #

source
theorem TauCeti.hasWeakLineDerivOn_of_tendsto_lintegral_enorm_sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {v : E} {ι : Type u_3} {l : Filter ι} [OpensMeasurableSpace E] [l.NeBot] {u u' : ι → E → F} {w w' : E → F} (hw : MeasureTheory.LocallyIntegrableOn w (↑Ω) μ) (hw' : MeasureTheory.LocallyIntegrableOn w' (↑Ω) μ) (h : ∀ (i : ι), HasWeakLineDerivOn μ Ω (u i) (u' i) v) (hu : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : E) in ↑Ω, ‖u i x - w x‖ₑ ∂μ) l (nhds 0)) (hu' : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : E) in ↑Ω, ‖u' i x - w' x‖ₑ ∂μ) l (nhds 0)) :
HasWeakLineDerivOn μ Ω w w' v

Weak directional derivatives pass to L¹(Ω) limits. If each uᵢ has uᵢ' as a weak derivative in the direction v on Ω, and both families converge in L¹(Ω) to locally integrable limits, then the limit of the derivatives is a weak derivative of the limit.

source
theorem TauCeti.hasWeakFDerivOn_of_tendsto_lintegral_enorm_sub {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : TopologicalSpace.Opens E} {ι : Type u_3} {l : Filter ι} [OpensMeasurableSpace E] [l.NeBot] {u : ι → E → F} {U : ι → E → E →L[ℝ] F} {w : E → F} {W : E → E →L[ℝ] F} (hw : MeasureTheory.LocallyIntegrableOn w (↑Ω) μ) (hW : ∀ (v : E), MeasureTheory.LocallyIntegrableOn (fun (x : E) => (W x) v) (↑Ω) μ) (h : ∀ (i : ι), HasWeakFDerivOn μ Ω (u i) (U i)) (hu : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : E) in ↑Ω, ‖u i x - w x‖ₑ ∂μ) l (nhds 0)) (hU : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : E) in ↑Ω, ‖U i x - W x‖ₑ ∂μ) l (nhds 0)) :
HasWeakFDerivOn μ Ω w W

Weak Fréchet derivatives pass to L¹(Ω) limits. The Fréchet form of TauCeti.hasWeakLineDerivOn_of_tendsto_lintegral_enorm_sub, with the derivatives converging in the operator norm.