TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Haar cell averages approximate smooth bounded-derivative data at first order

Statement

Let $f \in S^{1}$ with $M_{1} = M_{1} (f)$ . For every integer $J \geq 0$ , with $h = 2^{- J}$ and $P_{J}$ as in Haar cell-average projection on the unit interval, ${(\int_{0}^{1} ∣ f (x) - P_{J} f (x) ∣^{2} d x)}^{1 / 2} \leq \frac{h}{\sqrt{2}} M_{1} .$ Thus the cell-average Haar approximation has first-order error on the explicit derivative-bounded smooth class $S^{1}$ .

Facts & Assumptions

Given: $f \in S^{1}$ , $M_{1} = \sup_{[0, 1]} ∣ f^{'} ∣$ , and a dyadic level $J \geq 0$ .

[F1]

Haar cell-average projection on the unit interval: on each cell $I$ of length $h$ , $P_{J} f$ equals the average ${\overset{ˉ}{f}}_{I} = h^{- 1} \int_{I} f$ .

[F2]

Smooth functions on the unit interval with bounded derivative data: $f$ is $C^{1}$ on an open interval containing $[0, 1]$ and $∣ f^{'} (x) ∣ \leq M_{1}$ there for $x \in [0, 1]$ .

[F3]

Taylor's Lagrange remainder follows from repeated Rolle steps: if $f$ is $C^{1}$ on an open interval containing $[a, b]$ , then for $x, y \in [a, b]$ there is a point between them with $f (x) - f (y) = f^{'} (ξ) (x - y)$ ; for $x = y$ the difference is zero.

Proof

1.1givenF1algebra

Fix one cell $I$ of length $h$ and put ${\overset{ˉ}{f}}_{I} = h^{- 1} \int_{I} f$ . Expanding both sides gives $\int_{I} ∣ f (x) - {\overset{ˉ}{f}}_{I} ∣^{2} d x = \frac{1}{2 h} \int_{I} \int_{I} ∣ f (x) - f (y) ∣^{2} d y d x,$ because each side equals $\int_{I} f^{2} - h^{- 1} (\int_{I} f)^{2}$ .

2.1givenF2F3step 1.1algebra

For $x, y \in I$ , [F3] and [F2] give $∣ f (x) - f (y) ∣ \leq M_{1} ∣ x - y ∣ \leq M_{1} h$ . Hence the double integral in step 1.1 is at most $h^{2} M_{1}^{2} \cdot h^{2}$ , so $\int_{I} ∣ f - {\overset{ˉ}{f}}_{I} ∣^{2} \leq h^{3} M_{1}^{2} / 2$ .

3.1step 2.1algebra∎

There are $1 / h$ cells with disjoint interiors. Summing their squared errors gives $∥ f - P_{J} f ∥_{2}^{2} \leq h^{2} M_{1}^{2} / 2$ . Taking nonnegative square roots proves the stated bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

Gilbert Strang and Kevin Amaratunga, Wavelets and Filter Banks, MIT OpenCourseWare 18.327, Handouts 3 and 9 (standard reference, not scraped)
Stéphane Mallat, A Wavelet Tour of Signal Processing, 3rd ed., Chapter 9 (standard reference, not scraped)