High-contrast homogenization: Entry.Response.Kernel.SeminormHeadTailSplit #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The head/tail split of the scale-average seminorm #
The scale-average (Besov) seminorm
besovSeminorm t avg = ∑' n, 3 ^ ((t - n) / 2) √(card⁻¹ ∑_w |avg n w|²) is split at a window
depth H into a finite head and an older-scale tail, resting on the fact that the flat average of
the depth-n subcell averages recovers the parent cell average. On the good branch, each
discarded scale n beyond H carries the factor 1 + 3 ^ (ρn/2), and the resulting
3 ^ (-n/2)-weighted tail is controlled by 6/(1-ρ). This file converts that per-scale analytic
bound into the two branch bounds of Proposition p.response.transfer, the diagonal weak-norm
estimate of the response transfer, and proves the good branch's majorant is summable.
The parent cell average of a doubled field is the flat average of its subcell averages #
For an invertible grid q, a generation t and a depth n, the 3^{nd} aligned depth-n
subcells adaptedCellAtCenter q (t - n) w are pairwise disjoint open sets of equal volume,
contained
in the parent cell HighContrast.adaptedCell q t, and covering it up to the Lebesgue-null grid
seams. Consequently, for a doubled field X whose components are integrable on the parent
cell, the flat average over the index box of the subcell averages of each component equals the
parent cell average of that component.
This is the vector-valued counterpart of the scalar parent energy partition: each component of
cellAverage is a scalar volumeAverage, and the whole statement is 2 d instances of the
almost-everywhere partition identity average_over_aePartition. The equal volume of the
subcells is what makes the unweighted flat mean correct; a weighted sum would be needed without
it. Measurability, disjointness, containment and the null seam are all supplied by IsUnit q
through the cell lemmas, while the integrability of each component is an explicit hypothesis.
The parent cell average is the flat average of the subcell averages. For an invertible
grid q, generation t and depth n, each component of the parent cell average of a doubled
field X over HighContrast.adaptedCell q t equals the flat average over the 3^{nd} aligned
depth-n subcells of that component's subcell averages. Every geometric hypothesis is
discharged from IsUnit q; only the integrability of the two components on the parent cell
remains as a hypothesis.
The head/tail split of a scale-average sum, generic #
The cell-average argument splits the scale-average seminorm at the window depth H. The tree
proves that split only privately, tied to the cell-average family, so no consumer above can reuse
it. This module proves the two series facts the split rests on, for an arbitrary summable real
family: the split itself, and the geometric bound on the shifted tail. Nothing here mentions a
cell, a coefficient field, or a seminorm, so the module sits below every carrier and can be used
on either side of the estimate.
Splitting a summable real series at an index H + 1: the full sum is the finite head over
range (H + 1) plus the tail whose indices are shifted by H + 1.
The scale-average seminorm: head window plus per-scale tail #
The scale-average seminorm
besovSeminorm t avg = ∑' n, 3 ^ ((t - n) / 2) * √(card⁻¹ ∑_w |avg n w|²)
splits at the window edge H: the first H + 1 terms are the head, the older-scale terms are the
tail. The split landed here keeps every tail term intact, in the per-scale shape the energy bound
reads, rather than collapsing the tail through Jensen. Both statements are series identities
about the seminorm itself; nothing here mentions a cell, a coefficient field, or a maximizer.
besovTerm is defined in a module above this one and is deliberately not imported, so the n-th
term is spelled out here. The tail index follows tsum_split_range, namely j + (H + 1).
Normalizing by the factor 3 ^ (-(t/2)) moves the weight of the n-th scale-average term
from the paper's 3 ^ ((t - n)/2) to 3 ^ (-(n/2)).
The normalized scale-average seminorm is the finite head over range (H + 1) plus the
per-scale tail of every older term, each term kept as an individual weighted scale average.
Real arithmetic for the discarded old scales on the good branch #
Below the response window the cell-average lemma discards the scales above the cutoff H and
pays 3 ^ (-((1 - ρ) / 2) * H) for them. On the good branch each discarded scale n carries
the factor 1 + 3 ^ (ρ n / 2), so the 3 ^ (-(n / 2))-weighted tail
∑ j, 3 ^ (-(n / 2)) * (1 + 3 ^ (ρ n / 2)), with n = H + 1 + j, is controlled by
6 / (1 - ρ) times the window weight. This leaf module records the three real inequalities
realizing that step for 0 ≤ ρ < 1. No cell, matrix or measure appears.
The good-branch discarded tail: for 0 ≤ ρ < 1, the 3 ^ (-(n / 2))-weighted sum of
1 + 3 ^ (ρ n / 2) over the scales n = H + 1, H + 2, … is bounded by 6 / (1 - ρ) times
the window weight 3 ^ (-((1 - ρ) / 2) * H).
The older-scale tail of the cell-average estimate, both branches of the cutoff #
The per-scale analytic bound of the cell-average estimate is
T n ≤ √2 · K · (1 + √M · 3 ^ (ρ n / 2)) · ℰ with ρ = Quenched.contrastRho γ. This module
converts
that pointwise family bound into the two branch bounds carried by the printed tail.
On the good branch M ≤ 1 the factor √M may be dropped and the discarded old scales
n = H + 1, H + 2, … are summed with the weight 3 ^ (-(n / 2)); the sharp geometric
comparison already in the tree leaves the window factor 3 ^ (-(Quenched.contrastAlpha γ · H))
and the
constant 16 / (1 - Quenched.contrastRho γ).
On the bad branch 1 < M the whole weighted sum over all scales is absorbed; splitting
1 + √M · 3 ^ (ρ n / 2) into its two geometric parts and using 1 - Quenched.contrastRho γ = 2 · Quenched.contrastAlpha γ again leaves 16 / (1 - Quenched.contrastRho γ) · K · √M · ℰ. Only
real analysis on a
sequence appears; no cell, matrix or measure is involved.
The good branch of the older-scale tail: a nonnegative per-scale family obeying
T n ≤ √2 · K · (1 + √M · 3 ^ (ρ n / 2)) · ℰ, with M ≤ 1, has its 3 ^ (-(n / 2))
weighted tail from H + 1 on bounded by 16 / (1 - Quenched.contrastRho γ) · K · 3 ^ (-(Quenched.contrastAlpha γ · H)) · ℰ.
The bad branch of the older-scale tail: a nonnegative per-scale family obeying
T n ≤ √2 · K · (1 + √M · 3 ^ (ρ n / 2)) · ℰ, with 1 < M, has its 3 ^ (-(n / 2))
weighted sum over all scales bounded by 16 / (1 - Quenched.contrastRho γ) · K · √M · ℰ.