High-contrast homogenization: Provider.Quenched.CoupledMixingScaleEngineAdapter

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

Coupled witness from the quenched bad-tail engine

The stopping engine selects one random scale together with its marginal tail and its all-later bad-event certificate. This module places those outputs, the weighted row series, and the final normalizer in the dependent structure consumed by the physical-scale argument.

theorem HCPolySupport.HighContrast.Quenched.three_mul_le_rpow_of_le_rpow {base A Cstop Cround Cmix : ℝ} (hbase : 1 ≤ base) (hA : 0 ≤ A) (hthree : 3 ≤ base ^ Cround) (hstop : A ≤ base ^ Cstop) (hcost : Cround + Cstop ≤ Cmix) : 3 * A ≤ base ^ Cmix

A second factor of three can be absorbed by one additional polynomial cost, with the three exponent costs combined additively.

def HCPolySupport.HighContrast.Quenched.coupledMixingScaleWitnessOfSelectedEngine {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} {B F : ℕ → Omega → ℝ} {cMix cd eta kappa delta Astop Amix : ℝ} {Rmix : Omega → ℝ} (hAstop : 1 ≤ Astop) (hAmix : 1 ≤ Amix) (hbuffer : 3 * Astop ≤ Amix) (hRmixMeasurable : Measurable Rmix) (hRmixOne : ∀ (a : Omega), 1 ≤ Rmix a) (hRmixTail : ∀ (t : ℝ), 1 ≤ t → P.real {a : Omega | cMix * t ≤ Rmix a} ≤ Real.exp (-cd * t ^ eta)) (hBNonnegative : ∀ (m : ℕ) (a : Omega), 0 ≤ B m a) (hFsum : ∀ᵐ (a : Omega) ∂P, ∀ (n : ℕ), HasSum (fun (j : ℕ) => 3 ^ (kappa * ↑j) * B (n + j) a) (F n a)) (hBadMeasurable : ∀ (n : ℕ), MeasurableSet (rowBadEvent delta F n)) (hcertificate : ∀ᵐ (a : Omega) ∂P, ∀ (n : ℕ), Astop * Rmix a ≤ 3 ^ n → a ∉ rowBadEvent delta F n) : CoupledMixingScaleWitness P B cMix cd eta kappa delta

Package one selected scale, its row series, and its own bad-event certificate into the coupled witness used by the physical-scale argument.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.Quenched.exists_coupledMixingScaleWitness_of_polynomial_engine {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {nstar qfb b : ℕ} {R B F : ℕ → Omega → ℝ} {theta mu eta cd delta Cblk base C1 C2 C3 Cstop Cround Cmix : ℝ} (htheta : 0 < theta) (hmu : 0 < mu) (heta : eta = 2 * mu) (hcd : 0 < cd) (hdelta : 0 < delta) (hCblk : 0 < Cblk) (hFmeas : ∀ (n : ℕ), Measurable (F n)) (hRtail : ∀ (n q : ℕ), nstar ≤ n → P.real {a : Omega | 3 ^ (n + q + b) < R n a} ≤ Real.exp (-(cd * 3 ^ (2 * mu * ↑q)))) (hBdecay : ∀ᵐ (a : Omega) ∂P, ∀ (m : ℕ), nstar ≤ m → B m a ≤ Cblk * delta * 3 ^ (-theta * (↑m - ↑(stoppingGeneration nstar qfb R m a) - ↑nstar))) (hBNonnegative : ∀ (m : ℕ) (a : Omega), 0 ≤ B m a) (hFsum : ∀ᵐ (a : Omega) ∂P, ∀ (k : ℕ), HasSum (fun (j : ℕ) => 3 ^ (theta / 2 * ↑j) * B (k + j) a) (F k a)) {N0 : ℕ} {Bconst : ℝ} (hstar : nstar ≤ N0) (hBconst : 1 ≤ Bconst) (hN0low : ↑qfb + ↑b + 1 + rowSplitOffset theta Cblk ≤ ↑N0 - ↑nstar) (hN0gain : Real.log 2 ≤ cd * 3 ^ (2 * mu * (↑N0 - ↑nstar - badTailOffset theta Cblk qfb b)) * (3 ^ (mu / 2) - 1)) (hN0abs : 2 * Real.log 4 ≤ cd * 3 ^ (2 * mu * (↑N0 - ↑nstar - badTailOffset theta Cblk qfb b))) (hBrel : 3 ^ (2 * mu * (↑nstar + badTailOffset theta Cblk qfb b - ↑N0)) ≤ cd / 2 * Bconst ^ (2 * mu)) (hbase : 1 ≤ base) (hthree : 3 ≤ base ^ C3) (hgen : 3 ^ N0 ≤ base ^ C1) (hnorm : Bconst ≤ base ^ C2) (hrawCost : C1 + C2 + C3 ≤ Cstop) (hround : 3 ≤ base ^ Cround) (hfinalCost : Cround + Cstop ≤ Cmix) : ∃ (W : CoupledMixingScaleWitness P B 2 1 eta (theta / 2) delta), W.normalization ≤ base ^ Cmix

The polynomial bad-tail engine supplies the complete dual-normalizer coupled witness. The raw engine normalizer is used for its certificate; one additional factor of three is absorbed into the final replay normalizer.