High-contrast homogenization: Provider.Response.RandomAdaptedResponseCarrierBridge

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

True response-load carrier bridges

Constant-skew covariance identifies the two terminal centered calls, while flattening the two block coordinates exposes the row load used by calibration.

theorem HCPolySupport.HighContrast.Response.true_load_centered_response_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) {S SStar K : Mat d} (e : Vec d) : let h0 := responseSkew K; have p := centeredResponseLoadP S SStar K e; have r := centeredResponseLoadQ S SStar K e; (∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew h0 ⋯).coeffOn (adaptedDomain hq t)) p r ∂P - 1 / 2 * vecDot (fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageGradient (adaptedDomain hq t) ((a.subSkew h0 ⋯).coeffOn (adaptedDomain hq t)) (centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew h0 ⋯) p r) i ∂P) fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageFlux (adaptedDomain hq t) ((a.subSkew h0 ⋯).coeffOn (adaptedDomain hq t)) (centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew h0 ⋯) p r) i ∂P) = centeredResponse P (adaptedDomain hq t) p (r - Matrix.mulVec (responseSkew K) p)

At the true Schur load, the recentered primal integral is the centered response used by the terminal supremum.

theorem HCPolySupport.HighContrast.Response.true_load_centered_adjoint_response_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) {S SStar K : Mat d} (e : Vec d) : let h0 := responseSkew K; have p := centeredResponseLoadP S SStar K e; have r := centeredResponseLoadQ S SStar K e; (∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew h0 ⋯).transpose.coeffOn (adaptedDomain hq t)) p r ∂P - 1 / 2 * vecDot (fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageGradient (adaptedDomain hq t) ((a.subSkew h0 ⋯).transpose.coeffOn (adaptedDomain hq t)) (centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew h0 ⋯) p r) i ∂P) fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageFlux (adaptedDomain hq t) ((a.subSkew h0 ⋯).transpose.coeffOn (adaptedDomain hq t)) (centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew h0 ⋯) p r) i ∂P) = centeredAdjointResponse P (adaptedDomain hq t) p (r + Matrix.mulVec (responseSkew K) p)

At the same true load, the independently recentered adjoint integral is the centered adjoint response with the opposite load correction.

theorem HCPolySupport.HighContrast.Response.true_carrier_compact_minus {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q m0 : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hint : HasFiniteAdaptedMean P q t) {S SStar K : Mat d} (e : Vec d) {C expo : ℝ} (hE6 : let h0 := responseSkew K; have hh0 := ⋯; have p := centeredResponseLoadP S SStar K e; have r := centeredResponseLoadQ S SStar K e; have center := profilePrimalCenter P hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r; have tau := profilePrimalResponseDefect P hq h0 hh0 s t p r; have EJ := ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew h0 hh0).coeffOn (adaptedDomain hq t)) p r ∂P; have row := profilePrimalHattedEarlierRow P q h0 s center.1 center.2; have weak := profilePrimalWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r; have Jtilde := EJ - 1 / 2 * vecDot (fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageGradient (adaptedDomain hq t) ((a.subSkew h0 hh0).coeffOn (adaptedDomain hq t)) (centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew h0 hh0) p r) i ∂P) fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageFlux (adaptedDomain hq t) ((a.subSkew h0 hh0).coeffOn (adaptedDomain hq t)) (centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew h0 hh0) p r) i ∂P; ENNReal.ofReal |Jtilde| ≤ ENNReal.ofReal C * ENNReal.ofReal √tau * (ENNReal.ofReal √tau + ENNReal.ofReal √EJ + row ^ (1 / 2)) + ENNReal.ofReal C * ENNReal.ofReal expo * ENNReal.ofReal √EJ * (ENNReal.ofReal √EJ + row ^ (1 / 2)) + ENNReal.ofReal C * weak) : let h0 := responseSkew K; have hh0 := ⋯; have p := centeredResponseLoadP S SStar K e; have r := centeredResponseLoadQ S SStar K e; have center := profilePrimalCenter P hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r; have tau := profilePrimalResponseDefect P hq h0 hh0 s t p r; have EJ := ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew h0 hh0).coeffOn (adaptedDomain hq t)) p r ∂P; have row := profilePrimalHattedEarlierRow P q h0 s center.1 center.2; have weak := profilePrimalWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r; ENNReal.ofReal |centeredResponse P (adaptedDomain hq t) p (r - Matrix.mulVec h0 p)| ≤ ENNReal.ofReal C * ENNReal.ofReal √tau * (ENNReal.ofReal √tau + ENNReal.ofReal √EJ + row ^ (1 / 2)) + ENNReal.ofReal C * ENNReal.ofReal expo * ENNReal.ofReal √EJ * (ENNReal.ofReal √EJ + row ^ (1 / 2)) + ENNReal.ofReal C * weak

