High-contrast homogenization: Provider.Response.AdaptedWeakTransport

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

The concrete weak seminorm under an adapted-cell normalization

An invertible grid identifies every aligned adapted subdivision with the standard subdivision of the reference cube. Normalized cell averages have no Jacobian factor under this identification. The two slots of a doubled field transform contravariantly, and their Euclidean square is controlled by the larger of the two Frobenius norms.

theorem HCPolySupport.HighContrast.Response.memVectorL2_affinePullback {d : ℕ} {L : Mat d} (hL : IsUnit (Matrix.det L)) {U : Set (Vec d)} (hU : MeasurableSet U) {F : Vec d → Vec d} (hF : MemVectorL2 U F) : MemVectorL2 (matImage L⁻¹ U) fun (y : Vec d) => F (matVecMul L y)

Vector-valued square integrability is preserved by an invertible affine pullback.

theorem HCPolySupport.HighContrast.Response.alignedIndex_one_eq {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {j t : ℤ} (hjt : j ≤ t) : alignedIndex 1 j t = alignedIndex q j t

The labels of an aligned subdivision do not depend on its invertible positive-definite grid.

theorem HCPolySupport.HighContrast.Response.matImage_inv_adaptedCellAt_eq {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) : matImage q⁻¹ (adaptedCellAt q k w) = adaptedCellAt 1 k w

The inverse grid sends an aligned adapted cell to the corresponding cell of the identity grid.

theorem HCPolySupport.HighContrast.Response.matImage_adaptedCellAt_one_eq {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) : matImage q (adaptedCellAt 1 k w) = adaptedCellAt q k w

The grid sends an identity-grid aligned cell to the corresponding adapted cell.

theorem HCPolySupport.HighContrast.Response.blockCellAverage_affinePullback {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (A B : Mat d) (k : ℤ) (w : Fin d → ℤ) (F : Vec d → BlockVec d) (hF₁ : MemVectorL2 (adaptedCellAt q k w) fun (x : Vec d) => (F x).1) (hF₂ : MemVectorL2 (adaptedCellAt q k w) fun (x : Vec d) => (F x).2) : (blockCellAverage (adaptedCellAt 1 k w) fun (y : Vec d) => (matVecMul A (F (matVecMul q y)).1, matVecMul B (F (matVecMul q y)).2)) = (matVecMul A (blockCellAverage (adaptedCellAt q k w) F).1, matVecMul B (blockCellAverage (adaptedCellAt q k w) F).2)

A doubled cell average transforms slotwise under the dual affine actions. The square-integrability hypotheses are inherited from response solutions in the intended application.

theorem HCPolySupport.HighContrast.Response.blockVecDot_affineSlots_le {d : ℕ} (A B : Mat d) (v : BlockVec d) : blockVecDot (matVecMul A v.1, matVecMul B v.2) (matVecMul A v.1, matVecMul B v.2) ≤ max (Book.Ch02.matrixFrobeniusNormSq A) (Book.Ch02.matrixFrobeniusNormSq B) * blockVecDot v v

The squared length of the two-slot affine image is controlled by the larger Frobenius square of the two matrices.

theorem HCPolySupport.HighContrast.Response.blockAvsumL2_affineSlots_le {d : ℕ} {I : Type u_1} (Z : Finset I) (A B : Mat d) (u : I → BlockVec d) : (blockAvsumL2 Z fun (z : I) => (matVecMul A (u z).1, matVecMul B (u z).2)) ≤ √(max (Book.Ch02.matrixFrobeniusNormSq A) (Book.Ch02.matrixFrobeniusNormSq B)) * blockAvsumL2 Z u

The normalized finite-family L² norm obeys the same two-slot matrix bound.

theorem HCPolySupport.HighContrast.Response.adaptedWeakScaleTerm_affinePullback_le {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (A B : Mat d) (t : ℤ) (s : ℝ) (F : Vec d → BlockVec d) (hF₁ : MemVectorL2 (adaptedCell q t) fun (x : Vec d) => (F x).1) (hF₂ : MemVectorL2 (adaptedCell q t) fun (x : Vec d) => (F x).2) (j : ℕ) : adaptedWeakScaleTerm 1 t s (fun (y : Vec d) => (matVecMul A (F (matVecMul q y)).1, matVecMul B (F (matVecMul q y)).2)) j ≤ √(max (Book.Ch02.matrixFrobeniusNormSq A) (Book.Ch02.matrixFrobeniusNormSq B)) * adaptedWeakScaleTerm q t s F j

Each scale of the reference-cube seminorm is bounded by the corresponding adapted-cell scale and the explicit two-slot distortion.

theorem HCPolySupport.HighContrast.Response.adaptedWeakSeminorm_affinePullback_le {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (A B : Mat d) (t : ℤ) (s : ℝ) (F : Vec d → BlockVec d) (hF₁ : MemVectorL2 (adaptedCell q t) fun (x : Vec d) => (F x).1) (hF₂ : MemVectorL2 (adaptedCell q t) fun (x : Vec d) => (F x).2) : (adaptedWeakSeminorm 1 t s fun (y : Vec d) => (matVecMul A (F (matVecMul q y)).1, matVecMul B (F (matVecMul q y)).2)) ≤ ENNReal.ofReal √(max (Book.Ch02.matrixFrobeniusNormSq A) (Book.Ch02.matrixFrobeniusNormSq B)) * adaptedWeakSeminorm q t s F

The reference-cube concrete weak seminorm is controlled by the adapted seminorm with the explicit two-slot Frobenius distortion.