High-contrast homogenization: Provider.Quenched.EndpointRelativeTransport

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

Endpoint-relative coefficient transport

The physical-scale coefficient used by the quenched row is the same quotient pullback as the coefficient-space triadic dilation used to define the rebased law. This identifies endpoint-relative tail estimates under the mapped law with their pullbacks to the original law.

theorem HCPolySupport.HighContrast.Quenched.physical_scale_coeff_eq_triadicDilation {d : ℕ} (N : ℕ) (a : CoeffSpace d) : physicalScaleCoefficient N a = CoeffSpace.triadicDilation N a

The two quotient-level realizations of triadic coefficient dilation agree.

theorem HCPolySupport.HighContrast.Quenched.triadicRebasedSource_physical_scale_coeff {d : ℕ} (N : ℕ) (S : CoeffSpace d → ℝ) (a : CoeffSpace d) : triadicRebasedSource N S (physicalScaleCoefficient N a) = S a / 3 ^ N

The source in endpoint units evaluates to the restored source divided by the endpoint dilation factor.

theorem HCPolySupport.HighContrast.Quenched.measureReal_triadicRebasedLaw_upperTailEvent {d : ℕ} (N : ℕ) {P : MeasureTheory.Measure (CoeffSpace d)} {F : CoeffSpace d → ℝ} (hF : Measurable F) (t : ℝ) : (triadicRebasedLaw N P).real {a : CoeffSpace d | t < F a} = P.real {a : CoeffSpace d | t < F (physicalScaleCoefficient N a)}

A measurable strict upper-tail event under the endpoint-rebased law is exactly its physical-coefficient pullback under the original law.