ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The derivative of a bounded bilinear map

Example

Let $X$ , $Y$ , $Z$ be real Banach spaces and let $B : X \times Y \to Z$ be a bounded bilinear map (A bounded bilinear map between normed spaces), with the product space $X \times Y$ carrying the max norm $∥ (h, k) ∥_{\max} = \max {∥ h ∥, ∥ k ∥}$ (The standard product norms on a finite product of normed spaces). Then $B$ is Fréchet differentiable everywhere, with

$D B (x, y) (h, k) = B (h, y) + B (x, k) ((x, y), (h, k) \in X \times Y),$

the right-hand side being a bounded linear map of $(h, k)$ . In particular:

if an associative multiplication $m (a, b) = a b$ on a real Banach space is a bounded bilinear map — in particular, for a real Banach algebra — then $D m (a, b) (h, k) = h b + a k$ ;
if $X = Y$ , the diagonal map $d : X \to Z$ , $d (x) : = B (x, x)$ , has derivative $D d (x) h = B (h, x) + B (x, h)$ .

Facts & Assumptions

Given: Real Banach spaces $X, Y, Z$ , a bounded bilinear $B : X \times Y \to Z$ with a constant $C \geq 0$ satisfying $∥ B (u, v) ∥ \leq C ∥ u ∥ ∥ v ∥$ for all $u, v$ , and a point $(x, y) \in X \times Y$ .

[L1]

Bounded bilinearity and the defining estimate $∥ B (u, v) ∥ \leq C ∥ u ∥ ∥ v ∥$ (A bounded bilinear map between normed spaces).

[L2]

The max norm on $X \times Y$ is a norm and $∥ (h, k) ∥_{\max} \to 0$ exactly when $h \to 0$ and $k \to 0$ (The standard product norms on a finite product of normed spaces); the norm is subadditive and absolutely homogeneous (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

[L3]

Fréchet differentiability at $(x, y)$ means a bounded linear candidate $T$ whose remainder satisfies $∥ B (x + h, y + k) - B (x, y) - T (h, k) ∥ = o (∥ (h, k) ∥_{\max})$ (Fréchet derivative between Banach spaces); the operator norm bounds $∥ T u ∥ \leq ∥ T ∥ ∥ u ∥$ (The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

[L4]

When $X = Y$ , the diagonal map $Δ : X \to X \times X$ , $x \mapsto (x, x)$ , is bounded linear with $∥ Δ h ∥_{\max} = ∥ h ∥$ . Its derivative is $Δ$ directly from [L3]: $Δ (x + h) - Δ (x) - Δ h = 0$ , so the derivative remainder is identically zero. The chain rule for its composite with $B$ is supplied by Chain sum product and composition rules for Banach derivatives.

Verification

technique · direct

1.1

Expanding with [L1], $B (x + h, y + k) - B (x, y) = B (h, y) + B (x, k) + B (h, k)$ , so the remainder after subtracting the proposed linear part $T (h, k) : = B (h, y) + B (x, k)$ is exactly $B (h, k)$ .

L1algebra

1.2

The map $T (h, k) = B (h, y) + B (x, k)$ is linear in $(h, k)$ and bounded: $∥ T (h, k) ∥ \leq C ∥ h ∥ ∥ y ∥ + C ∥ x ∥ ∥ k ∥ \leq C (∥ y ∥ + ∥ x ∥) ∥ (h, k) ∥_{\max}$ by [L1] and [L2].

L1L2algebra

2.1

For $(h, k) \neq (0, 0)$ the normalised remainder is $∥ B (h, k) ∥ / ∥ (h, k) ∥_{\max} \leq C ∥ h ∥ ∥ k ∥ / ∥ (h, k) ∥_{\max} \leq C ∥ (h, k) ∥_{\max}$ , which tends to $0$ as $(h, k) \to 0$ by [L1] and [L2]; hence $D B (x, y) = T$ by [L3].

step 1.1step 1.2L1L2L3algebra

3.1

For an associative algebra multiplication that is bounded bilinear, [step 2.1] with $B = m$ gives $D m (a, b) (h, k) = m (h, b) + m (a, k) = h b + a k$ , using bilinearity to write $m (h, b) = h b$ and $m (a, k) = a k$ .

step 2.1algebra

3.2

Assume $X = Y$ . The diagonal map $d (x) : = B (x, x)$ is then the well-typed composite of $x \mapsto (x, x)$ from $X$ to $X \times X$ with $B : X \times X \to Z$ ; the diagonal is bounded linear with derivative $h \mapsto (h, h)$ , so the chain rule [L4] and [step 2.1] give $D d (x) h = D B (x, x) (h, h) = B (h, x) + B (x, h)$ .

step 2.1L4algebra

4.1

Steps 2.1, 3.1 and 3.2 establish every displayed claim of the example.

step 2.1step 3.1step 3.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

30 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Zuoqin Wang, Lecture 6 — §2.1.2 (Leibniz rule) (standard reference, not scraped)