High-contrast homogenization: Provider.Response.PreYoungCenteredDecomposition

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

Centered terminal-response decomposition

The annealed terminal response is split into a cutoff-weighted centered product, the cutoff-energy defect, and the two cutoff-defect means. The measurability of the centered product and the localized readouts is recovered from the measurable optimizer energy and coordinate-readout maps; quantitative domination is kept explicit.

theorem HCPolySupport.HighContrast.Response.integrable_responseJ_subSkew_of_finiteAdaptedMean {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsFiniteMeasure P] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r) P

A finite adapted mean makes the constant-skew primal terminal response integrable.

theorem HCPolySupport.HighContrast.Response.integrable_responseJ_adjointSubSkew_of_finiteAdaptedMean {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsFiniteMeasure P] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r) P

A finite adapted mean makes the independently transposed constant-skew terminal response integrable.

theorem HCPolySupport.HighContrast.Response.ofReal_abs_profilePrimalCenteredResponse_le_cutoff_decomposition_of_integrable {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) (hcutoff : MeasureTheory.Integrable (fun (a : CoeffSpace d) => (Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) (matVecMul (((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) - Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r) P) (hlocalized : ∀ (alpha : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => volumeAverage (adaptedCell q t) fun (x : Vec d) => (adaptedPreYoungCutoff q hq t x - 1) * toFullBlockVec (diagonalWeakState hq t (a.subSkew g hg) p r x) alpha) P) : have X := profilePrimalCenter P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r; have cut := adaptedPreYoungCutoff q hq t; have M := profilePrimalCutoffMean P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) cut p r; have J := fun (a : CoeffSpace d) => Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r; have W := fun (a : CoeffSpace d) => Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => cut x * (1 / 2 * vecDot ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) (matVecMul (((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x))); have C := fun (a : CoeffSpace d) => Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => cut x * (1 / 2 * vecDot ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x - X.1) (matVecMul (((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) - X.2)); ENNReal.ofReal |∫ (a : CoeffSpace d), J a ∂P - 1 / 2 * vecDot X.1 X.2| ≤ ENNReal.ofReal |∫ (a : CoeffSpace d), C a ∂P| + ENNReal.ofReal |∫ (a : CoeffSpace d), W a - J a ∂P| + ENNReal.ofReal (1 / 2 * |vecDot X.2 M.1 + vecDot X.1 M.2|)

The primal centered response splits into the centered cutoff product, the terminal cutoff-energy defect, and the two cutoff-defect means.

theorem HCPolySupport.HighContrast.Response.ofReal_abs_profileAdjointCenteredResponse_le_cutoff_decomposition_of_integrable {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) (hcutoff : MeasureTheory.Integrable (fun (a : CoeffSpace d) => (Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) (matVecMul (((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) - Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r) P) (hlocalized : ∀ (alpha : BlockCoord d), MeasureTheory.Integrable (fun (a : CoeffSpace d) => volumeAverage (adaptedCell q t) fun (x : Vec d) => (adaptedPreYoungCutoff q hq t x - 1) * toFullBlockVec (diagonalWeakAdjointState hq t (a.subSkew g hg) p r x) alpha) P) : have X := profileAdjointCenter P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r; have cut := adaptedPreYoungCutoff q hq t; have M := profileAdjointCutoffMean P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) cut p r; have J := fun (a : CoeffSpace d) => Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r; have W := fun (a : CoeffSpace d) => Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => cut x * (1 / 2 * vecDot ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) (matVecMul (((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x))); have C := fun (a : CoeffSpace d) => Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => cut x * (1 / 2 * vecDot ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x - X.1) (matVecMul (((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) - X.2)); ENNReal.ofReal |∫ (a : CoeffSpace d), J a ∂P - 1 / 2 * vecDot X.1 X.2| ≤ ENNReal.ofReal |∫ (a : CoeffSpace d), C a ∂P| + ENNReal.ofReal |∫ (a : CoeffSpace d), W a - J a ∂P| + ENNReal.ofReal (1 / 2 * |vecDot X.2 M.1 + vecDot X.1 M.2|)

The adjoint centered response splits into the centered cutoff product, the terminal cutoff-energy defect, and the two cutoff-defect means.

theorem HCPolySupport.HighContrast.Response.ofReal_abs_profilePrimalCenteredResponse_le_cutoff_decomposition_of_domination {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q m0 : Mat d} (hq : Matrix.PosDef q) (hm0 : Matrix.PosDef m0) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) (hweak : profilePrimalWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) (hdom : ∀ (a : CoeffSpace d), (0 ≤ Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) (matVecMul (((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) ∧ (Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) (matVecMul (((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) ≤ 2 * Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r) : have X := profilePrimalCenter P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r; have cut := adaptedPreYoungCutoff q hq t; have M := profilePrimalCutoffMean P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) cut p r; have J := fun (a : CoeffSpace d) => Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r; have W := fun (a : CoeffSpace d) => Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => cut x * (1 / 2 * vecDot ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) (matVecMul (((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x))); have C := fun (a : CoeffSpace d) => Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => cut x * (1 / 2 * vecDot ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x - X.1) (matVecMul (((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) - X.2)); ENNReal.ofReal |∫ (a : CoeffSpace d), J a ∂P - 1 / 2 * vecDot X.1 X.2| ≤ ENNReal.ofReal |∫ (a : CoeffSpace d), C a ∂P| + ENNReal.ofReal |∫ (a : CoeffSpace d), W a - J a ∂P| + ENNReal.ofReal (1 / 2 * |vecDot X.2 M.1 + vecDot X.1 M.2|)

Under finite primal weak quantity, response domination supplies every integrability premise in the centered cutoff decomposition.

theorem HCPolySupport.HighContrast.Response.ofReal_abs_profileAdjointCenteredResponse_le_cutoff_decomposition_of_domination {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q m0 : Mat d} (hq : Matrix.PosDef q) (hm0 : Matrix.PosDef m0) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) (g : Mat d) (hg : IsSkewMat g) (p r : Vec d) (hweak : profileAdjointWeakQuantity P m0 hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r ≠ ⊤) (hdom : ∀ (a : CoeffSpace d), (0 ≤ Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) (matVecMul (((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) ∧ (Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) (matVecMul (((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) ≤ 2 * Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r) : have X := profileAdjointCenter P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) p r; have cut := adaptedPreYoungCutoff q hq t; have M := profileAdjointCutoffMean P hq t (fun (a : CoeffSpace d) => a.subSkew g hg) cut p r; have J := fun (a : CoeffSpace d) => Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r; have W := fun (a : CoeffSpace d) => Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => cut x * (1 / 2 * vecDot ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) (matVecMul (((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x))); have C := fun (a : CoeffSpace d) => Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => cut x * (1 / 2 * vecDot ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x - X.1) (matVecMul (((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) - X.2)); ENNReal.ofReal |∫ (a : CoeffSpace d), J a ∂P - 1 / 2 * vecDot X.1 X.2| ≤ ENNReal.ofReal |∫ (a : CoeffSpace d), C a ∂P| + ENNReal.ofReal |∫ (a : CoeffSpace d), W a - J a ∂P| + ENNReal.ofReal (1 / 2 * |vecDot X.2 M.1 + vecDot X.1 M.2|)

Under finite adjoint weak quantity, response domination supplies every integrability premise in the centered cutoff decomposition.