High-contrast homogenization: Provider.Transport.NearIsometry

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The near-isometric comparison of the transport

This is the second half of the matrix calculation the proof of p.two.grid.transport isolates and uses at every target cell. The convex combination P_bar of the previous module lives on the old grid; the target cell lives on the new one, and the two normalizations differ by the bridge congruence S. The display e.two.grid.whitney.mean.bound says that transporting P_bar costs a factor depending only on d and Q plus one additive multiple of the bridge error — the error never multiplies the gain.

The mechanism is the splitting S^tP_barS - I = S^t(P_bar - I)S + (S^tS - I). The first term is positive and its trace is at most (1 + η)tr(P_bar - I); the second is bounded above by η times the identity. So the whole matrix is dominated by a positive matrix of trace at most (1 + η)tr(P_bar - I) + 2dη, and the trace of a spectral positive part is at most the trace of any positive matrix above it.

The passage from the trace bound to the gain bound is scalar and uses the convexity of the gain twice: once to absorb the factor 1 + 2dη into a constant, and once to see the remaining (1 + 2dη)^Q - 1 as a multiple of η.

theorem HCPolySupport.HighContrast.Transport.trace_gap_eq_trace_posPart {d : ℕ} {Mblk Phat : BlockMat d} (hPhat : toFullBlockMat Phat = 1 + toFullBlockMat (blockPosPart Mblk)) : blockTrace Phat - 2 * ↑d = (cfc (fun (x : ℝ) => max x 0) (toFullBlockMat Mblk)).trace

The trace gap of the transported block is the trace of the positive part.