@[reducible, inline]

noncomputable abbrev conjugate_function_strongDual {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → EReal) : StrongDual ℝ E → EReal

The Fenchel conjugate on the continuous dual, obtained by restricting the Chapter 4 owner conjugate_function along the canonical coercion StrongDual ℝ E → Module.Dual ℝ E.

@[simp]

theorem conjugate_function_strongDual_apply {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → EReal) (y : StrongDual ℝ E) : conjugate_function_strongDual f y = conjugate_function f ↑y

Evaluating the continuous-dual Fenchel conjugate is the same as evaluating the Chapter 4 owner at the underlying algebraic functional.

@[simp]

theorem mem_effective_domain_conjugate_function_strongDual {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : E → EReal} {y : StrongDual ℝ E} : y ∈ effective_domain (conjugate_function_strongDual f) ↔ conjugate_function_strongDual f y < ⊤

Membership in the finite-valued domain of the continuous-dual Fenchel conjugate is exactly the expected pointwise finiteness condition.

theorem conjugateFunctionStrongDual_closedConvex {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : E → EReal) : LowerSemicontinuous (conjugate_function_strongDual f) ∧ is_convex_function (conjugate_function_strongDual f)

The continuous-dual Fenchel conjugate is lower semicontinuous and convex. This is the canonical StrongDual ℝ E analogue of Chapter 4's conjugate closed/convex owner theorem, so downstream Chapter 5 files should reuse it instead of reproving the same affine-supremum argument locally.