High-contrast homogenization: Entry.Multiscale.ScaleSelection.BridgeApplication #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The short bridge, old-grid smallness and scale separation #
Group D of the printed proof (p.scale.selection), second part: the short
bridge applied at tolerance √ε σ with the chosen length, the smallness of the old-grid
profile at the doubled length, and the scale separation
C_tr (L + log₃((2+Π)(‖m‖‖m⁻¹‖))) ≤ n - j_* that the transport step consumes
(the condition actually proved below and supplied to TransportBody; C(L+1) ≤ n - j_*
concerns the choice of B₀, not the transport hypothesis).
Part of the proof of
HCPoly/Entry/Statements/ScaleSelection.lean. Conventions of the group: q = 𝒬(𝔪) is
Geometry.explicitRoundedGrid jStar m; the printed data are h = 2Q, c = c₀,
L(ε,σ) = selectionLength L₀ σ and
B₀(ε,σ) = max 1 (max (B₀^bridge (√ε σ) L) (2 C_tr (L+1))); √ε is the printed
ε^{1/2}; the source lower scale e.source.lower.scale is carried wherever
j_* appears with the law, and no integrability, finiteness or
measurability premise is added anywhere. Unused hypothesis binders of a statement are
underscore-prefixed; the tree compiles with -DwarningAsError=true.
The declaration text of this file is the closed skeleton's, copied unchanged; only this header, the imports and the namespace frame are new.
p.scale.selection: in the change-of-geometry case the short bridge applies at tolerance
ε^{1/2}σ with the chosen length, giving the two Loewner comparisons.
p.scale.selection: the old-grid smallness 𝒫_q(n+2L;k)+D(n+2L) ≤ 3^{−½(1−γ)L}ρ from the
one-grid fixed-span propagation at span 2L, the determinant bound and the smallness of ε.
p.scale.selection: the transport scale separation at the chosen data.