High-contrast homogenization: Provider.Quenched.SmallContrastOneStepHub

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

The conditional one-step hatted contraction on the fixed grid

This is the composition hub for the native form of Lemma 4.5 of HC: the fixed-grid pre-Young response families, the carrier bridges at the calibrated Schur loads, the hatted-drop profile-defect cap, the reabsorbed compact response upper bound, and the hatted response lower bound compose into a one-step estimate for the hatted carrier at the terminal generation.

The estimate is conditional on exactly the still-open row (L), weak (W), and centering (Z) caps at the calibrated loads: these three uniform caps are the only analytic inputs not derived from stationarity, unit range, Dagger, and the two smallness clauses. Once the cap theorem exists, this hub discharges it into hat(t) - 1 ≤ 4·Cpre·((3/2 + 1/(4η))·16d·(hat(s)-hat(t)) + L + W) + 2·Z.

theorem HCPolySupport.HighContrast.Quenched.exists_hatted_one_step_of_profile_caps (d : ℕ) [NeZero d] : ∃ (Cpre : ℝ), 1 ≤ Cpre ∧ ∀ {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P], IsStationaryLaw P → ∀ {gdag : ℝ} {Edag : BlockMat d} {Psidag : ℝ → ℝ} {Kdag : ℝ} {Sdag : CoeffSpace d → ℝ}, CoarseEllipticityDagger P gdag Edag Psidag Kdag Sdag → ∀ {l : ℤ} {m0 q : Mat d}, Matrix.PosDef m0 → q = roundedGrid l m0 → ∀ (hgrid : IsRoundedGrid l q) {s t : ℤ}, l ≤ s → ∀ (H : ℕ), t = s + ↑H → (∀ (k : ℤ), l ≤ k → k ≤ t → HasFiniteAdaptedMean P q k ∧ Book.Ch02.BlockPosDef (adaptedMean P q k)) → ∀ {S SStar K : Mat d}, Matrix.PosDef S → Matrix.PosDef SStar → toFullBlockMat (adaptedMean P q t) = schurBlock S SStar K → 6 * (blockContrast (adaptedMean P q t) - 1) ≤ 1 → ↑d * (adaptedHattedContrast P q s - adaptedHattedContrast P q t) ≤ 1 → ∀ {eta L W Z : ℝ}, 0 < eta → 0 ≤ L → 0 ≤ W → Cpre * eta + 3 / 2 * Cpre * 3 ^ (-↑H) ≤ 1 / 2 → (∀ (e : Vec d), e ⬝ᵥ e = 1 → let h0 := Response.responseSkew K; have hh0 := ⋯; have p := Response.centeredResponseLoadP S SStar K e; have r := Response.centeredResponseLoadQ S SStar K e; have hq := ⋯; have Xm := Response.profilePrimalCenter P hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r; have Xp := Response.profileAdjointCenter P hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r; Response.profilePrimalHattedEarlierRow P q h0 s Xm.1 Xm.2 ≤ ENNReal.ofReal L ∧ Response.profileAdjointHattedEarlierRow P q h0 s Xp.1 Xp.2 ≤ ENNReal.ofReal L ∧ Response.profilePrimalWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r ≤ ENNReal.ofReal W ∧ Response.profileAdjointWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r ≤ ENNReal.ofReal W ∧ 1 / 2 * |vecDot ⋯ ⋯| ≤ Z ∧ 1 / 2 * |vecDot ⋯ ⋯| ≤ Z) → adaptedHattedContrast P q t - 1 ≤ 4 * Cpre * ((3 / 2 + 1 / (4 * eta)) * (16 * ↑d * (adaptedHattedContrast P q s - adaptedHattedContrast P q t)) + L + W) + 2 * Z

The conditional one-step hatted contraction. The constant Cpre is selected before the law. All hypotheses except the three caps (hcaps) are either hcore data, grid/window geometry, or the two smallness clauses; the caps are the exact remaining analytic obligations of the small-contrast iteration.