noncomputable def SetValuedOperator.domainQuadraticPotential {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (D : Submodule ℝ H) (T : ↥D →ₗ[ℝ] H) : H → ↑(Set.Ioi ⊥)

The function h from Proposition 20.40, attached to a linear map T defined on a subspace D, equal to (1 / 2) ⟪x, T x⟫_ℝ on D and +∞ off D.

@[simp]

theorem SetValuedOperator.domainQuadraticPotential_apply_of_mem {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (D : Submodule ℝ H) (T : ↥D →ₗ[ℝ] H) {x : H} (hx : x ∈ D) : ↑(domainQuadraticPotential D T x) = ↑(1 / 2) * ↑(inner ℝ x (T ⟨x, hx⟩))

On the subspace D, domainQuadraticPotential D T equals (1 / 2) ⟪x, T x⟫_ℝ.

@[simp]

theorem SetValuedOperator.domainQuadraticPotential_apply_of_not_mem {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (D : Submodule ℝ H) (T : ↥D →ₗ[ℝ] H) {x : H} (hx : x ∉ D) : ↑(domainQuadraticPotential D T x) = ⊤

Outside the subspace D, domainQuadraticPotential D T equals +∞.

noncomputable def SetValuedOperator.supremalPotential {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (D : Submodule ℝ H) (T : ↥D →ₗ[ℝ] H) : H → ↑(Set.Ioi ⊥)

The function f from Proposition 20.40, defined as the supremum of the affine defects ⟪x, T y⟫_ℝ - h(y) over y ∈ D.

@[simp]

theorem SetValuedOperator.supremalPotential_apply {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (D : Submodule ℝ H) (T : ↥D →ₗ[ℝ] H) (x : H) : ↑(supremalPotential D T x) = ⨆ (y : ↥D), ↑(inner ℝ x (T y) - 1 / 2 * inner ℝ (↑y) (T y))

Coercing supremalPotential D T x to EReal recovers the displayed supremum over D.

theorem SetValuedOperator.supremalPotential_add_indicator_eq_domainQuadraticPotential {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (D : Submodule ℝ H) (T : ↥D →ₗ[ℝ] H) (hsymm : ∀ (x y : ↥D), inner ℝ (↑x) (T y) = inner ℝ (T x) ↑y) (hT_mono : (ofFunction ↑D ⇑T).IsMonotone) : Function.asEReal (supremalPotential D T) + Function.asEReal ι[↑D] = Function.asEReal (domainQuadraticPotential D T)

Proposition 20.40 (1): if A = ofFunction D T is monotone and T is symmetric on D, then the supremal potential f satisfies f + ι_D = h.

theorem SetValuedOperator.supremalPotential_mem_gammaZero_of_monotone {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (D : Submodule ℝ H) (T : ↥D →ₗ[ℝ] H) (hsymm : ∀ (x y : ↥D), inner ℝ (↑x) (T y) = inner ℝ (T x) ↑y) (hT_mono : (ofFunction ↑D ⇑T).IsMonotone) : supremalPotential D T ∈ Γ₀(H)

Proposition 20.40 (2): if A = ofFunction D T is monotone and T is symmetric on D, then the supremal potential belongs to Γ₀(H).

theorem SetValuedOperator.subdifferential_supremalPotential_eq {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (D : Submodule ℝ H) (T : ↥D →ₗ[ℝ] H) (hsymm : ∀ (x y : ↥D), inner ℝ (↑x) (T y) = inner ℝ (T x) ↑y) (hT_max : Maximal IsMonotone (ofFunction ↑D ⇑T)) : ERealFunction.subdifferential (supremalPotential D T) = ofFunction ↑D ⇑T

Proposition 20.40 (3): if A = ofFunction D T is maximally monotone and T is symmetric on D, then the subdifferential of the supremal potential is exactly A.

theorem SetValuedOperator.supremalPotential_eq_biconjugate_domainQuadraticPotential {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (D : Submodule ℝ H) (T : ↥D →ₗ[ℝ] H) (hsymm : ∀ (x y : ↥D), inner ℝ (↑x) (T y) = inner ℝ (T x) ↑y) (hT_max : Maximal IsMonotone (ofFunction ↑D ⇑T)) : Function.asEReal (supremalPotential D T) = ERealFunction.conjugate (ERealFunction.conjugate (Function.asEReal (domainQuadraticPotential D T)))

Proposition 20.40 (4): if A = ofFunction D T is maximally monotone and T is symmetric on D, then the supremal potential is the Fenchel biconjugate of h.