The closed-graph step for weak Sobolev spaces

This file packages the successor step shared by the iterated weak Sobolev spaces. Given a real module X with a topology and a continuous linear map from X to an Lᵖ space of F-valued fields, TauCeti.WeakDerivStep adjoins an Lᵖ weak Fréchet derivative of that field. The admissibility condition is a closed subspace. If X carries a complete uniform structure, the resulting graph space is complete. The construction works on any real normed domain with measurable opens and a measure finite on compact sets. Its intrinsic weak-derivative characterization additionally needs local finiteness of the measure restricted to the open set, while finite dimensionality is needed only for extensionality via uniqueness of weak derivatives. The constructor takes an existing weak derivative and needs no local-finiteness assumption.

The construction is independent of the order of differentiation. It is iterated by Wkp, which starts from the weak gradient and adjoins one weak derivative per order; the projections, constructors, norm bounds, and completeness there specialize the results proved here.

When X is seminormed, the graph carries the Euclidean (WithLp 2) product norm

(∥x∥_X² + ∥Du∥_p²)¹⁄²,

whose exponent is two whatever p is. That is what makes the squared-norm identity TauCeti.WeakDerivStep.norm_sq_eq_norm_prev_sq_add_norm_weakFDeriv_sq available for every p.

Main declarations

• TauCeti.weakDerivStepSubmodule: the closed graph of one weak-derivative step.
• TauCeti.mem_weakDerivStepSubmodule_iff_hasWeakFDerivOn: its intrinsic characterization.
• TauCeti.WeakDerivStep: the resulting graph space, with projections TauCeti.WeakDerivStep.prev and TauCeti.WeakDerivStep.weakFDeriv, constructor TauCeti.WeakDerivStep.mk, and extensionality TauCeti.WeakDerivStep.ext.
• TauCeti.WeakDerivStep.norm_sq_eq_norm_prev_sq_add_norm_weakFDeriv_sq, TauCeti.WeakDerivStep.norm_prev_add_norm_weakFDeriv_le: the graph norm in terms of its components, and the bound ‖x‖ + ‖Du‖_p ≤ √2 ‖(x, Du)‖.
• TauCeti.WeakDerivStep.restrictBaseL: restriction of the selected field to an open subdomain, with its exact and almost-everywhere characteristic equations.
• TauCeti.WeakDerivStep.norm_prev_sq_eq_integral, TauCeti.WeakDerivStep.norm_weakFDeriv_sq_eq_integral: on the line, the squared norms of a W^{1,2} path and of its weak derivative are the integrals of ‖φ‖² and ‖φ'‖² for a C¹ representative φ.

References

The iterated weak-derivative definition and the closed-graph completeness argument follow L. C. Evans, Partial Differential Equations, Chapter 5, §5.2.

@[reducible, inline]

abbrev TauCeti.WeakDerivStepJetLp {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] (mu : MeasureTheory.Measure E) (Omega : TopologicalSpace.Opens E) (p : ENNReal) (X : Type u_4) (F : Type u_5) [NormedAddCommGroup F] [NormedSpace ℝ F] : Type (max (max u_1 u_5) u_4)

The ambient graph space obtained by adjoining an Lᵖ candidate weak derivative to X, with the product topology and, when X is seminormed, the Euclidean (WithLp 2) product norm. Its components are projected out by WithLp.fst and WithLp.snd.

noncomputable def TauCeti.weakDerivStepSubmodule {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (mu : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts mu] (Omega : TopologicalSpace.Opens E) (p : ENNReal) [Fact (1 ≤ p)] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) : ClosedSubmodule ℝ (WeakDerivStepJetLp mu Omega p X F)

The closed subspace in which the adjoined field is the weak derivative of base x.

