UnbalancedHaarWavelet

Read the PDF documentation

Lean 4 formalization of unbalanced Haar wavelets on finite measure spaces with nested finite measurable partitions, following the construction of Girardi and Sweldens (1997).

The development now covers the full pipeline from grids and induced binary refinements to real and complex unconditional Schauder basis theorems in L^p, including explicit coefficient formulas for the resulting Haar expansions.

Main Results

For a grid G and a chosen full Haar system F, the project formalizes:

1. Existence of binary refinements of grid cells with at least two children.
2. Construction of local unbalanced Haar wavelets from branch splits.
3. The full Haar family, consisting of the normalized father function and all wavelets.
4. Orthogonality of distinct full Haar functions and explicit L^2 square norms.
5. Linear-combination identities showing that grid-cell indicators lie in the span of the full Haar system.
6. Density of the full Haar family in real and complex L^p.
7. A filtration and partition-average martingale attached to the induced unary-binary grid.
8. Burkholder finite-sign estimates for finite Haar sums.
9. Abstract-index unconditional Schauder basis theorems for real and complex L^p, for every 1 < p < infinity.
10. Nat-indexed basis theorems when the full Haar index type is countably infinite.
11. Concrete coefficient formulas: coeff_i(f) = integral f phi_i dmu / ||phi_i||_2^2, together with uniqueness and expansion results.

The preferred final real theorem is exists_fullHaarSystem_unconditionalSchauderBasisAbstractIndex_Real. The preferred final complex theorem is exists_fullHaarSystem_unconditionalSchauderBasisAbstractIndex_Complex. The coefficient expansion theorem is FullHaarSystem.hasSum_coeff_of_memLp.

Mathematical Roadmap

1. Grids

A Grid consists of a finite measure, a nested sequence of finite measurable partitions, and positive mass for every partition cell. The partition sequence starts with {univ}, covers the space at every level, has pairwise disjoint cells at each level, refines from one level to the next, and generates the ambient measurable space.

The current formal Grid structure does not assume a separate measure-decrease axiom along refinement chains. Positivity and finiteness provide the normalization facts needed in the Haar construction.

2. Binary Refinements

For every grid cell with at least two children, the project chooses a finite binary tree whose leaves/tops are exactly those children. Cells with only one child are treated as degenerate nonsplitting nodes. This is packaged by BinaryRefinementOfGrid and supplied by the external LaminarFamiliesMaximalBinaryTrees dependency.

3. Haar Systems

Given a branch split (L, R) of child collections, the corresponding Haar wavelet is

1_{support(L)} / mu(support(L)) - 1_{support(R)} / mu(support(R)).

The full Haar system adds the normalized father function 1_univ / mu(univ). Its index type is an inductive type with one father index and one constructor for ordinary wavelet indices.

4. Orthogonality and Coefficients

The development proves zero mean for wavelets, pairwise orthogonality of distinct globally indexed Haar wavelets, father-wavelet orthogonality, and orthogonality for distinct full Haar indices.

It also defines explicit square norms and coefficients:

||psi_(L,R)||_2^2 = 1 / mu(L) + 1 / mu(R)
coeff_i(f) = integral f phi_i dmu / ||phi_i||_2^2.

Finite sums recover their coefficients, and L^p Haar expansions have these concrete coefficients.

5. Density

The proof that the full Haar family is dense in L^p proceeds by showing that indicators of grid cells belong to the Haar span, then applying the fact that the grid partitions generate the measurable space. Both real and complex versions are formalized.

6. Martingales and Burkholder Estimates

The induced unary-binary grid defines finite partitions at each deepness level and hence a filtration. Partition averages form a Mathlib martingale. The one-step martingale increments are either zero at degenerate nodes or the projection coefficient times the corresponding Haar wavelet at genuine binary nodes.

Finite Haar sums are identified with martingale transforms, and Burkholder's martingale-transform inequality gives the finite-sign bounds used by the abstract unconditional-basis criterion.

7. Unconditional Schauder Bases

The final step applies the external UnconditionalSchauderBasis criterion: dense span, nonzero vectors, and finite-sign bounds imply an unconditional Schauder basis.

There are two kinds of final statements:

• Abstract-index theorems, indexed by F.Index. These are the preferred statements and do not require the index type to be infinite.
• Nat-indexed theorems. These choose an enumeration Nat equiv F.Index and therefore require [Countable F.Index] [Infinite F.Index].

Both real and complex versions are present. In the complex finite-sign estimate, the constant is twice the real one because the proof splits coefficients into real and imaginary parts.

Repository Structure

• UnbalancedHaarWavelet/GridDefinition.lean

  • Nested finite partition sequences, grids, children of cells, and the binary-refinement structure.

• UnbalancedHaarWavelet/HaarWaveletsDefinition.lean

  • Branch supports, Haar wavelets, Haar systems, full Haar systems, and global index types.

• UnbalancedHaarWavelet/HaarWaveletsInducedBinaryGrid.lean

  • Support laminarity, global support injectivity, deepness chains, and induced unary-binary grid infrastructure.

• UnbalancedHaarWavelet/HaarWaveletsOrthogonality.lean

  • Integrability, zero-mean, square-norm, and orthogonality results.

• UnbalancedHaarWavelet/HaarWaveletsLinearCombinations.lean

  • Refinement-tree linear identities and proofs that grid-cell indicators lie in the full Haar span.

• UnbalancedHaarWavelet/HaarWaveletsDenseSpan.lean

  • Real and complex L^p span definitions and density theorems.

• UnbalancedHaarWavelet/HaarWavelets_def_Martingale.lean

  • Filtrations, partition-average martingales, projection coefficients, martingale-transform identities, and Burkholder estimates.

• UnbalancedHaarWavelet/HaarWaveletsUnconditionalBasis.lean

  • Finite-sign bounds in L^p, real and complex unconditional basis theorems, and abstract-index / Nat-indexed variants.

• UnbalancedHaarWavelet/HaarWaveletsCoeffs.lean

  • Explicit Haar coefficient formulas, coefficient recovery, and full L^p expansion with concrete coefficients.

• docs/Documentation.tex

  • Mathematical write-up of the formalization.

Dependencies

The project depends on:

• mathlib
• LaminarFamiliesMaximalBinaryTrees
• Burkholder
• UnconditionalSchauderBasis

See lakefile.toml and lake-manifest.json for pinned versions.

Commands

Build the project:

lake build

Check one file:

lake env lean UnbalancedHaarWavelet/HaarWaveletsUnconditionalBasis.lean

Run the local proof-sanity script:

scripts/check-proof-sanity.sh

Reference

Maria Girardi and Wim Sweldens, A New Class of Unbalanced Haar Wavelets That Form an Unconditional Basis for L^p on General Measure Spaces, Journal of Fourier Analysis and Applications, 3(4), 1997. DOI: 10.1007/BF02649107

Status

This repository is part of a broader formalization program around wavelets on general measure spaces, with future targets including Besov-space applications and transfer-operator methods.

Contributor

Daniel Smania