High-contrast homogenization: Provider.Response.AdaptedWeakProductAnnealed

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

Annealed weak-product bounds for adapted responses

The samplewise affine weak-product estimate is specialized to the separately centered primal and adjoint response profiles. Integrating these literal physical cutoff terms gives the weak components used by the response estimate.

theorem HCPolySupport.HighContrast.Response.ofReal_abs_adaptedPreYoungCutoff_primalSample_le {d : ℕ} [NeZero d] {l t : ℤ} {m0 : Mat d} (hm0 : Matrix.PosDef m0) (hgrid : IsRoundedGrid l (roundedGrid l m0)) (P : MeasureTheory.Measure (CoeffSpace d)) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) (a : CoeffSpace d) : have hq := ⋯; have center := profilePrimalCenter P hq t sample p r; ENNReal.ofReal |Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => adaptedPreYoungCutoff (roundedGrid l m0) hq t x * (1 / 2 * vecDot ((centeredResponseOptimizer (adaptedDomain hq t) (sample a) p r).toH1.grad x - center.1) (matVecMul (((sample a).coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredResponseOptimizer (adaptedDomain hq t) (sample a) p r).toH1.grad x) - center.2))| ≤ ENNReal.ofReal (1 + divCurlDimensionCoeff d * adaptedCutoffDerivativeCoeff d * (51 / 50 * ↑d ^ 2)) * profilePrimalWeakRoot m0 hq t sample p r center a ^ 2

One primal sample's physical cutoff product is bounded by its squared normalized profile weak root.

theorem HCPolySupport.HighContrast.Response.ofReal_abs_adaptedPreYoungCutoff_adjointSample_le {d : ℕ} [NeZero d] {l t : ℤ} {m0 : Mat d} (hm0 : Matrix.PosDef m0) (hgrid : IsRoundedGrid l (roundedGrid l m0)) (P : MeasureTheory.Measure (CoeffSpace d)) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) (a : CoeffSpace d) : have hq := ⋯; have center := profileAdjointCenter P hq t sample p r; ENNReal.ofReal |Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => adaptedPreYoungCutoff (roundedGrid l m0) hq t x * (1 / 2 * vecDot ((centeredAdjointOptimizer (adaptedDomain hq t) (sample a) p r).toH1.grad x - center.1) (matVecMul (((sample a).transpose.coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredAdjointOptimizer (adaptedDomain hq t) (sample a) p r).toH1.grad x) - center.2))| ≤ ENNReal.ofReal (1 + divCurlDimensionCoeff d * adaptedCutoffDerivativeCoeff d * (51 / 50 * ↑d ^ 2)) * profileAdjointWeakRoot m0 hq t sample p r center a ^ 2

One adjoint sample obeys the same weak-product bound, with its independently centered transposed-coefficient optimizer and adjoint weak root.

theorem HCPolySupport.HighContrast.Response.ofReal_abs_integral_adaptedPreYoungCutoff_primal_le {d : ℕ} [NeZero d] {l t : ℤ} {m0 : Mat d} (hm0 : Matrix.PosDef m0) (hgrid : IsRoundedGrid l (roundedGrid l m0)) (P : MeasureTheory.Measure (CoeffSpace d)) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) : have hq := ⋯; have center := profilePrimalCenter P hq t sample p r; ENNReal.ofReal |∫ (a : CoeffSpace d), Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => adaptedPreYoungCutoff (roundedGrid l m0) hq t x * (1 / 2 * vecDot ((centeredResponseOptimizer (adaptedDomain hq t) (sample a) p r).toH1.grad x - center.1) (matVecMul (((sample a).coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredResponseOptimizer (adaptedDomain hq t) (sample a) p r).toH1.grad x) - center.2)) ∂P| ≤ ENNReal.ofReal (1 + divCurlDimensionCoeff d * adaptedCutoffDerivativeCoeff d * (51 / 50 * ↑d ^ 2)) * profilePrimalWeakQuantity P m0 hq t sample p r

The expectation of the literal primal cutoff product is controlled by the primal weak quantity, with the rounded-grid distortion already absorbed.

theorem HCPolySupport.HighContrast.Response.ofReal_abs_integral_adaptedPreYoungCutoff_adjoint_le {d : ℕ} [NeZero d] {l t : ℤ} {m0 : Mat d} (hm0 : Matrix.PosDef m0) (hgrid : IsRoundedGrid l (roundedGrid l m0)) (P : MeasureTheory.Measure (CoeffSpace d)) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) : have hq := ⋯; have center := profileAdjointCenter P hq t sample p r; ENNReal.ofReal |∫ (a : CoeffSpace d), Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => adaptedPreYoungCutoff (roundedGrid l m0) hq t x * (1 / 2 * vecDot ((centeredAdjointOptimizer (adaptedDomain hq t) (sample a) p r).toH1.grad x - center.1) (matVecMul (((sample a).transpose.coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredAdjointOptimizer (adaptedDomain hq t) (sample a) p r).toH1.grad x) - center.2)) ∂P| ≤ ENNReal.ofReal (1 + divCurlDimensionCoeff d * adaptedCutoffDerivativeCoeff d * (51 / 50 * ↑d ^ 2)) * profileAdjointWeakQuantity P m0 hq t sample p r

The corresponding adjoint expectation is controlled by the independently centered adjoint weak quantity.