High-contrast homogenization: Provider.Quenched.QuenchedPolynomialNormalizer

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

The polynomial cost of the mixing normalizer

The normalizer of the mixing scale is the product of the base generation and the gauge normalizer. Its polynomial cost is additive in the exponents, exactly as the reference length of the homogenization statement is: three separate exponents are useless, their sum is what must be admissible. This file records that absorption, the resulting mixing-scale witness carrying its own polynomial bound, and an explicit admissible pair for which the two constituent bounds are checkable.

Additive absorption of the three polynomial costs

theorem HCPolySupport.HighContrast.Quenched.three_mul_pow_mul_le_rpow {base Bconst C1 C2 C3 Cmix : ℝ} {N0 : ℕ} (hbase : 1 ≤ base) (hBnonneg : 0 ≤ Bconst) (hthree : 3 ≤ base ^ C3) (hgen : 3 ^ N0 ≤ base ^ C1) (hnorm : Bconst ≤ base ^ C2) (hsum : C1 + C2 + C3 ≤ Cmix) : 3 * 3 ^ N0 * Bconst ≤ base ^ Cmix

The three polynomial costs of the mixing normalizer are absorbed by the sum of their exponents; requiring each separately is not enough.

The mixing-scale witness with its polynomial cost

theorem HCPolySupport.HighContrast.Quenched.exists_coupled_mixingScale_polynomial {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {nstar qfb b : ℕ} {R B F : ℕ → Ω → ℝ} {theta mu eta cd delta Cblk base C1 C2 C3 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 {ω : Ω | 3 ^ (n + q + b) < R n ω} ≤ Real.exp (-(cd * 3 ^ (2 * mu * ↑q)))) (hBdecay : ∀ᵐ (ω : Ω) ∂P, ∀ (m : ℕ), nstar ≤ m → B m ω ≤ Cblk * delta * 3 ^ (-theta * (↑m - ↑(stoppingGeneration nstar qfb R m ω) - ↑nstar))) (hFsum : ∀ᵐ (ω : Ω) ∂P, ∀ (k : ℕ), HasSum (fun (j : ℕ) => 3 ^ (theta / 2 * ↑j) * B (k + j) ω) (F k ω)) {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) (hsum : C1 + C2 + C3 ≤ Cmix) : ∃ (Amix : ℝ) (Rmix : Ω → ℝ), 1 ≤ Amix ∧ Amix ≤ base ^ Cmix ∧ Measurable Rmix ∧ (∀ (ω : Ω), 1 ≤ Rmix ω) ∧ (∀ (t : ℝ), 1 ≤ t → P.real {ω : Ω | 2 * t ≤ Rmix ω} ≤ Real.exp (-1 * t ^ eta)) ∧ (∀ (n : ℕ), MeasurableSet (rowBadEvent delta F n)) ∧ (∀ (n : ℕ) (ω : Ω), ω ∈ rowBadEvent delta F n ↔ delta ≤ F n ω) ∧ ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), Amix * Rmix ω ≤ 3 ^ n → ω ∉ rowBadEvent delta F n

The coupled mixing-scale witness together with the polynomial bound on its normalizer required by the physical-scale assembly.

An explicit admissible pair

noncomputable def HCPolySupport.HighContrast.Quenched.admissibleGenerationBound (nstar qfb b : ℕ) (theta mu cd Cblk : ℝ) : ℝ

The explicit real threshold above which a base generation meets the three lower bounds of the bad-tail estimate.

Equations

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

noncomputable def HCPolySupport.HighContrast.Quenched.normalizerWitness (mu cd Z : ℝ) : ℝ

The explicit normalizer attached to a base generation.

Equations

• HCPolySupport.HighContrast.Quenched.normalizerWitness mu cd Z = max 1 ((2 / cd * Z) ^ (1 / (2 * mu)))

theorem HCPolySupport.HighContrast.Quenched.one_le_normalizerWitness (mu cd Z : ℝ) : 1 ≤ normalizerWitness mu cd Z

theorem HCPolySupport.HighContrast.Quenched.le_mul_normalizerWitness {mu cd Z : ℝ} (hmu : 0 < mu) (hcd : 0 < cd) (hZ : 0 < Z) : Z ≤ cd / 2 * normalizerWitness mu cd Z ^ (2 * mu)

The explicit normalizer absorbs its own positive datum.

theorem HCPolySupport.HighContrast.Quenched.exists_admissible_thresholds_bounded {nstar qfb b : ℕ} {theta mu cd Cblk : ℝ} (hmu : 0 < mu) (hcd : 0 < cd) : ∃ (N0 : ℕ) (Bconst : ℝ), nstar ≤ N0 ∧ 1 ≤ Bconst ∧ ↑qfb + ↑b + 1 + rowSplitOffset theta Cblk ≤ ↑N0 - ↑nstar ∧ Real.log 2 ≤ cd * 3 ^ (2 * mu * (↑N0 - ↑nstar - badTailOffset theta Cblk qfb b)) * (3 ^ (mu / 2) - 1) ∧ 2 * Real.log 4 ≤ cd * 3 ^ (2 * mu * (↑N0 - ↑nstar - badTailOffset theta Cblk qfb b)) ∧ 3 ^ (2 * mu * (↑nstar + badTailOffset theta Cblk qfb b - ↑N0)) ≤ cd / 2 * Bconst ^ (2 * mu) ∧ ↑N0 ≤ admissibleGenerationBound nstar qfb b theta mu cd Cblk + 1 ∧ Bconst = normalizerWitness mu cd (3 ^ (2 * mu * (↑nstar + badTailOffset theta Cblk qfb b - ↑N0)))

An admissible base generation and normalizer, both with an explicit upper bound, so that their polynomial costs can be checked.