High-contrast homogenization: Provider.Response.AdaptedWeakChild

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

Weak seminorm control on one aligned child

The normalized first-power cell-average sum is bounded by its square-average counterpart. On a fixed descendant the latter costs only the square root of the number of siblings when compared with the parent cube. These two facts turn the terminal adapted weak seminorm into a uniform bound for every finite child-cube scalar seminorm.

theorem HCPolySupport.HighContrast.Response.cubeBesovCircPartialNorm_one_one_le_two_one {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (G : Vec d → ℝ) : cubeBesovCircPartialNorm Q s 1 1 N G ≤ cubeBesovCircPartialNorm Q s 2 1 N G

The endpoint inner L¹ descendant average is bounded by the normalized L² descendant average at every finite collection of depths.

theorem HCPolySupport.HighContrast.Response.descendantsAverage_le_card_mul_parentAverage {d : ℕ} {Q R : TriadicCube d} {H : ℕ} (hR : R ∈ descendantsAtDepth Q H) (j : ℕ) {F : TriadicCube d → ℝ} (hF : ∀ S ∈ descendantsAtDepth Q (H + j), 0 ≤ F S) : descendantsAverage R j F ≤ ↑(descendantsAtDepth Q H).card * descendantsAverage Q (H + j) F

One selected descendant average is bounded by the parent average times the number of descendants at the selected depth.

theorem HCPolySupport.HighContrast.Response.cubeBesovCircPartialNorm_child_le_sqrt_card_mul_parent {d : ℕ} {Q R : TriadicCube d} {H : ℕ} (hR : R ∈ descendantsAtDepth Q H) (s : ℝ) (N : ℕ) (G : Vec d → ℝ) : cubeBesovCircPartialNorm R s 1 1 N G ≤ √↑(descendantsAtDepth Q H).card * cubeBesovCircPartialNorm Q s 2 1 (H + N) G

A fixed depth-H descendant has at most the square-root cardinality loss against the parent's finite scalar circ norm.

theorem HCPolySupport.HighContrast.Response.ofReal_cubeBesovCircPartialNorm_child_rawPullback_le {d : ℕ} {q S : Mat d} (hq : Matrix.PosDef q) (hS : Matrix.PosDef S) {t : ℤ} {Q R : TriadicCube d} {H : ℕ} (hQ : Q = originCube d t) (hR : R ∈ descendantsAtDepth Q H) (N : ℕ) (F : Vec d → BlockVec d) (alpha : BlockCoord d) (hF₁ : MemVectorL2 (adaptedCell q t) fun (x : Vec d) => matVecMul S (F x).1) (hF₂ : MemVectorL2 (adaptedCell q t) fun (x : Vec d) => matVecMul S⁻¹ (F x).2) : ENNReal.ofReal (cubeBesovCircPartialNorm R (1 / 2) 1 1 N fun (y : Vec d) => toFullBlockVec (F (matVecMul q y)) alpha) ≤ ENNReal.ofReal √↑(descendantsAtDepth Q H).card * ENNReal.ofReal (cubeBesovScaleWeight (-(1 / 2)) Q) * ENNReal.ofReal (3 ^ (-(1 / 2 * ↑t))) * ENNReal.ofReal √(max (Book.Ch02.matrixFrobeniusNormSq S⁻¹) (Book.Ch02.matrixFrobeniusNormSq S)) * adaptedWeakSeminorm q t (1 / 2) fun (x : Vec d) => (matVecMul S (F x).1, matVecMul S⁻¹ (F x).2)

The scalar component of a raw affine pullback is bounded by the terminal metric weak seminorm, with the finite descendant and metric distortions kept explicit.