High-contrast homogenization: Provider.Quenched.CoupledQuenchedMinimalScale #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The coupled quenched minimal scale #
The physical replay scale controls two different constants. Its tail uses an outer dimensional constant, while the block row retains the small threshold selected before the law. Keeping the latter coefficient avoids losing the entry-scale smallness when the strict source tail and the mixing tail are combined.
theorem
HCPolySupport.HighContrast.Quenched.exists_quenched_minimal_scale_of_coupled_witness
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
[NeZero d]
[MeasureTheory.IsProbabilityMeasure P]
{g : ℝ}
{E : BlockMat d}
{Psi : ℝ → ℝ}
{K : ℝ}
{S : CoeffSpace d → ℝ}
(hstationary : IsStationaryLaw P)
(hdagger : CoarseEllipticityDagger P g E Psi K S)
{rho cMix cd eta kappa delta Cann Cmix C cSrc : ℝ}
{Abar : BlockMat d}
{N : ℕ}
(W :
CoupledMixingScaleWitness P
(fun (m : ℕ) (a : CoeffSpace d) => quenchedBlockRow rho Abar (max 1 (S a / 3 ^ N)) (physicalScaleCoefficient N a) m)
cMix cd eta kappa delta)
(hkappa : 0 < kappa)
(hdelta : delta ∈ Set.Ioo 0 1)
(hN : 3 ^ N ≤ (2 + aspectRatio E * K) ^ Cann)
(hW : W.normalization ≤ (2 + aspectRatio E * K) ^ Cmix)
(habsorb : Cann + Cmix ≤ C)
(hC : 1 < C)
(hcMix : cMix ≤ C)
(hcSrcOne : 1 < cSrc)
(hcSrcC : cSrc < C)
:
∃ (Lpoly : ℝ) (Ssrc : CoeffSpace d → ℝ) (X : CoeffSpace d → ℝ),
Lpoly = coupledPhysicalLength N W ∧ (∀ (a : CoeffSpace d), Ssrc a = max 1 (S a / 3 ^ N)) ∧ (∀ (a : CoeffSpace d), X a = Lpoly * max 1 (max (W.scale a) (Ssrc a))) ∧ 1 ≤ Lpoly ∧ Lpoly ≤ (2 + aspectRatio E * K) ^ C ∧ Measurable Ssrc ∧ (∀ (a : CoeffSpace d), 1 ≤ Ssrc a) ∧ Measurable X ∧ (∀ (a : CoeffSpace d), 1 ≤ X a) ∧ (∀ (t : ℝ),
1 ≤ t →
P.real {a : CoeffSpace d | C * Lpoly * t ≤ X a} ≤ Real.exp (-cd * t ^ eta) + (Psi (cSrc * t))⁻¹) ∧ ∃ (OmegaEnd : Set (CoeffSpace d)),
MeasurableSet OmegaEnd ∧ P.real OmegaEnd = 1 ∧ (∀ (z : Fin d → ℤ), translateCoeff z ⁻¹' OmegaEnd = OmegaEnd) ∧ ∀ a ∈ OmegaEnd, HasAllLaterPhysicalBlockRow rho kappa delta Abar S X a
With fixed outer constants, the coupled witness gives a measurable quenched scale with the strict two-part tail and, on one invariant full-measure event, the small block row at entry together with its algebraic decay.