Operator-norm bounds on ℝ × ℝ from directional components

ℝ × ℝ carries the sup norm ‖(a, b)‖ = max |a| |b| (Prod.norm_def), whose dual is the ℓ¹ norm: a continuous linear functional on ℝ × ℝ is controlled by the sum of its two directional values. This file records that fact, once for a functional into any normed space, and derives the analogous bound for a bilinear form (a continuous linear map into a space of continuous linear maps) by applying it twice. Neither theorem mentions any zoomed field; both are used to convert the pointwise radial/axial derivative bounds of eq:aniso:zoom:derivatives into the operator-norm bounds the finite-axis closures of FiniteContradictionClosure.lean consume.

theorem CIV.norm_clm_le_norm_apply_add_norm_apply {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (L : ℝ × ℝ →L[ℝ] F) : ‖L‖ ≤ ‖L (1, 0)‖ + ‖L (0, 1)‖

A continuous linear functional out of ℝ × ℝ (sup norm) is bounded by the sum of the absolute values of its two directional values L (1, 0) and L (0, 1): every vector's coordinates are each bounded by its sup norm.

theorem CIV.norm_fderiv_fderiv_le_of_apply (g : ℝ × ℝ → ℝ) (y : ℝ × ℝ) : ‖fderiv ℝ (fderiv ℝ g) y‖ ≤ |((fderiv ℝ (fderiv ℝ g) y) (1, 0)) (1, 0)| + |((fderiv ℝ (fderiv ℝ g) y) (1, 0)) (0, 1)| + |((fderiv ℝ (fderiv ℝ g) y) (0, 1)) (1, 0)| + |((fderiv ℝ (fderiv ℝ g) y) (0, 1)) (0, 1)|

The bilinear-form analogue, specialised to an iterated Fréchet derivative: the operator norm of the second derivative of g : ℝ × ℝ → ℝ at y is bounded, by applying norm_clm_le_norm_apply_add_norm_apply twice (once to the second derivative itself, valued in the functionals (ℝ × ℝ) →L[ℝ] ℝ, and once to each of the two resulting functionals), by the sum of the absolute values of its four directional entries. Stating the bound at fderiv ℝ (fderiv ℝ g) y itself, rather than at a bare universally quantified continuous linear map, keeps every instance on the operator-norm topology that fderiv itself installs; a free variable of the bare bilinear type picks up a competing (defeq but not syntactically equal) topology instance from the plain continuous-linear-map arrow and the two do not unify.