High-contrast homogenization: Entry.ScaleSelection #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Scale selection #
The type repeats the p.scale.selection statement
(HCPoly/Entry/Statements/ScaleSelection.lean, p.scale.selection): same binders, same binder
kinds and order, the same conclusion ∃ S : SelectionData, S.Selects d γ, and no
additional hypothesis.
The five guarded alternatives are proved in HCPoly/Entry/Multiscale/ScaleSelection/, one printed
step per file; this file only chooses the selection data and the two outermost constants
C(d,γ) and C_src(d,γ) before the law, the geometry, ε, σ and B, as the statement
requires, and dispatches the five cases of alternatives_exhaustive. It consumes the
two applications of Entry.fixed_geometry_one_grid_propagation
(HCPoly/Entry/OneGridPropagation.lean) and Entry.two_grid_transport
(HCPoly/Entry/TwoGridTransport.lean), together with
Entry.successful_short_bridge.
Proof of p.scale.selection, repeating the type of
HCPolySupport.HighContrast.scale_selection (HCPoly/Entry/Statements/ScaleSelection.lean,
p.scale.selection)
byte for byte. Assembled from the five alternative lemmas with h = 2Q, c = c₀,
L(ε,σ) = selectionLength L₀ σ, B₀(ε,σ) = max 1 (max (B₀^bridge (√ε σ) L) (2 C_tr (L+1))),
C above 2Q C₁ and 2 C_tr, Csrc := max Csrc₁ (max Csrc₂ Csrc₃) of the three
immediately consumed source constants, and ε₀ from exists_eps0.