theorem TauCeti.mem_weakDerivStepSubmodule_iff {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (J : WeakDerivStepJetLp mu Omega p X F) : J ∈ weakDerivStepSubmodule mu Omega p base ↔ ∀ (phi : TestFunction Omega ℝ ⊤) (v : E), ∫ (x : E), lineDeriv ℝ (⇑phi) x v • ↑↑(base (WithLp.fst J)) x ∂mu + ∫ (x : E), phi x • (↑↑(WithLp.snd J) x) v ∂mu = 0

Membership in the weak-derivative step is the family of integration-by-parts identities.

theorem TauCeti.mem_weakDerivStepSubmodule_iff_hasWeakFDerivOn {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] [MeasureTheory.IsLocallyFiniteMeasure (mu.restrict ↑Omega)] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (J : WeakDerivStepJetLp mu Omega p X F) : J ∈ weakDerivStepSubmodule mu Omega p base ↔ HasWeakFDerivOn mu Omega ↑↑(base (WithLp.fst J)) ↑↑(WithLp.snd J)

A jet is in the closed graph exactly when its last field is the weak derivative of the field selected by base.

@[reducible, inline]

noncomputable abbrev TauCeti.WeakDerivStep {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (mu : MeasureTheory.Measure E) [MeasureTheory.IsFiniteMeasureOnCompacts mu] (Omega : TopologicalSpace.Opens E) (p : ENNReal) [Fact (1 ≤ p)] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) : Submodule ℝ (WeakDerivStepJetLp mu Omega p X F)

One weak-derivative graph step over the field selected by base. For X with a complete uniform structure, this graph space is complete.

noncomputable def TauCeti.WeakDerivStep.prevL {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) : ↥(WeakDerivStep mu Omega p base) →L[ℝ] X

The continuous projection to the preceding graph space.

noncomputable def TauCeti.WeakDerivStep.prev {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (u : ↥(WeakDerivStep mu Omega p base)) : X

The preceding graph-space component.

@[simp]

theorem TauCeti.WeakDerivStep.prevL_apply {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (u : ↥(WeakDerivStep mu Omega p base)) : (prevL base) u = prev base u

@[simp]

theorem TauCeti.WeakDerivStep.prev_add {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (u w : ↥(WeakDerivStep mu Omega p base)) : prev base (u + w) = prev base u + prev base w

The projection prev is additive.

@[simp]

theorem TauCeti.WeakDerivStep.prev_smul {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (c : ℝ) (u : ↥(WeakDerivStep mu Omega p base)) : prev base (c • u) = c • prev base u

The projection prev commutes with scalar multiplication.

@[simp]

theorem TauCeti.WeakDerivStep.prev_zero {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) : prev base 0 = 0

The projection prev vanishes at zero.

theorem TauCeti.WeakDerivStep.prev_coe {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (u : ↥(WeakDerivStep mu Omega p base)) : prev base u = WithLp.fst ↑u

noncomputable def TauCeti.WeakDerivStep.restrictBaseL {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) {V : TopologicalSpace.Opens E} (hV : V ≤ Omega) : ↥(WeakDerivStep mu Omega p base) →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑V))

Restrict the field selected by base to an open subset of its domain.

@[simp]

theorem TauCeti.WeakDerivStep.restrictBaseL_apply {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) {V : TopologicalSpace.Opens E} (hV : V ≤ Omega) (u : ↥(WeakDerivStep mu Omega p base)) : (restrictBaseL base hV) u = (MeasureTheory.Lp.LpToLpOfMeasureLeSMul restrictBaseL_apply._proof_1 ⋯) (base (prev base u))

Restriction is the canonical map between the two restricted-measure Lᵖ spaces.

theorem TauCeti.WeakDerivStep.restrictBaseL_apply_ae {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) {V : TopologicalSpace.Opens E} (hV : V ≤ Omega) (u : ↥(WeakDerivStep mu Omega p base)) : ↑↑((restrictBaseL base hV) u) =ᵐ[mu.restrict ↑V] ↑↑(base (prev base u))

Restriction preserves the selected field almost everywhere on the smaller domain.

noncomputable def TauCeti.WeakDerivStep.weakFDerivL {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) : ↥(WeakDerivStep mu Omega p base) →L[ℝ] ↥(MeasureTheory.Lp (E →L[ℝ] F) p (mu.restrict ↑Omega))

The continuous projection to the adjoined weak Fréchet derivative.

noncomputable def TauCeti.WeakDerivStep.weakFDeriv {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (u : ↥(WeakDerivStep mu Omega p base)) : ↥(MeasureTheory.Lp (E →L[ℝ] F) p (mu.restrict ↑Omega))

The adjoined Lᵖ weak Fréchet derivative.

@[simp]

theorem TauCeti.WeakDerivStep.weakFDerivL_apply {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (u : ↥(WeakDerivStep mu Omega p base)) : (weakFDerivL base) u = weakFDeriv base u

theorem TauCeti.WeakDerivStep.weakFDeriv_coe {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (u : ↥(WeakDerivStep mu Omega p base)) : weakFDeriv base u = WithLp.snd ↑u

def TauCeti.WeakDerivStep.mk {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (x : X) (D : ↥(MeasureTheory.Lp (E →L[ℝ] F) p (mu.restrict ↑Omega))) (h : HasWeakFDerivOn mu Omega ↑↑(base x) ↑↑D) : ↥(WeakDerivStep mu Omega p base)

Construct an element of a weak-derivative graph from its two components.

@[simp]

theorem TauCeti.WeakDerivStep.prev_mk {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (x : X) (D : ↥(MeasureTheory.Lp (E →L[ℝ] F) p (mu.restrict ↑Omega))) (h : HasWeakFDerivOn mu Omega ↑↑(base x) ↑↑D) : prev base (mk base x D h) = x

@[simp]

theorem TauCeti.WeakDerivStep.weakFDeriv_mk {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (x : X) (D : ↥(MeasureTheory.Lp (E →L[ℝ] F) p (mu.restrict ↑Omega))) (h : HasWeakFDerivOn mu Omega ↑↑(base x) ↑↑D) : weakFDeriv base (mk base x D h) = D

theorem TauCeti.WeakDerivStep.hasWeakFDerivOn_base_prev {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] [MeasureTheory.IsLocallyFiniteMeasure (mu.restrict ↑Omega)] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (u : ↥(WeakDerivStep mu Omega p base)) : HasWeakFDerivOn mu Omega ↑↑(base (prev base u)) ↑↑(weakFDeriv base u)

The adjoined field is the weak derivative of the field selected by base.

theorem TauCeti.WeakDerivStep.ext_prev_weakFDeriv {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] {base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))} {u v : ↥(WeakDerivStep mu Omega p base)} (hprev : prev base u = prev base v) (hweakFDeriv : weakFDeriv base u = weakFDeriv base v) : u = v

Two elements of a weak-derivative graph are equal when their preceding components and their adjoined weak derivatives are equal.

theorem TauCeti.WeakDerivStep.ext {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] [FiniteDimensional ℝ E] [BorelSpace E] {base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))} {u v : ↥(WeakDerivStep mu Omega p base)} (hprev : prev base u = prev base v) : u = v

Two elements of a weak-derivative graph are equal when their preceding components are equal: uniqueness of the weak derivative then forces the adjoined components to agree.

theorem TauCeti.WeakDerivStep.ext_iff {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] [FiniteDimensional ℝ E] [BorelSpace E] {base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))} {u v : ↥(WeakDerivStep mu Omega p base)} : u = v ↔ prev base u = prev base v

theorem TauCeti.WeakDerivStep.tendsto_iff_prev_weakFDeriv {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [TopologicalSpace X] {base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))} {I : Type u_4} {l : Filter I} {v : I → ↥(WeakDerivStep mu Omega p base)} {u : ↥(WeakDerivStep mu Omega p base)} : Filter.Tendsto v l (nhds u) ↔ Filter.Tendsto (fun (i : I) => prev base (v i)) l (nhds (prev base u)) ∧ Filter.Tendsto (fun (i : I) => weakFDeriv base (v i)) l (nhds (weakFDeriv base u))

Convergence in a weak-derivative graph step is equivalent to convergence of the preceding component and of the adjoined weak derivative.

theorem TauCeti.WeakDerivStep.norm_prev_le {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [SeminormedAddCommGroup X] [Module ℝ X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (u : ↥(WeakDerivStep mu Omega p base)) : ‖prev base u‖ ≤ ‖u‖

The graph norm controls the preceding component.

theorem TauCeti.WeakDerivStep.norm_weakFDeriv_le {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [SeminormedAddCommGroup X] [Module ℝ X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (u : ↥(WeakDerivStep mu Omega p base)) : ‖weakFDeriv base u‖ ≤ ‖u‖

The graph norm controls the adjoined weak derivative.

theorem TauCeti.WeakDerivStep.norm_sq_eq_norm_prev_sq_add_norm_weakFDeriv_sq {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [SeminormedAddCommGroup X] [Module ℝ X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (u : ↥(WeakDerivStep mu Omega p base)) : ‖u‖ ^ 2 = ‖prev base u‖ ^ 2 + ‖weakFDeriv base u‖ ^ 2

The squared graph norm is the sum of the squared component norms.

theorem TauCeti.WeakDerivStep.norm_prev_add_norm_weakFDeriv_le {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [SeminormedAddCommGroup X] [Module ℝ X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) (u : ↥(WeakDerivStep mu Omega p base)) : ‖prev base u‖ + ‖weakFDeriv base u‖ ≤ √2 * ‖u‖

The sum of the component norms is at most √2 times the graph norm.

instance TauCeti.WeakDerivStep.instCompleteSpaceSubtypeWeakDerivStepJetLpMemSubmoduleReal {E : Type u_1} {F : Type u_2} {X : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [NormedSpace ℝ E] [OpensMeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [AddCommGroup X] [Module ℝ X] [UniformSpace X] [CompleteSpace X] (base : X →L[ℝ] ↥(MeasureTheory.Lp F p (mu.restrict ↑Omega))) : CompleteSpace ↥(WeakDerivStep mu Omega p base)

A weak-derivative graph step over a complete preceding space is complete because it is a closed subspace.

Norms of a path with a C¹ representative on the line

theorem TauCeti.WeakDerivStep.norm_prev_sq_eq_integral {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {u : ↥(WeakDerivStep MeasureTheory.volume ⊤ 2 (ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp F 2 (MeasureTheory.volume.restrict ↑⊤))))} {φ : ℝ → F} (hu : ↑↑(prev (ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp F 2 (MeasureTheory.volume.restrict ↑⊤))) u) =ᵐ[MeasureTheory.volume.restrict ↑⊤] φ) : ‖prev (ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp F 2 (MeasureTheory.volume.restrict ↑⊤))) u‖ ^ 2 = ∫ (s : ℝ), ‖φ s‖ ^ 2

The squared L² norm of a path is the integral of the squared norm of a representative.

theorem TauCeti.WeakDerivStep.norm_weakFDeriv_sq_eq_integral {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {u : ↥(WeakDerivStep MeasureTheory.volume ⊤ 2 (ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp F 2 (MeasureTheory.volume.restrict ↑⊤))))} {φ : ℝ → F} (hφ : ContDiff ℝ 1 φ) (hu : ↑↑(prev (ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp F 2 (MeasureTheory.volume.restrict ↑⊤))) u) =ᵐ[MeasureTheory.volume.restrict ↑⊤] φ) : ‖weakFDeriv (ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp F 2 (MeasureTheory.volume.restrict ↑⊤))) u‖ ^ 2 = ∫ (s : ℝ), ‖deriv φ s‖ ^ 2

The squared L² norm of the weak derivative is that of the classical derivative of a C¹ representative.