High-contrast homogenization: Entry.Response.Transfer.ResponseContractionParameters

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

Closing the multiscale contraction

The source load bound L_s^± ≤ C κ_s^{3/2} of p.response.transfer is proved by removing the translation dependence through integer stationarity, bounding the weighted sum of the coarse-block norms by a constant multiple of the finest one via the determinant-drift telescope, and treating the scales below the selection threshold with the source estimate and the smallness hypothesis on the source term. Turning the resulting one-step inequality κ_t - 1 ≤ ω κ_t into the target bound κ_t ≤ 1 + δ_ad is pure real arithmetic, valid once ω ≤ δ_ad/(1+δ_ad). The parameter choice closes the argument by fixing, in order, a scale H large enough that 3^{-H} and 3^{-αH} are small, a tolerance η small enough that the resulting quadratic term is small, and a base scale σ₀ small enough that the eccentricity r stays close to 1, so that the printed contraction constant ω obeys the bound the arithmetic step needs.

The source load bound

theorem HCPolySupport.HighContrast.Multiscale.response_source_load_bound (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (_hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (_hS : S.Selects d γ) (Cc Cs Cl : ℝ) (_hCc : 0 < Cc) (_hCs : 0 < Cs) (_hCl : 0 < Cl) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (ε σ : ℝ), ε ∈ Set.Ioc 0 S.eps0 → σ ∈ Set.Ioc 0 ε → ∀ (Cglob Cprof Bresp : ℝ), 0 ≤ Cglob → ∀ (H : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ), RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ Kg Src B jStar F s t → RespCalibrated Cc P jStar F s t → ∀ η ∈ Set.Ioo 0 (1 / 2), Cprof * σ ^ ((1 - γ) / 8) ≤ η → RespSourceSmall d γ Cs η E F jStar s t → ∀ (e : Vec d), vecDot e e = 1 → RespLoadMean Cl P jStar F s t e → RespLoadBound C P jStar F s t e

The source load bound response_source_load_bound (p.response.transfer): L_s^± <= C kappa_s^{3/2}.

Route: for k >= j_* integer stationarity removes z (Annealed.annealedBlock_adaptedCellAtCenter), and the weighted sum of the E_k is bounded by C(1 + D_{q,j_*}(s))E_s -- telescope the mean increments of determinantDrift and use 3/2 > (1-gamma)/8. For k < j_* the source estimate and the second inequality of e.response.source.smallness bound the rest by C E_s. Apply the resulting matrix bounds to the two coordinate projections of Y^± and finish with response_calibrated_blocks and response_load_and_mean; the series converges because gamma < 3/2.

Premises _hε, _hσ: without them 1 ≤ B and jStar ≤ s are unavailable. The binder names are underscore-prefixed because they do not occur in the statement's own type; the proof uses them.

The contraction arithmetic

theorem HCPolySupport.HighContrast.Multiscale.response_contraction_arith (d : ℕ) (_hd : 2 ≤ d) (σ δad κt κs r ω : ℝ) (hκt : 1 ≤ κt) (_hts : κt ≤ κs) (_hsr : κs ≤ r ^ 2 * κt) (_hr : r < Real.exp (↑d * σ)) (hδad : δad ∈ Set.Ioc 0 1) (hω : κt - 1 ≤ ω * κt) (hωδ : ω ≤ δad / (1 + δad)) : κt ≤ 1 + δad

The contraction arithmetic response_contraction_arith: rearranging kappa_t - 1 <= omega kappa_t (p.response.transfer). Pure real arithmetic.

From omega <= delta/(1+delta) < 1 one gets (1-omega) kappa_t <= 1, hence kappa_t <= 1/(1-omega) <= 1 + delta.

The parameter choice

theorem HCPolySupport.HighContrast.Multiscale.response_parameter_choice (d : ℕ) (_hd : 2 ≤ d) (h Q : ℕ) (ε δad α C : ℝ) (CH : ℕ → ℝ) (_hε : 0 < ε) (_hδad : δad ∈ Set.Ioc 0 1) (_hα : α ∈ Set.Ioo 0 1) (_hC : 0 < C) (_hQ : 2 ≤ Q) (_hCH : ∀ (n : ℕ), 0 < CH n) : ∃ (H : ℕ), max 4 h ≤ H ∧ ∃ η ∈ Set.Ioo 0 (1 / 2), ∃ σ₀ ∈ Set.Ioc 0 ε, ∀ σ ∈ Set.Ioc 0 σ₀, ∀ (r : ℝ), 1 ≤ r → r < Real.exp (↑d * σ) → C * r ^ 2 * (r - 1 + √(r - 1) + 3 ^ (-↑H) + (3 ^ (-(α * ↑H)) + CH H * η ^ (1 / (2 * ↑Q))) ^ 2) ≤ δad / (1 + δad)

The parameter choice response_parameter_choice (p.response.transfer): choose H large, then eta small, then sigma_0 small enough that r < e^{d sigma_0}, so that the printed omega obeys omega <= delta_ad/(1+delta_ad). The omega formula matches the printed display symbol for symbol.

Route: 3^{-H} and 3^{-alpha H} tend to 0, so fix H with C' (3^{-H} + 4 * 3^{-2 alpha H}) <= delta_ad/(4(1+delta_ad)), where C' absorbs the r^2 factor (bounded once sigma_0 <= 1); then eta with C' * 4 * (C_H eta^{1/(2Q)})^2 small; then sigma_0 so small that r - 1 <= e^{d sigma_0} - 1 and sqrt(r-1) are small.