Pipeline-generated

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.

✓ 3 results · all verified · 3 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 3 also cleared it.

Wavelet transforms and nonlinear approximation — Examples

1 · Prerequisites

2 · Summary

These examples compute a finite Haar compression, compare two explicitly defined endpoint-padding rules, and contrast soft shrinkage with optimal hard m-term retention. Each computation uses the A-page conventions and gives the exact coefficient and error values.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Periodic and symmetric padding give different Haar coefficients

Example

Start with the odd-length data $(0, 0, 1)$ . Define two explicit padding rules to length four. Periodic endpoint padding appends the first entry, giving $x_{P} = (0, 0, 1, 0)$ . Symmetric endpoint padding repeats the final entry, giving $x_{S} = (0, 0, 1, 1)$ . Applying the first Haar stage to the last pair gives $(a, d) = (1 / \sqrt{2}, 1 / \sqrt{2})$ for $x_{P}$ and $(a, d) = (\sqrt{2}, 0)$ for $x_{S}$ . The coefficients change because the boundary rule changes the pair presented to the filter.

Verification

Given: The two length-four padded vectors above and the Haar pair map of Finite periodic Haar transform.

[F1] Finite periodic Haar transform: a pair $(u, v)$ maps to $((u + v) / \sqrt{2}, (u - v) / \sqrt{2})$ .

1.1givenF1algebra

For the periodic padding, the last pair is $(1, 0)$ ; substitution gives average $(1 + 0) / \sqrt{2} = 1 / \sqrt{2}$ and detail $(1 - 0) / \sqrt{2} = 1 / \sqrt{2}$ .

2.1givenF1step 1.1algebra∎

For the symmetric padding, the last pair is $(1, 1)$ ; substitution gives average $(1 + 1) / \sqrt{2} = \sqrt{2}$ and detail $(1 - 1) / \sqrt{2} = 0$ . The two coefficient pairs differ.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Exact two-coefficient Haar compression of a four-entry step vector

Example

For the four-entry step vector $x = (1, 1, 0, 0)$ , the finite periodic Haar transform has coefficient vector $(1, 1, 0, 0)$ in the order “coarse average, coarsest detail, finest details.” Retaining the first two coefficients reconstructs $x$ exactly. Among one-coefficient approximations the squared error is $1$ .

Verification

Given: $x = (1, 1, 0, 0)$ and the transform convention of Finite periodic Haar transform.

[F1] Finite periodic Haar transform: each pair $(u, v)$ maps to average/detail $((u + v) / \sqrt{2}, (u - v) / \sqrt{2})$ , and output order is coarse coefficient followed by detail blocks from coarse to fine.

[F2] Orthogonality, inverse, and Parseval identity for the finite periodic Haar transform: the transform is orthogonal with inverse transpose and preserves squared Euclidean norm.

[F3] Hard m-term retention is optimal for an orthonormal coefficient basis: keeping $m$ largest coefficients is best among all $m$ -coefficient reconstructions and squared error is the discarded squared sum.

1.1givenF1algebra

The first pair $(1, 1)$ yields approximation $\sqrt{2}$ and detail $0$ ; the second pair $(0, 0)$ yields approximation and detail $0$ . Transforming the remaining approximation pair $(\sqrt{2}, 0)$ gives coarse coefficient $1$ and coarsest detail $1$ . In the declared ordering the full vector is therefore $(1, 1, 0, 0)$ .

2.1givenF2F3step 1.1algebra∎

Keeping the two nonzero coefficients gives the original vector by the inverse in [F2]. Keeping only one leaves one coefficient of magnitude $1$ discarded; [F3] gives squared error $1$ .

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Soft thresholding shrinks a retained coefficient while hard best-m retention does not

Example

In the standard orthonormal basis, let $c = (3, 1)$ , choose $m = 1$ , and use soft threshold $λ = 1$ . Hard best-1 retention gives $(3, 0)$ and error norm $1$ . Soft thresholding gives $(2, 0)$ and error norm $\sqrt{2}$ : it both shrinks the retained coefficient and discards the smaller one.

Verification

Given: $c = (3, 1)$ , $m = 1$ , $λ = 1$ , and the standard orthonormal basis $U = I_{2}$ .

[F1] Hard m-term retention and soft thresholding of finite coefficients: $H_{m}$ keeps the $m$ largest absolute coordinates, while $S_{λ} (c)_{i} = sign (c_{i}) (∣ c_{i} ∣ - λ)_{+}$ .

[F2] Hard m-term retention is optimal for an orthonormal coefficient basis: hard retention has squared error equal to the discarded squared-coefficient sum and is best among one-term approximations.

1.1givenF1F2algebra

The coordinate magnitudes are $3 > 1$ , so [F1] gives $H_{1} (c) = (3, 0)$ . The discarded coordinate is $1$ , hence [F2] gives hard squared error $1$ .

2.1givenF1step 1.1algebra∎

The soft formula gives $S_{1} (c) = (2, 0)$ . Its residual is $(1, 1)$ , whose squared norm is $1^{2} + 1^{2} = 2$ , so the soft error norm is $\sqrt{2} > ⁣ 1$ .

Wavelet transforms and nonlinear approximation — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Periodic and symmetric padding give different Haar coefficients

Example

Verification

Exact two-coefficient Haar compression of a four-entry step vector

Example

Verification

Soft thresholding shrinks a retained coefficient while hard best-m retention does not

Example

Verification

Sources