High-contrast homogenization: Provider.Response.ReferenceWeakBridge

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

The concrete weak seminorm on the reference cube

For the identity grid, the aligned cells at depth j are exactly the triadic descendants of the origin cube at that depth. This identifies each slot of the concrete doubled-field seminorm with the finite Chapter-5 negative Besov seminorm. The statement keeps the normalized factor 3^{-st} visible; the inverse factor used by the div--curl estimate is consequently not hidden in a constant.

theorem HCPolySupport.HighContrast.Response.image_translateCube_alignedIndex_one_eq_descendantsAtDepth (d : ℕ) (t : ℤ) (j : ℕ) : Finset.image (fun (w : Fin d → ℤ) => translateCube w (originCube d (t - ↑j))) (alignedIndex 1 (t - ↑j) t) = descendantsAtDepth (originCube d t) j

At the identity grid, the aligned labels at depth j enumerate exactly the depth-j descendants of the origin cube.

theorem HCPolySupport.HighContrast.Response.cubeAverageVec_translateCube_eq_volumeAverageVec_standardCell {d : ℕ} (k : ℤ) (w : Fin d → ℤ) (F : Vec d → Vec d) : cubeAverageVec (translateCube w (originCube d k)) F = volumeAverageVec (standardCell d k w) F

A vector average on a translated reference cell is the corresponding triadic cube average. Passing between the open and half-open cube changes only a null boundary.

theorem HCPolySupport.HighContrast.Response.sqrt_depthAverage_fst_le_blockAvsumL2 {d : ℕ} (t : ℤ) (j : ℕ) (F : Vec d → BlockVec d) : √(cubeBesovNegativeVectorDepthAverage (originCube d t) (fun (x : Vec d) => (F x).1) j) ≤ blockAvsumL2 (alignedIndex 1 (t - ↑j) t) fun (w : Fin d → ℤ) => blockCellAverage (adaptedCellAt 1 (t - ↑j) w) F

Each Chapter-5 depth average of the first slot is bounded by the matching identity-grid doubled scale average.

theorem HCPolySupport.HighContrast.Response.sqrt_depthAverage_snd_le_blockAvsumL2 {d : ℕ} (t : ℤ) (j : ℕ) (F : Vec d → BlockVec d) : √(cubeBesovNegativeVectorDepthAverage (originCube d t) (fun (x : Vec d) => (F x).2) j) ≤ blockAvsumL2 (alignedIndex 1 (t - ↑j) t) fun (w : Fin d → ℤ) => blockCellAverage (adaptedCellAt 1 (t - ↑j) w) F

Each Chapter-5 depth average of the second slot is bounded by the matching identity-grid doubled scale average.

theorem HCPolySupport.HighContrast.Response.ofReal_partialSeminorm_fst_le_normalized_adaptedWeakSeminorm {d : ℕ} (t : ℤ) (s : ℝ) (N : ℕ) (F : Vec d → BlockVec d) : ENNReal.ofReal (cubeBesovNegativeVectorPartialSeminorm (originCube d t) s N fun (x : Vec d) => (F x).1) ≤ ENNReal.ofReal (3 ^ (-(s * ↑t))) * adaptedWeakSeminorm 1 t s F

Every finite Chapter-5 weak seminorm of the first slot is bounded by the normalized concrete identity-grid seminorm.

theorem HCPolySupport.HighContrast.Response.ofReal_partialSeminorm_snd_le_normalized_adaptedWeakSeminorm {d : ℕ} (t : ℤ) (s : ℝ) (N : ℕ) (F : Vec d → BlockVec d) : ENNReal.ofReal (cubeBesovNegativeVectorPartialSeminorm (originCube d t) s N fun (x : Vec d) => (F x).2) ≤ ENNReal.ofReal (3 ^ (-(s * ↑t))) * adaptedWeakSeminorm 1 t s F

Every finite Chapter-5 weak seminorm of the second slot is bounded by the normalized concrete identity-grid seminorm.