Prove2Me

The norm of a real-linear map on C\mathbb C is at most ∥T1∥+∥Ti∥\|T1\|+\|Ti\|

Proved
JHolomorphic.norm_le_norm_apply_one_add_norm_apply_I

by Mazecto · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysislinear-algebra

Let FF be a real normed space and T:C→FT:\mathbb C\to F a continuous real-linear map. Then

∥T∥≤∥T(1)∥+∥T(i)∥.\|T\|\le\|T(1)\|+\|T(i)\|.

This bounds operator norms of derivatives on planar domains by their two partial derivatives.

Formalization Note T : ℂ →L[ℝ] F, the operator norm ‖T‖.

Preamble
import Definitions.Def_JHolomorphic_Setting
import Mathlib.Analysis.Calculus.ContDiff.Operations
import Mathlib.Analysis.Calculus.ContDiff.Comp
import Mathlib.Analysis.Calculus.FDeriv.CompCLM
import Mathlib.Analysis.Calculus.FDeriv.Mul
import Mathlib.Analysis.Calculus.FDeriv.Measurable
import Mathlib.Analysis.Normed.Operator.Bilinear
import Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
import Mathlib.MeasureTheory.Function.LpSpace.Indicator
Formal statement
namespace JHolomorphic

open MeasureTheory Metric Filter Topology Set
open scoped ContDiff ENNReal NNReal

/-- The operator norm of a real-linear map `T` on `ℂ` is at most `‖T 1‖ + ‖T i‖`. -/
theorem norm_le_norm_apply_one_add_norm_apply_I {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    (T : ℂ →L[ℝ] F) : ‖T‖ ≤ ‖T 1‖ + ‖T Complex.I‖ := by
  sorry

end JHolomorphic
Source
Elementary linear algebra; used for C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 2, Theorem 2.22

View graph