High-contrast homogenization: Entry.Response.Rows.CutoffOscillationAdjointCarrier

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

The oscillation half of the cutoff-mean row for the adjoint sign

This file proves, for the adjoint recentred coefficient a_+ = a^T + g, the same closing statement proved elsewhere for the negative sign: the oscillation half of the cutoff-mean row is bounded by the source load once the terminal optimizer family supplies the refinement identity at every depth, the cutoff-weight increment, and the pathwise crossed-pairing bound on each descendant cell. Only the sign of the recentred coefficient changes; the increment envelope, the vanishing remainder, and the general closure statement are shared with the negative-sign case and are not reproved here. The per-descendant-cell crossed-pairing bound is again left as a hypothesis, to be discharged where the terminal optimizer field for this sign is actually constructed. The bound is the adjoint-sign half of the cutoff-mean row used by the cutoff estimate p.response.transfer, and so contributes to the polynomial entry result t.polynomial.entry.

The oscillation half of the cutoff-mean row at the carriers, adjoint sign

The adjoint twin of CutoffOscillationHalfClosure: the same carrier data for the recentred adjoint coefficient a_+ = aᵀ + g, with the same per-descendant-cell crossed pairing left as a hypothesis.

theorem HCPolySupport.HighContrast.Multiscale.integrable_and_abs_integral_cross_sub_cellPart_le_respCoeffPlus_car {d : ℕ} [NeZero d] (hd : 2 ≤ d) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (hdag : CoarseEllipticityDagger P γ E Ψ Kg Src) (jStar : ℕ) (hjStar : 2 * d ≤ 3 ^ jStar) (F : BlockMat d) (hm : Matrix.PosDef (explicitCanonicalMetric F)) (hq : IsUnit (respGrid jStar F)) (H : ℕ) (s t : ℤ) (ht : t = s + ↑H) (hjs : ↑jStar ≤ s) (e : Vec d) (φ : Vec d → ℝ) (hφ : IsResponseCutoff (respGrid jStar F) t φ) (Y : BlockVec d) (uP : (a : CoeffSpace d) → AHarmonicFunction (respCoeffPlus F a) (respCell jStar F t)) (hmax : ∀ (a : CoeffSpace d), IsResponseMaximizer (respCell jStar F t) (respP (respMean P jStar F t) e) (respqPlus P jStar F t e) (respCoeffPlus F a) (uP a)) (hEint : ∀ (a : CoeffSpace d), MeasureTheory.IntegrableOn (scalarVariationEnergyIntegrand (respCoeffPlus F a) (uP a)) (respCell jStar F t) MeasureTheory.volume) (hJ : MeasureTheory.Integrable (fun (a : CoeffSpace d) => respJ (respGrid jStar F) t (respP (respMean P jStar F t) e) (respqPlus P jStar F t e) (respCoeffPlus F a)) P) (hsumm : Summable fun (n : ℕ) => 3 ^ (-(3 / 2) * ↑n) * ((↑(triadicIndexBox d n).card)⁻¹ * ∑ z ∈ triadicIndexBox d n, (√(vecDot Y.1 (matVecMul (annealedBlockOf P (adaptedCellAtCenter (respGrid jStar F) (s - ↑n) z) (respCoeffPlus F)).upperLeft Y.1)) + √(vecDot Y.2 (matVecMul (annealedBlockOf P (adaptedCellAtCenter (respGrid jStar F) (s - ↑n) z) (respCoeffPlus F)).lowerRight Y.2))) ^ 2)) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => volumeAverage (respCell jStar F t) fun (x : Vec d) => (φ x - 1) * (vecDot Y.2 (optimizerField (respCoeffPlus F a) (uP a) x).1 + vecDot Y.1 (optimizerField (respCoeffPlus F a) (uP a) x).2)) P ∧ |∫ (a : CoeffSpace d), volumeAverage (respCell jStar F t) fun (x : Vec d) => (φ x - 1) * (vecDot Y.2 (optimizerField (respCoeffPlus F a) (uP a) x).1 + vecDot Y.1 (optimizerField (respCoeffPlus F a) (uP a) x).2) ∂P - ∫ (a : CoeffSpace d), (↑(triadicIndexBox d H).card)⁻¹ * ∑ w ∈ triadicIndexBox d H, (volumeAverage (adaptedCellAtCenter (respGrid jStar F) (t - ↑H) w) fun (x : Vec d) => φ x - 1) * volumeAverage (adaptedCellAtCenter (respGrid jStar F) (t - ↑H) w) fun (x : Vec d) => vecDot Y.2 (optimizerField (respCoeffPlus F a) (uP a) x).1 + vecDot Y.1 (optimizerField (respCoeffPlus F a) (uP a) x).2 ∂P| ≤ 32 * ↑d ^ 2 * responseCutoffProfileConst * 3 ^ (-↑H) * (√(∑' (n : ℕ), 3 ^ (-(↑n / 2))) * √(3 ^ (3 / 2) * respSourceLoad P jStar F s (respCoeffPlus F) Y)) * √(2 * (4 * respEJPlus P jStar F t e))

The oscillation half of the cutoff-mean row at the carriers, plus sign. The (φ-1)-weighted cell average of the crossed pairing of the deterministic dual variable with the terminal optimizer state is P-integrable, and its annealed mean differs from that of its depth-H cell part by at most 32 d² Θ 3^{-H} (3^{3/2} 𝓛_s^-)^{1/2} (8 E[J_t^-])^{1/2} times the geometric factor.