The carried primal compact estimate at one Schur load rewrites to the literal endgame premise without changing any row or weak carrier.

theorem HCPolySupport.HighContrast.Response.true_carrier_compact_plus {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q m0 : Mat d} (hq : Matrix.PosDef q) {s t : ℤ} (hint : HasFiniteAdaptedMean P q t) {S SStar K : Mat d} (e : Vec d) {C expo : ℝ} (hE6 : let h0 := responseSkew K; have hh0 := ⋯; have p := centeredResponseLoadP S SStar K e; have r := centeredResponseLoadQ S SStar K e; have center := profileAdjointCenter P hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r; have tau := profileAdjointResponseDefect P hq h0 hh0 s t p r; have EJ := ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew h0 hh0).transpose.coeffOn (adaptedDomain hq t)) p r ∂P; have row := profileAdjointHattedEarlierRow P q h0 s center.1 center.2; have weak := profileAdjointWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r; have Jtilde := EJ - 1 / 2 * vecDot (fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageGradient (adaptedDomain hq t) ((a.subSkew h0 hh0).transpose.coeffOn (adaptedDomain hq t)) (centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew h0 hh0) p r) i ∂P) fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageFlux (adaptedDomain hq t) ((a.subSkew h0 hh0).transpose.coeffOn (adaptedDomain hq t)) (centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew h0 hh0) p r) i ∂P; ENNReal.ofReal |Jtilde| ≤ ENNReal.ofReal C * ENNReal.ofReal √tau * (ENNReal.ofReal √tau + ENNReal.ofReal √EJ + row ^ (1 / 2)) + ENNReal.ofReal C * ENNReal.ofReal expo * ENNReal.ofReal √EJ * (ENNReal.ofReal √EJ + row ^ (1 / 2)) + ENNReal.ofReal C * weak) : let h0 := responseSkew K; have hh0 := ⋯; have p := centeredResponseLoadP S SStar K e; have r := centeredResponseLoadQ S SStar K e; have center := profileAdjointCenter P hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r; have tau := profileAdjointResponseDefect P hq h0 hh0 s t p r; have EJ := ∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew h0 hh0).transpose.coeffOn (adaptedDomain hq t)) p r ∂P; have row := profileAdjointHattedEarlierRow P q h0 s center.1 center.2; have weak := profileAdjointWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r; ENNReal.ofReal |centeredAdjointResponse P (adaptedDomain hq t) p (r + Matrix.mulVec h0 p)| ≤ ENNReal.ofReal C * ENNReal.ofReal √tau * (ENNReal.ofReal √tau + ENNReal.ofReal √EJ + row ^ (1 / 2)) + ENNReal.ofReal C * ENNReal.ofReal expo * ENNReal.ofReal √EJ * (ENNReal.ofReal √EJ + row ^ (1 / 2)) + ENNReal.ofReal C * weak

The carried adjoint compact estimate rewrites with the adjoint defect, center-component row, and weak quantity unchanged.

theorem HCPolySupport.HighContrast.Response.hatted_adjoint_quadratic_load_eq {d : ℕ} (h : Mat d) (E : BlockMat d) (Pcen Qcen : Vec d) : profileQuadraticLoad (profileHattedAdjointBlock h E) Pcen Qcen = profileQuadraticLoad (profileHattedBlock h E) Pcen Qcen

Coefficient transposition preserves the quadratic row load before the adjoint center components are inserted.