High-contrast homogenization: Provider.Quenched.SmallContrastHattedCarrier

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

The hatted small-contrast carrier

The small-contrast argument uses the normalized trace of the two symmetric Schur blocks. This file records that carrier on a doubled block and relates it directly to the calibrated primal--adjoint centered responses.

noncomputable def HCPolySupport.HighContrast.Quenched.schurHattedContrast {d : ℕ} (S SStar : Mat d) : ℝ

The normalized trace of the upper Schur block relative to the lower one.

Equations

• HCPolySupport.HighContrast.Quenched.schurHattedContrast S SStar = (↑d)⁻¹ * (HCPolySupport.HighContrast.matSqrt SStar⁻¹ * S * HCPolySupport.HighContrast.matSqrt SStar⁻¹).trace

noncomputable def HCPolySupport.HighContrast.Quenched.hattedContrast {d : ℕ} (H : BlockMat d) : ℝ

The hatted contrast of a doubled block, written with its lower-right block, which is the inverse lower Schur block on positive data.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.Quenched.adaptedHattedContrast {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (m : ℤ) : ℝ

The hatted contrast of the annealed response on an adapted cell.

Equations

• HCPolySupport.HighContrast.Quenched.adaptedHattedContrast P q m = HCPolySupport.HighContrast.Quenched.hattedContrast (HCPolySupport.HighContrast.adaptedMean P q m)

theorem HCPolySupport.HighContrast.Quenched.hattedContrast_eq_trace_lowerRight_mul {d : ℕ} {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) (hpos : Book.Ch02.BlockPosDef H) : hattedContrast H = (↑d)⁻¹ * (H.lowerRight * schurSigma H).trace

On positive data cyclicity writes the hatted carrier without square roots.

theorem HCPolySupport.HighContrast.Quenched.hattedContrast_le_of_blockMatLoewnerLE {d : ℕ} {A E : BlockMat d} (hAsymm : IsSymmetricBlockMat A) (hApos : Book.Ch02.BlockPosDef A) (hEsymm : IsSymmetricBlockMat E) (hEpos : Book.Ch02.BlockPosDef E) (hle : BlockMatLoewnerLE A E) : hattedContrast A ≤ hattedContrast E

The hatted carrier is monotone for the doubled Loewner order on symmetric positive blocks.

theorem HCPolySupport.HighContrast.Quenched.hattedContrast_le_blockContrast {d : ℕ} [NeZero d] {H : BlockMat d} (hsymm : IsSymmetricBlockMat H) (hpos : Book.Ch02.BlockPosDef H) : hattedContrast H ≤ blockContrast H

The normalized trace carrier is bounded by the intrinsic polynomial contrast.

theorem HCPolySupport.HighContrast.Quenched.adaptedHattedContrast_le {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {l : ℤ} {q : Mat d} (hgrid : IsRoundedGrid l q) {j p : ℤ} (hlj : l ≤ j) (hjp : j ≤ p) (hfinj : HasFiniteAdaptedMean P q j) (hfinp : HasFiniteAdaptedMean P q p) : adaptedHattedContrast P q p ≤ adaptedHattedContrast P q j

The hatted contrast decreases along one fixed rounded adapted grid.

theorem HCPolySupport.HighContrast.Quenched.adaptedHattedContrast_one {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (m : ℤ) : adaptedHattedContrast P 1 m = hattedContrast (annealedBlock P (centeredCube d m))

On the Euclidean grid, the adapted carrier is the hatted carrier of the annealed response on the centered cube.

theorem HCPolySupport.HighContrast.Quenched.adaptedHattedContrast_one_le_annealedContrast {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) (m : ℤ) : adaptedHattedContrast P 1 m ≤ annealedContrast P m

On the Euclidean grid, the adapted hatted carrier is bounded by the annealed intrinsic contrast.

theorem HCPolySupport.HighContrast.Quenched.adaptedHattedContrast_one_sub_one_le_of_annealedContrast_sub_one_le {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) (m : ℤ) {c : ℝ} (hsmall : annealedContrast P m - 1 ≤ c) : adaptedHattedContrast P 1 m - 1 ≤ c

Euclidean annealed smallness therefore initializes the adapted hatted carrier at the same generation.

theorem HCPolySupport.HighContrast.Quenched.hattedContrast_eq_schurHattedContrast {d : ℕ} {H : BlockMat d} {S SStar K : Mat d} (hStar : Matrix.PosDef SStar) (hH : toFullBlockMat H = schurBlock S SStar K) : hattedContrast H = schurHattedContrast S SStar

A Schur representation identifies the intrinsic block carrier with the two-matrix Schur carrier.

theorem HCPolySupport.HighContrast.Quenched.schurHattedContrast_sub_one_eq_trace_centeredResponseX {d : ℕ} [NeZero d] (S SStar : Mat d) : schurHattedContrast S SStar - 1 = (↑d)⁻¹ * Matrix.trace (Response.centeredResponseX S SStar)

The hatted defect is the dimension-normalized trace of the positive Schur excess.

theorem HCPolySupport.HighContrast.Quenched.schurHattedContrast_sub_one_le_absoluteCenteredResponseSup {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) {S SStar K : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K) : schurHattedContrast S SStar - 1 ≤ sSup ((fun (e : Vec d) => |Response.centeredResponse P U (Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e - Matrix.mulVec (Response.responseSkew K) (Response.centeredResponseLoadP S SStar K e))| + |Response.centeredAdjointResponse P U (Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e + Matrix.mulVec (Response.responseSkew K) (Response.centeredResponseLoadP S SStar K e))|) '' {e : Vec d | e ⬝ᵥ e = 1})

The source hatted defect is controlled directly by the calibrated absolute primal--adjoint centered response supremum.

theorem HCPolySupport.HighContrast.Quenched.hattedContrast_annealedBlock_sub_one_le_absoluteCenteredResponseSup {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) {S SStar K : Mat d} (hS : Matrix.PosDef S) (hStar : Matrix.PosDef SStar) (hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K) : hattedContrast (annealedBlock P U.carrier) - 1 ≤ sSup ((fun (e : Vec d) => |Response.centeredResponse P U (Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e - Matrix.mulVec (Response.responseSkew K) (Response.centeredResponseLoadP S SStar K e))| + |Response.centeredAdjointResponse P U (Response.centeredResponseLoadP S SStar K e) (Response.centeredResponseLoadQ S SStar K e + Matrix.mulVec (Response.responseSkew K) (Response.centeredResponseLoadP S SStar K e))|) '' {e : Vec d | e ⬝ᵥ e = 1})

The same response lower bound, expressed on the annealed doubled block.