High-contrast homogenization: Entry.Response.Kernel.PrimalBranchSelector #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The branch selector for the normalized scale-average seminorm #
Given the per-scale bound S n ≤ √2 · K · (1 + √M · 3^(ρn/2)) · ℰ, this file proves the printed
estimate in two branches: on 1 < M the whole series is absorbed by the recent-scale weight, and
on M ≤ 1 the head/tail split applies. It records the algebraic spine of that per-scale bound,
composes it with the variance bound and the remaining analytic inputs into the per-scale tail, and
rewrites the estimate's left-hand side as a genuine besovSeminorm of a cellAverageFamily split
at the window depth. It also proves the summability the split needs for the recentred,
metric-transported cell-average family. The branch selection and the cell-average inputs serve the
diagonal weak-norm estimate of p.response.transfer.
The two branch bounds for the whole normalized scale-average seminorm #
The cell-average estimate's left-hand side is the normalized seminorm
3 ^ (-(t / 2)) * besovSeminorm t avg, i.e. ∑' n, 3 ^ (-(n / 2)) * S n with S the depth-n
scale average. Given the per-scale bound S n ≤ √2 · K · (1 + √M · 3 ^ (ρ n / 2)) · En, the
printed estimate is proved in two branches. On 1 < M the whole series is absorbed by the
older-scale term; on M ≤ 1 only the scales beyond the window H are, and the first H + 1
scales remain as an explicit head sum. Nothing here mentions a matrix or a measure: both
statements are real analysis about the family avg alone.
The normalization 3 ^ (-(t / 2)) * besovSeminorm t avg = ∑' n, 3 ^ (-(n / 2)) * S n is the
unsplit form of normalized_besovTerm; it is proved inline because the module that once
packaged it is not present, so the bad branch never needs the window split.
The two branch bounds of the cell-average estimate for the whole normalized seminorm. The
per-scale input is S n ≤ √2 · K · (1 + √M · 3 ^ (Quenched.contrastRho γ * n / 2)) · En; summing it
geometrically gives the bad-branch bound 16 / (1 - Quenched.contrastRho γ) · K · √M · En on 1 < M, and the
good-branch bound ∑_{n ≤ H} 3 ^ (-(n / 2)) S n + 16 / (1 - Quenched.contrastRho γ) · K · 3 ^ (-(Quenched.contrastAlpha γ * H)) · En on M ≤ 1.
The per-scale energy bound #
The head/tail splitting of the normalized scale-average seminorm leaves a single per-scale
estimate: the normalized L² average, over the depth-n aligned subcells, of the metric transport
of the recentred cell averages of a doubled field is bounded by √2 · K · B · ℰ, where ℰ is the
pathwise optimizer energy of the parent adapted cell.
The algebraic content is the real-arithmetic spine scaleInput_spine_le, which combines a
per-cell quadratic bound with an averaged energy bound. This module specializes that spine to the
parent optimizer energy: the averaged energy bound is the partition identity that recombines the
subcell energy averages into the squared parent energy, so the energy factor in the conclusion is
the parent pathwise energy itself.
The per-scale energy bound, from a per-cell bound and an averaged energy bound. If every
depth-n subcell adaptedCellAtCenter q (t - n) w bounds the quadratic metric form of the
transported
cell average R (X)_w by (K B)^2 times a nonnegative energy density G w, and if the flat
average of G over the subcells is at most 2 En^2, then the flat L² average of the transported
cell averages is at most √2 · K · B · En.
This is the spine scaleInput_spine_le at load En and defect 1; the factor √1 = 1 is
discarded.
The composed per-scale tail bound #
At depth n the older-scale tail of the cell-average estimate compares the transported recentred
subcell averages of the doubled optimizer field with the transported parent cell average. This
module composes the per-scale energy bound scaleEnergy_of_analytic with the two remaining
analytic inputs:
- the variance bound
hvar, which majorizes the recentred flatL²average by the uncentred one; - the per-cell energy bound
hcelland the parent partition identityhpart, which supply the averaged energy bound of the spine.
The result is the tail estimate √(card⁻¹ ∑ |R((X)_w − (X)_U)|²) ≤ √2 · K · B · ℰ, where ℰ is
the pathwise optimizer energy of the parent adapted cell.
The composed per-scale tail bound. Suppose the recentred flat L² average of the
transported subcell averages is at most the uncentred one, each transported subcell average
satisfies the quadratic bound against (K B)^2 times twice its subcell energy average, and the flat
average of the subcell energy averages equals the squared parent pathwise energy ℰ^2. Then the
transported recentred tail is at most √2 · K · B · ℰ.
The left-hand side of the cell-average estimate, public #
The cell-average estimate has left-hand side
3 ^ (-(t / 2)) * besovSeminorm t (fun n w => blockMatVecMul A (cellAverageFamily q t X n w - c)),
and its argument needs that quantity rewritten as a besovSeminorm of a genuine
cellAverageFamily and then split at the window depth. RecentEnergyMapSupport.lean
contains both steps, but private, so no consumer above that module can reach them. This module
lands public copies.
The recentring here asks integrability only on the cells the seminorm actually reads,
w ∈ triadicIndexBox d n, rather than on every label; that is exactly the hypothesis
besovSeminorm_congr needs.
Main results #
cellAverage_blockMatVecMul: the cell average commutes with block transport.cellAverage_sub_const: the cell average of a recentred field.
The cell average commutes with the block transport: averaging the transported field is the
transport of the averaged field. Integrability is asked componentwise on V.
The cell average of a recentred field is the recentred cell average, provided the cell has finite and nonzero volume so that the constant integrates to itself.
Summability of the recentred, metric-transported cell-average family #
The scale-average seminorm besovSeminorm is a real tsum, so every identity that splits it
needs its family to be summable. The tree already proves the needed summability above the
cell-average estimate in ResponseWeakEstimateBasics.lean, but that module sits above the
estimate in
public import order, so the estimate cannot reach it. This module re-lands the same fact below
it, on
the two public cell-average identities of PrimalBranchSelector.lean.
The engine is summable_besov_cellAverageFamily (ScaleAverageSeminorm.lean): for the transported
recentring x ↦ A (X x - ⟨X⟩_{U_t}) the family of cell averages is summable as soon as the
transported field is in L² on U_t; the recentred family of the statement is that family,
restricted to the labels w ∈ triadicIndexBox d n the seminorm reads.
The second statement is the unsplit normalisation of the seminorm: pulling the factor
3 ^ (-(t/2)) inside the tsum moves the weight of the n-th term to 3 ^ (-(n/2)). It is a
series identity and needs no summability.
Local helpers #
These are the L²-to-integrability ingredients of the proof. They are not imported because the
copies in ResponseWeakEstimateBasics.lean are private and that module is above this one in
import
order. The cell-average identities themselves are the public
cellAverage_blockMatVecMul and cellAverage_sub_const.
The summability half. The recentred, metric-transported cell-average family of an
L²(U_t) block field is summable with the scale weights of the seminorm. The engine
summable_besov_cellAverageFamily is applied to the transported recentring
X' = x ↦ A (X x - ⟨X⟩_{U_t}); on the read cells the cell average of X' is the transported
recentred cell average, by the two public cell-average identities.