High-contrast homogenization: Provider.Quenched.CoupledPhysicalScale #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Physical scale from a coupled mixing witness #
This module restores the microscopic source, combines it with the selected mixing scale, and proves the strict two-part tail and physical all-later row estimate. The mixing tail and bad-event certificate are consumed from one coupled witness.
theorem
HCPolySupport.HighContrast.Quenched.exists_coupled_physical_outer_constants
(cMix Crebase Cann Cmix : ℝ)
:
Deterministic outer constants can simultaneously absorb the rebase cost, the annealed and mixing length exponents, and the two strict tail thresholds.
theorem
HCPolySupport.HighContrast.Quenched.exists_physical_scale_of_coupled_mixing_witness
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
[NeZero d]
[MeasureTheory.IsProbabilityMeasure P]
{g : ℝ}
{E : BlockMat d}
{Psi : ℝ → ℝ}
{K : ℝ}
{S : CoeffSpace d → ℝ}
(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))⁻¹) ∧ ∀ᵐ (a : CoeffSpace d) ∂P, HasAllLaterPhysicalBlockRow rho kappa C Abar S X a
Restore the microscopic source and assemble the physical replay length, random scale, strict two-part tail, and all-later block-row estimate.