High-contrast homogenization:

Provider.Regularity.UnitCubeContinuousKNormalizedEnergyConstantMatrix

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

Constant matrices on the normalized unit-cube continuous K-energy

Constant matrix multiplication acts on both the normalized Euclidean L² term and every genuine H¹ competitor in the continuous K-functional. The resulting quadratic energy is bounded by the square of the Euclidean matrix operator norm.

noncomputable def HCPolySupport.HighContrast.unitCubeEuclideanL2FieldConstMatrixMul {d : ℕ} (A : Mat d) (F : UnitCubeEuclideanL2Field d) : UnitCubeEuclideanL2Field d

Pointwise constant-matrix multiplication, packaged on the unit-cube Euclidean L² carrier.

Equations

• HCPolySupport.HighContrast.unitCubeEuclideanL2FieldConstMatrixMul A F = { toField := fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul A (F.toField x), euclideanMemL2 := ⋯ }

@[simp]

theorem HCPolySupport.HighContrast.unitCubeEuclideanL2FieldConstMatrixMul_apply {d : ℕ} (A : Mat d) (F : UnitCubeEuclideanL2Field d) (x : Vec d) : (unitCubeEuclideanL2FieldConstMatrixMul A F).toField x = matVecMul A (F.toField x)

noncomputable def HCPolySupport.HighContrast.continuousKCompetitorConstMatrixMul {d : ℕ} (A : Mat d) (G : ContinuousKCompetitor d) : ContinuousKCompetitor d

Apply the constant matrix A to a continuous K-functional competitor by taking linear combinations of its H¹ coordinates.

Equations

• HCPolySupport.HighContrast.continuousKCompetitorConstMatrixMul A G = { coord := fun (i : Fin d) => ∑ j : Fin d, A i j • G.coord j }

theorem HCPolySupport.HighContrast.continuousKFunctional_constMatrixMul_le {d : ℕ} (t : ↑ContinuousKScale) (A : Mat d) (F : UnitCubeEuclideanL2Field d) : continuousKFunctional t (unitCubeEuclideanL2FieldConstMatrixMul A F) ≤ ‖A‖ * continuousKFunctional t F

Constant matrix multiplication scales the continuous K-functional by at most the Euclidean matrix operator norm.

theorem HCPolySupport.HighContrast.continuousKSeminormIntegrand_constMatrixMul_le {d : ℕ} (sigma : ℝ) (A : Mat d) (F : UnitCubeEuclideanL2Field d) (t : ℝ) : continuousKSeminormIntegrand sigma (unitCubeEuclideanL2FieldConstMatrixMul A F) t ≤ ENNReal.ofReal (‖A‖ ^ 2) * continuousKSeminormIntegrand sigma F t

The pointwise continuous K-seminorm integrand scales by the square of the Euclidean matrix operator norm.

theorem HCPolySupport.HighContrast.continuousKSeminormIntegral_constMatrixMul_le {d : ℕ} (sigma : ℝ) (A : Mat d) (F : UnitCubeEuclideanL2Field d) : ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand sigma (unitCubeEuclideanL2FieldConstMatrixMul A F) t ≤ ENNReal.ofReal (‖A‖ ^ 2) * ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand sigma F t

The continuous K-seminorm integral scales by the square of the Euclidean matrix operator norm.

theorem HCPolySupport.HighContrast.unitCubeNormalizedEuclideanLpENorm_constMatrixMul_le {d : ℕ} (A : Mat d) (F : UnitCubeEuclideanL2Field d) : (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 (unitCubeEuclideanL2FieldConstMatrixMul A F).toField ≤ ENNReal.ofReal ‖A‖ * (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 F.toField

Constant matrix multiplication scales the normalized unit-cube Euclidean L² term by the Euclidean matrix operator norm.

theorem HCPolySupport.HighContrast.unitCubeNormalizedContinuousKEnergy_constMatrixMul_le {d : ℕ} (s : ↑FractionalOrder) (A : Mat d) (F : UnitCubeEuclideanL2Field d) : (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 (unitCubeEuclideanL2FieldConstMatrixMul A F).toField ^ 2 + ENNReal.ofReal (2 * ↑s) * ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand (↑s) (unitCubeEuclideanL2FieldConstMatrixMul A F) t ≤ ENNReal.ofReal (‖A‖ ^ 2) * ((unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 F.toField ^ 2 + ENNReal.ofReal (2 * ↑s) * ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand (↑s) F t)

Constant matrix multiplication scales the normalized quadratic continuous K-energy on the unit cube by the square of the Euclidean matrix operator norm.