def SetValuedOperator.leftEndpoint (T : ↑(Set.Ioi 0)) : ↑(Set.Icc 0 ↑T)

The left endpoint 0 of the interval [0,T] as a point of Set.Icc (0 : ℝ) T.

def SetValuedOperator.rightEndpoint (T : ↑(Set.Ioi 0)) : ↑(Set.Icc 0 ↑T)

The right endpoint T of the interval [0,T] as a point of Set.Icc (0 : ℝ) T.

theorem SetValuedOperator.instIsFiniteMeasureElemRealIccOfNatValMemSetIoiVolume (T : ↑(Set.Ioi 0)) : MeasureTheory.IsFiniteMeasure MeasureTheory.volume

inductive SetValuedOperator.TimeDerivativeBoundaryCondition (H : Type u) : Type u

Boundary conditions from Example 20.9 for the time-derivative operator on L²([0,T]; H).

• initial {H : Type u} (x0 : H) : TimeDerivativeBoundaryCondition H

  The Sobolev representative has prescribed initial value x0.

• periodic {H : Type u} : TimeDerivativeBoundaryCondition H

  The Sobolev representative is periodic on [0,T].

def SetValuedOperator.TimeDerivativeBoundaryCondition.Holds {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] {T : ↑(Set.Ioi 0)} (bc : TimeDerivativeBoundaryCondition H) (f : SobolevW12 H T) : Prop

The boundary condition from Example 20.9 imposed on a Sobolev representative on [0,T].

@[simp]

theorem SetValuedOperator.TimeDerivativeBoundaryCondition.holds_initial_iff {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] {T : ↑(Set.Ioi 0)} (x0 : H) (f : SobolevW12 H T) : (initial x0).Holds f ↔ f.toContinuousMap (leftEndpoint T) = x0

@[simp]

theorem SetValuedOperator.TimeDerivativeBoundaryCondition.holds_periodic_iff {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] {T : ↑(Set.Ioi 0)} (f : SobolevW12 H T) : periodic.Holds f ↔ f.toContinuousMap (leftEndpoint T) = f.toContinuousMap (rightEndpoint T)

def SetValuedOperator.timeDerivativeDomain {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ↑(Set.Ioi 0)) (bc : TimeDerivativeBoundaryCondition H) : Set ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)

The source domain D from Example 20.9: the L²([0,T]; H) classes that admit a W^{1,2} representative satisfying the chosen boundary condition.

@[simp]

theorem SetValuedOperator.mem_timeDerivativeDomain_iff {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ↑(Set.Ioi 0)) (bc : TimeDerivativeBoundaryCondition H) (x : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) : x ∈ timeDerivativeDomain T bc ↔ ∃ (f : SobolevW12 H T), f.toLp = x ∧ bc.Holds f

theorem SetValuedOperator.existsUnique_deriv_of_mem_timeDerivativeDomain {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ↑(Set.Ioi 0)) (bc : TimeDerivativeBoundaryCondition H) {x : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)} (hx : x ∈ timeDerivativeDomain T bc) : ∃! x' : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume), ∃ (f : SobolevW12 H T), f.toLp = x ∧ bc.Holds f ∧ f.deriv = x'

On the source domain from Example 20.9, the derivative class is uniquely determined by the L² class together with the boundary condition.

noncomputable def SetValuedOperator.timeDerivative {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ↑(Set.Ioi 0)) (bc : TimeDerivativeBoundaryCondition H) : ↑(timeDerivativeDomain T bc) → ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)

The canonical derivative class attached to an element of the source domain from Example 20.9.

theorem SetValuedOperator.timeDerivative_spec {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ↑(Set.Ioi 0)) (bc : TimeDerivativeBoundaryCondition H) (x : ↑(timeDerivativeDomain T bc)) : ∃ (f : SobolevW12 H T), f.toLp = ↑x ∧ bc.Holds f ∧ f.deriv = timeDerivative T bc x

The canonical derivative on the source domain is realized by a Sobolev representative with the chosen boundary condition.

