High-contrast homogenization: Provider.Response.PreYoungPrimalAssembly

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

Primal compact pre-Young assembly

The centered decomposition, weak-product bound, cutoff-energy estimate, and boundary-row estimates combine into the compact primal response family. The finite weak-quantity assumption is confined to the component branch.

theorem HCPolySupport.HighContrast.Response.compact_pre_young_primal_of_row_estimates {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {l s t : ℤ} {m0 : Mat d} (hm0 : Matrix.PosDef m0) (hgrid : IsRoundedGrid l (roundedGrid l m0)) (hstat : IsStationaryLaw P) (hls : l ≤ s) (H : ℕ) (ht : t = s + ↑H) (hints : HasFiniteAdaptedMean P (roundedGrid l m0) s) (hintt : HasFiniteAdaptedMean P (roundedGrid l m0) t) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) {Cpre : ℝ} (hCpre : 1 ≤ Cpre) (hcut : 32 * ↑d ^ 2 * smoothTransitionProfile.derivBound ≤ Cpre) (hcomponent : preYoungComponentCoefficient d ≤ Cpre) (hfour : 4 ≤ Cpre) (hsqrtTwo : √2 ≤ Cpre) (hrows : profilePrimalWeakQuantity P m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤ → have hq := ⋯; have X := profilePrimalCenter P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r; have tau := profilePrimalResponseDefect P hq g hg s t p r; have EJ := ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r ∂P; have gain := preYoungComponentCoefficient d * 3 ^ (-↑H) * √EJ; have cut := adaptedPreYoungCutoff (roundedGrid l m0) hq t; ENNReal.ofReal |vecDot X.2 (profilePrimalCutoffMean P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) cut p r).1| ≤ ENNReal.ofReal (√(4 * tau) * profileSchurLoadFlux (profileHattedBlock g (adaptedMean P (roundedGrid l m0) s)) X.2) + ENNReal.ofReal gain * profilePrimalHattedEarlierRow P (roundedGrid l m0) g s X.1 X.2 ^ (1 / 2) ∧ ENNReal.ofReal |vecDot X.1 (profilePrimalCutoffMean P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) cut p r).2| ≤ ENNReal.ofReal (√(4 * tau) * profileSchurLoadGradient (profileHattedBlock g (adaptedMean P (roundedGrid l m0) s)) X.1) + ENNReal.ofReal gain * profilePrimalHattedEarlierRow P (roundedGrid l m0) g s X.1 X.2 ^ (1 / 2)) : have hq := ⋯; have X := profilePrimalCenter P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r; have tau := profilePrimalResponseDefect P hq g hg s t p r; have EJ := ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r ∂P; have row := profilePrimalHattedEarlierRow P (roundedGrid l m0) g s X.1 X.2; have weak := profilePrimalWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r; have Jtilde := EJ - 1 / 2 * vecDot (fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageGradient (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) (centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r) i ∂P) fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageFlux (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) (centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r) i ∂P; ∀ (Cresp : ℝ), Cpre ≤ Cresp → ENNReal.ofReal |Jtilde| ≤ ENNReal.ofReal Cresp * ENNReal.ofReal √tau * (ENNReal.ofReal √tau + ENNReal.ofReal √EJ + row ^ (1 / 2)) + ENNReal.ofReal Cresp * ENNReal.ofReal (3 ^ (-↑H)) * ENNReal.ofReal √EJ * (ENNReal.ofReal √EJ + row ^ (1 / 2)) + ENNReal.ofReal Cresp * weak

Primal boundary-row estimates complete the compact response bound, with the infinite weak-quantity branch closed algebraically.