noncomputable def quadratic_affine_function_on_lp {ι : Type u} [Fintype ι] (p : ENNReal) (A : Matrix ι ι ℝ) (b : ι → ℝ) (c : ℝ) : WithLp p (ι → ℝ) → ℝ

The quadratic-affine function x ↦ (1 / 2) xᵀ A x + bᵀ x + c, viewed on the canonical WithLp p model of a finite real product, specializing to ℝ^n for ι = Fin n.

@[simp]

theorem quadratic_affine_function_on_lp_apply {ι : Type u} [Fintype ι] (p : ENNReal) (A : Matrix ι ι ℝ) (b : ι → ℝ) (c : ℝ) (x : WithLp p (ι → ℝ)) : quadratic_affine_function_on_lp p A b c x = quadratic_affine_function A b c x.ofLp

Evaluating quadratic_affine_function_on_lp p A b c at x applies the Chapter 4 quadratic-affine function to the underlying coordinate vector ofLp x.

@[simp]

theorem quadratic_affine_function_on_lp_two_apply_eq {ι : Type u} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℝ) (b x : EuclideanSpace ℝ ι) : quadratic_affine_function_on_lp 2 A b.ofLp 0 x = 1 / 2 * inner ℝ ((Matrix.toEuclideanLin A) x) x + inner ℝ b x

The Chapter 5 coordinate quadratic owner at p = 2 is the intrinsic Euclidean quadratic x ↦ (1 / 2) ⟪A.toEuclideanLin x, x⟫ + ⟪b, x⟫.

theorem quadratic_affine_function_on_lp_is_l_smooth_on_opNorm {ι : Type u} [Fintype ι] (p q : ENNReal) [DecidableEq ι] [Fact (1 ≤ p)] [Fact (1 ≤ q)] [p.HolderConjugate q] (A : Matrix ι ι ℝ) (hA : A.IsSymm) (b : ι → ℝ) (c : ℝ) : is_l_smooth_on (quadratic_affine_function_on_lp p A b c) Set.univ ‖LinearMap.toContinuousLinearMap ((Matrix.toLpLin p q) A)‖.toNNReal

Helper for Proposition 5.1: the induced matrix norm Real.toNNReal ‖A‖[p,q] is a global smoothness parameter for the quadratic-affine function on WithLp p (ι → ℝ).

theorem quadratic_affine_function_on_lp_opNorm_isLeast_smoothness_parameter {ι : Type u} [Fintype ι] (p q : ENNReal) [DecidableEq ι] [Fact (1 ≤ p)] [Fact (1 ≤ q)] [p.HolderConjugate q] (A : Matrix ι ι ℝ) (hA : A.IsSymm) (b : ι → ℝ) (c : ℝ) : IsLeast {L : NNReal | is_l_smooth_on (quadratic_affine_function_on_lp p A b c) Set.univ L} ‖LinearMap.toContinuousLinearMap ((Matrix.toLpLin p q) A)‖.toNNReal

Proposition 5.1: for the quadratic function x ↦ (1 / 2) xᵀ A x + bᵀ x + c on ℝ^n, viewed with the ℓ_p norm on a finite real product ι → ℝ, and hence on ℝ^n when ι = Fin n, the smallest global smoothness parameter is Real.toNNReal ‖A‖[p,q], the textbook induced matrix norm ‖A‖_{p,q} for a Hölder-conjugate pair p, q.