High-contrast homogenization: Entry.Response.Rows.CutoffMeanDefectIntegrability #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Coordinatewise integrability of the cutoff-mean defect #
For the cutoff-mean row of the cutoff estimate in p.response.transfer, the annealed cutoff-mean
defect splits, coordinate by coordinate, into a cell part and an oscillation part. Four families of
P-integrability feed that split — the terminal cell mean of the optimizer state, its depth-H
cell part, the cutoff-weighted mean, and the oscillation part itself — and this file proves all
four, for both the minus and the plus sign, from the integrability established for the oscillation
half of the row. A short auxiliary fact about the vanishing of a pairing against the zero vector
closes one of the coordinate cases.
The cutoff-mean defect is integrable in every coordinate #
The cutoff-mean row of p.response.transfer splits the annealed cutoff-mean defect, coordinate by
coordinate, into a cell part and an oscillation part. Four families of P-integrabilities feed
that split: the terminal cell mean, the depth-H cell part, the cutoff-weighted mean and the
oscillation part. All four come from the oscillation half of the row read at the 2d basis dual
vectors: at Y = (0, δ_i) the crossed scalar ⟨Y₂, ∇u⟩ + ⟨Y₁, a ∇u⟩ collapses to (∇u)_i and at
Y = (δ_i, 0) to (a ∇u)_i, so the annealed functional of the half is the (φ-1)-weighted mean
of one coordinate, and the Fenchel probe of CellOscillationSplit makes the unweighted cell means
integrable on every aligned cell. The source-load series converges at every dual vector
(OptimizerMeanRowCarriers), so the 2d instantiations are legitimate.
The four coordinate integrabilities of the cutoff-mean defect, minus sign. The terminal
cell mean, the depth-H cell part, the cutoff-weighted mean and the oscillation part of each
coordinate of the terminal optimizer state are P-integrable.
The four coordinate integrabilities of the cutoff-mean defect, plus sign. The adjoint
twin of integrable_cutoffMeanDefect_coords_respCoeffMinus.