High-contrast homogenization: Provider.Regularity.PrintOrderDualBesovPerturbationAlgebra

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

Linear algebra for the cube full-dual vector norm

The vector norm used by the finite recurrence is the sum of its scalar full-dual component norms. This file records the corresponding triangle and constant-matrix bounds on L² fields. The induced matrix factor is written explicitly as the sum of the absolute values of its entries.

theorem HCPolySupport.HighContrast.cubeBesovDualFullNorm_add_le_of_memLp_two {d : ℕ} (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (f h : Vec d → ℝ) (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) (hh : MeasureTheory.MemLp h 2 (normalizedCubeMeasure Q)) : (cubeBesovDualFullNorm Q s 2 2 fun (x : Vec d) => f x + h x) ≤ cubeBesovDualFullNorm Q s 2 2 f + cubeBesovDualFullNorm Q s 2 2 h

The scalar full-dual norm is subadditive on L² fields.

theorem HCPolySupport.HighContrast.cubeBesovDualFullNorm_const_mul_le_of_memLp_two {d : ℕ} (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (c : ℝ) (f : Vec d → ℝ) (hf : MeasureTheory.MemLp f 2 (normalizedCubeMeasure Q)) : (cubeBesovDualFullNorm Q s 2 2 fun (x : Vec d) => c * f x) ≤ |c| * cubeBesovDualFullNorm Q s 2 2 f

Multiplication by a scalar acts on the scalar full-dual norm by its absolute value.

def HCPolySupport.HighContrast.dualBesovMatrixActionSize {d : ℕ} (A : Mat d) : ℝ

Entry-sum matrix size induced by the component-sum full-dual vector norm.

Equations

• HCPolySupport.HighContrast.dualBesovMatrixActionSize A = ∑ i : Fin d, ∑ j : Fin d, |A i j|

theorem HCPolySupport.HighContrast.dualBesovMatrixActionSize_nonneg {d : ℕ} (A : Mat d) : 0 ≤ dualBesovMatrixActionSize A

theorem HCPolySupport.HighContrast.abs_matrix_entry_le_l2_opNorm {d : ℕ} (A : Mat d) (i j : Fin d) : |A i j| ≤ ‖A‖

Every matrix entry is bounded by the Euclidean operator norm.

theorem HCPolySupport.HighContrast.dualBesovMatrixActionSize_le_dim_sq_mul_norm {d : ℕ} (A : Mat d) : dualBesovMatrixActionSize A ≤ ↑d ^ 2 * ‖A‖

The entry-sum action size is controlled by the Euclidean operator norm with the finite-dimensional factor forced by the component-sum vector norm.

theorem HCPolySupport.HighContrast.dualBesovMatrixActionSize_le_dim_sq_mul_ellipticity {d : ℕ} {lam Lam : ℝ} {A : Mat d} (hA : IsEllipticMatrix lam Lam A) : dualBesovMatrixActionSize A ≤ ↑d ^ 2 * Lam

An ellipticity upper bound controls the induced entry-sum action size.

theorem HCPolySupport.HighContrast.cubeScaleNormalizedDualNegativeBesovVectorNormTwo_matVecMul_le {d : ℕ} (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (A : Mat d) (F : Vec d → Vec d) (hF : MemVectorL2 (cubeSet Q) F) : (cubeScaleNormalizedDualNegativeBesovVectorNormTwo Q s fun (x : Vec d) => matVecMul A (F x)) ≤ dualBesovMatrixActionSize A * cubeScaleNormalizedDualNegativeBesovVectorNormTwo Q s F

A fixed matrix acts continuously on the component-sum cube full-dual vector norm, with the exact entry-sum action size.

theorem HCPolySupport.HighContrast.cubeScaleNormalizedDualNegativeBesovVectorNormTwo_add_le {d : ℕ} (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (F G : Vec d → Vec d) (hF : MemVectorL2 (cubeSet Q) F) (hG : MemVectorL2 (cubeSet Q) G) : (cubeScaleNormalizedDualNegativeBesovVectorNormTwo Q s fun (x : Vec d) => F x + G x) ≤ cubeScaleNormalizedDualNegativeBesovVectorNormTwo Q s F + cubeScaleNormalizedDualNegativeBesovVectorNormTwo Q s G

Triangle inequality for the component-sum cube full-dual vector norm.