Documentation

TauCeti.Analysis.Sobolev.GraphStep

The closed-graph step for weak Sobolev spaces #

This file packages the successor step shared by the iterated weak Sobolev spaces. Given a seminormed space X 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, so the resulting graph space is complete whenever X is. 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.

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 #

References #

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

source
@[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, carrying the Euclidean (WithLp 2) product norm of its two components. They are projected out by WithLp.fst and WithLp.snd.

Equations
Instances For
    source
    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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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.

    Equations
    Instances For
      source
      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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))) (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.

      source
      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] [SeminormedAddCommGroup X] [NormedSpace ℝ X] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [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.

      source
      @[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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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. It is complete when X is complete.

      Equations
      Instances For
        source
        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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))) :
        ↥(WeakDerivStep mu Omega p base) →L[ℝ] X

        The continuous projection to the preceding graph space.

        Equations
        Instances For
          source
          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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))) (u : ↥(WeakDerivStep mu Omega p base)) :
          X

          The preceding graph-space component.

          Equations
          Instances For
            source
            @[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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))) (u : ↥(WeakDerivStep mu Omega p base)) :
            (prevL base) u = prev base u
            source
            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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))) (u : ↥(WeakDerivStep mu Omega p base)) :
            prev base u = WithLp.fst ↑u
            source
            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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))) :
            ↥(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.

            Equations
            Instances For
              source
              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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))) (u : ↥(WeakDerivStep mu Omega p base)) :
              ↥(MeasureTheory.Lp (E →L[ℝ] F) p (mu.restrict ↑Omega))

              The adjoined Lᵖ weak Fréchet derivative.

              Equations
              Instances For
                source
                @[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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))) (u : ↥(WeakDerivStep mu Omega p base)) :
                (weakFDerivL base) u = weakFDeriv base u
                source
                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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))) (u : ↥(WeakDerivStep mu Omega p base)) :
                weakFDeriv base u = WithLp.snd ↑u
                source
                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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))) (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.

                Equations
                Instances For
                  source
                  @[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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))) (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
                  source
                  @[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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))) (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
                  source
                  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] [SeminormedAddCommGroup X] [NormedSpace ℝ X] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [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.

                  source
                  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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))} {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.

                  source
                  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] [SeminormedAddCommGroup X] [NormedSpace ℝ X] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [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.

                  source
                  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] [SeminormedAddCommGroup X] [NormedSpace ℝ X] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [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
                  source
                  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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))) (u : ↥(WeakDerivStep mu Omega p base)) :
                  ‖prev base u‖ ≤ ‖u‖

                  The graph norm controls the preceding component.

                  source
                  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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))) (u : ↥(WeakDerivStep mu Omega p base)) :
                  ‖weakFDeriv base u‖ ≤ ‖u‖

                  The graph norm controls the adjoined weak derivative.

                  source
                  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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))) (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.

                  source
                  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] [SeminormedAddCommGroup X] [NormedSpace ℝ 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))} {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.

                  source
                  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] [SeminormedAddCommGroup X] [NormedSpace ℝ X] {mu : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts mu] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] [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.