High-contrast homogenization: Provider.Quenched.EndpointRelativeEngineData

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

Endpoint-relative coupled-engine data

The coefficient law is first read in the units of the annealed endpoint. Growing recent windows then give a radius family with a uniform shifted tail, while the same family controls the physical block row after pulling it back to the original coefficient law.

theorem HCPolySupport.HighContrast.Quenched.exists_coupledWitnessEngineData_of_endpoint (d : ℕ) (hd : 2 ≤ d) (g : ℝ) : g ∈ Set.Ico 0 1 → ∀ (alpha : ℝ), 0 < alpha → ∃ (Cmix : ℝ) (theta : ℝ) (deltaOut : ℝ), 0 < Cmix ∧ 0 < theta ∧ deltaOut ∈ Set.Ioo 0 1 ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Psi : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (Abar : BlockMat d) (Nann : ℕ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Psi K S → IsSymmetricBlockMat Abar → Book.Ch02.BlockPosDef Abar → (∀ (j : ℕ), annealedContrast P ↑(Nann + j) - 1 ≤ 3 ^ (-alpha * ↑j)) → (∀ (j : ℕ), BlockMatLoewnerLE Abar (annealedBlock P (centeredCube d ↑(Nann + j))) ∧ BlockMatLoewnerLE (annealedBlock P (centeredCube d ↑(Nann + j))) (blockScale (1 + 6 * 3 ^ (-alpha * ↑j)) Abar)) → Nonempty (CoupledWitnessEngineData P g E Psi K S Abar Nann theta deltaOut Cmix)

The endpoint-relative renormalization family supplies the complete datum consumed by the coupled witness assembly.