theorem SetValuedOperator.deriv_eq_timeDerivative_of_exists {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ↑(Set.Ioi 0)) (bc : TimeDerivativeBoundaryCondition H) (x : ↑(timeDerivativeDomain T bc)) {x' : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)} (hx' : ∃ (f : SobolevW12 H T), f.toLp = ↑x ∧ bc.Holds f ∧ f.deriv = x') : x' = timeDerivative T bc x

Any Sobolev representative of a point in the source domain has derivative equal to the canonical derivative attached to that domain point.

def SetValuedOperator.timeDerivativeOperator {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ↑(Set.Ioi 0)) (bc : TimeDerivativeBoundaryCondition H) : SetValuedOperator ↥(MeasureTheory.Lp H 2 MeasureTheory.volume) ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)

Example 20.9: the time-derivative operator sends x to the singleton {x'} on the source domain D, where x' is the canonical derivative class, and to ∅ outside D.

@[simp]

theorem SetValuedOperator.timeDerivativeOperator_apply_of_mem {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ↑(Set.Ioi 0)) (bc : TimeDerivativeBoundaryCondition H) {x : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)} (hx : x ∈ timeDerivativeDomain T bc) : timeDerivativeOperator T bc x = {timeDerivative T bc ⟨x, hx⟩}

@[simp]

theorem SetValuedOperator.timeDerivativeOperator_apply_of_not_mem {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ↑(Set.Ioi 0)) (bc : TimeDerivativeBoundaryCondition H) {x : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)} (hx : x ∉ timeDerivativeDomain T bc) : timeDerivativeOperator T bc x = ∅

@[simp]

theorem SetValuedOperator.mem_dom_timeDerivativeOperator_iff {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ↑(Set.Ioi 0)) (bc : TimeDerivativeBoundaryCondition H) (x : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) : x ∈ (timeDerivativeOperator T bc).dom ↔ x ∈ timeDerivativeDomain T bc

The source domain D is exactly the domain of the time-derivative operator from Example 20.9.

@[simp]

theorem SetValuedOperator.mem_timeDerivativeOperator_iff {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ↑(Set.Ioi 0)) (bc : TimeDerivativeBoundaryCondition H) (x x' : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) : x' ∈ timeDerivativeOperator T bc x ↔ ∃ (f : SobolevW12 H T), f.toLp = x ∧ bc.Holds f ∧ f.deriv = x'

Bridge lemma: membership in the time-derivative operator is exactly the existential graph description in terms of Sobolev representatives satisfying the chosen boundary condition.

theorem SetValuedOperator.mem_timeDerivativeOperator_initial_iff {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ↑(Set.Ioi 0)) (x0 : H) (x x' : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) : x' ∈ timeDerivativeOperator T (TimeDerivativeBoundaryCondition.initial x0) x ↔ ∃ (f : SobolevW12 H T), f.toLp = x ∧ f.toContinuousMap (leftEndpoint T) = x0 ∧ f.deriv = x'

Membership in the initial-value time-derivative operator means being the derivative class of a Sobolev representative with the prescribed left endpoint.

theorem SetValuedOperator.mem_timeDerivativeOperator_periodic_iff {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ↑(Set.Ioi 0)) (x x' : ↥(MeasureTheory.Lp H 2 MeasureTheory.volume)) : x' ∈ timeDerivativeOperator T TimeDerivativeBoundaryCondition.periodic x ↔ ∃ (f : SobolevW12 H T), f.toLp = x ∧ f.toContinuousMap (leftEndpoint T) = f.toContinuousMap (rightEndpoint T) ∧ f.deriv = x'

Membership in the periodic time-derivative operator means being the derivative class of a Sobolev representative whose endpoint values on [0,T] coincide.

theorem SetValuedOperator.timeDerivativeOperator_isMonotone {H : Type u} [NormedAddCommGroup H] [NormedSpace ℝ H] (T : ↑(Set.Ioi 0)) [InnerProductSpace ℝ H] (bc : TimeDerivativeBoundaryCondition H) : (timeDerivativeOperator T bc).IsMonotone

Example 20.9: for either a prescribed initial value or the periodic boundary condition, the time-derivative operator on L²([0,T]; H) is monotone.