High-contrast homogenization: Entry.Response.Kernel.WeakEstimateFenchelBound

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

The pathwise Fenchel and Loewner bounds for the weak quantity

Restricting the cell-average half of AK.HC (2.15) to an arbitrary triadic subcell of the response cell, this file bounds the squared doubled cell average of the optimizer state there by the same Fenchel-derived quadratic form, and combines it with the coarse-block envelope of the all-scale maximum to bound the per-scale terms entering the scale-average seminorm of AK.HC (2.130). It assembles the resulting per-scale bounds into the pathwise estimate e.response.weak.estimate of the squared seminorm of the doubled optimizer state. It closes with the all-scale Loewner bound p.response.transfer - the operator-norm envelope that dominates the response grid's terminal cell also dominates every triadic subcell, with the depth-dependent contrast weight made explicit - and the elementary quadratic-form algebra (congruence, scaling, a Loewner comparison, a block sum) that transports it.

The Fenchel bound on a triadic subcell of the response cell

The cell-average half of AK.HC (2.15) restricted to a triadic subcell adaptedCellAtCenter q (t - n) w of the response cell U_t = adaptedCell q t: a field harmonic on the whole cell restricts to the subcell, its gradient — hence its optimizer field and scalar variation energy integrand — is unchanged, and the squared doubled cell average of the optimizer field over the subcell is controlled by the pathwise symmetric energy of the field times any positive constant K that bounds above the quadratic form of the coarse block of b on the subcell augmented by the swap block 𝐑.

theorem HCPolySupport.HighContrast.Multiscale.blockVecDot_cellAverage_subcell_le {d : ℕ} [NeZero d] {q : Mat d} (hq : IsUnit q) (t : ℤ) (n : ℕ) {w : Fin d → ℤ} (hw : w ∈ triadicIndexBox d n) {lam Lam : ℝ} {b : CoeffField d} (hEll : IsEllipticFieldOn lam Lam (adaptedCell q t) b) (v : AHarmonicFunction b (adaptedCell q t)) (K : ℝ) (hK : 0 < K) (hB : ∀ (X : BlockVec d), blockVecDot X (blockMatVecMul (ofFullBlockMat (toFullBlockMat (coarseBlockMatrix (adaptedCellAtCenter q (t - ↑n) w) b) + toFullBlockMat (blockSwap d))) X) ≤ K * blockVecDot X X) : blockVecDot (cellAverage (adaptedCellAtCenter q (t - ↑n) w) (optimizerField b v)) (cellAverage (adaptedCellAtCenter q (t - ↑n) w) (optimizerField b v)) ≤ K * volumeAverage (adaptedCellAtCenter q (t - ↑n) w) (scalarVariationEnergyIntegrand b v)

The cell-average energy bound on a triadic subcell of the response cell: for v harmonic on the response cell U_t, the squared doubled cell average over the depth-n subcell adaptedCellAtCenter q (t - n) w of its optimizer field is bounded by the pathwise symmetric energy of the field over that subcell times any positive constant K that bounds above the quadratic form of the coarse block of b on the subcell augmented by the swap block 𝐑. This is the cell-average half of AK.HC (2.15) on a subcell of U_t; the proof restricts v to the subcell and applies the cell-average bound there.

The pathwise per-scale bound for the weak-quantity integrand

The scale-average seminorm [·] of AK.HC (2.130) is built from the squared L² cell means of the optimizer state on the depth-n triadic subcells of the response cell. This file records the pathwise bound those subcell terms satisfy: after the test block S and the shift Y are applied, the normalized sum over the subcells is controlled by the pathwise symmetric energy of the harmonic field on the response cell. The estimate chains the cell-average half of the Fenchel bound (2.15) on each subcell with the exact partition identity of the subcell energy averages.

theorem HCPolySupport.HighContrast.Multiscale.avsum_optimizerState_sq_le_of_inputs {d : ℕ} [NeZero d] {q : Mat d} (hq : IsUnit q) (t : ℤ) (n : ℕ) {lam Lam : ℝ} {b : CoeffField d} (hEll : IsEllipticFieldOn lam Lam (adaptedCell q t) b) (v : AHarmonicFunction b (adaptedCell q t)) (S : BlockMat d) (Y : BlockVec d) (kS : ℝ) (hkS : 0 ≤ kS) (hS : ∀ (X : BlockVec d), blockVecDot (blockMatVecMul S X) (blockMatVecMul S X) ≤ kS * blockVecDot X X) (K : ℝ) (hK : 0 < K) (hB : ∀ w ∈ triadicIndexBox d n, ∀ (X : BlockVec d), blockVecDot X (blockMatVecMul (ofFullBlockMat (toFullBlockMat (coarseBlockMatrix (adaptedCellAtCenter q (t - ↑n) w) b) + toFullBlockMat (blockSwap d))) X) ≤ K * blockVecDot X X) (hint : MeasureTheory.IntegrableOn (scalarVariationEnergyIntegrand b v) (adaptedCell q t) MeasureTheory.volume) : (↑(triadicIndexBox d n).card)⁻¹ * ∑ w ∈ triadicIndexBox d n, blockVecDot (blockMatVecMul S (cellAverage (adaptedCellAtCenter q (t - ↑n) w) (optimizerField b v) - Y)) (blockMatVecMul S (cellAverage (adaptedCellAtCenter q (t - ↑n) w) (optimizerField b v) - Y)) ≤ kS * (2 * (K * volumeAverage (adaptedCell q t) (scalarVariationEnergyIntegrand b v)) + 2 * blockVecDot Y Y)

The pathwise per-scale bound for the weak-quantity integrand e.response.weak.estimate: for a b-harmonic field v on the response cell U_t = adaptedCell q t, a test block S with |S X|² ≤ kS |X|², a shift Y, and a constant K that bounds the coarse block of b augmented by the swap block 𝐑 on every depth-n triadic subcell, the normalized sum over the 3 ^ (n d) subcells of the squared length of S applied to the shifted subcell average of the optimizer field of v is at most kS (2 K ⟨∇v ⬝ symm(b) ∇v⟩_{U_t} + 2 |Y|²). The proof applies the cell-average half of the Fenchel bound (2.15) on each subcell, averages the subcell energy over the exact partition of U_t, and expands the shift; this is the pathwise input of the scale-average seminorm bound AK.HC (2.130).

The pathwise seminorm bound by the cell energy

The scale-average seminorm [·] of AK.HC (2.130) is a sum of per-scale cell averages. The per-scale bound avsum_optimizerState_sq_le_of_inputs controls each scale by the pathwise cell energy with a coarse-block envelope K = K₀ · 3 ^ (ρ n), while the summation besovSeminorm_sq_le_of_scale_bound accepts any per-scale majorant A · 3 ^ (ρ n) with ρ < 1. This file chains the two: the envelope and the shift are monotone in the geometric factor 3 ^ (ρ n) ≥ 1, so the per-scale bound can be rewritten in the majorant shape with the geometric loss absorbed into the coefficient A. This is the pathwise input e.response.weak.estimate into the squared scale-average seminorm bound AK.HC (2.130).

theorem HCPolySupport.HighContrast.Multiscale.besovSeminorm_sq_optimizerState_le_of_scale_bounds {d : ℕ} [NeZero d] {q : Mat d} (hq : IsUnit q) (t : ℤ) (ρ : ℝ) (hρ0 : 0 ≤ ρ) (hρ1 : ρ < 1) {lam Lam : ℝ} {b : CoeffField d} (hEll : IsEllipticFieldOn lam Lam (adaptedCell q t) b) (v : AHarmonicFunction b (adaptedCell q t)) (S : BlockMat d) (Y : BlockVec d) (kS : ℝ) (hkS : 0 ≤ kS) (hS : ∀ (X : BlockVec d), blockVecDot (blockMatVecMul S X) (blockMatVecMul S X) ≤ kS * blockVecDot X X) (K₀ : ℝ) (hK₀ : 0 < K₀) (hB : ∀ (n : ℕ), ∀ w ∈ triadicIndexBox d n, ∀ (X : BlockVec d), blockVecDot X (blockMatVecMul (ofFullBlockMat (toFullBlockMat (coarseBlockMatrix (adaptedCellAtCenter q (t - ↑n) w) b) + toFullBlockMat (blockSwap d))) X) ≤ K₀ * 3 ^ (ρ * ↑n) * blockVecDot X X) (hint : MeasureTheory.IntegrableOn (scalarVariationEnergyIntegrand b v) (adaptedCell q t) MeasureTheory.volume) (hEnn : 0 ≤ volumeAverage (adaptedCell q t) (scalarVariationEnergyIntegrand b v)) : (besovSeminorm t fun (n : ℕ) (z : Fin d → ℤ) => blockMatVecMul S (cellAverage (adaptedCellAtCenter q (t - ↑n) z) (optimizerField b v) - Y)) ^ 2 ≤ (1 - 3 ^ ((ρ - 1) / 2))⁻¹ ^ 2 * (3 ^ ↑t * (kS * (2 * (K₀ * volumeAverage (adaptedCell q t) (scalarVariationEnergyIntegrand b v)) + 2 * blockVecDot Y Y)))

The pathwise bound of the squared scale-average seminorm AK.HC (2.130) by the cell energy, with the geometric loss absorbed. For a b-harmonic field v on the response cell U_t = adaptedCell q t, a test block S with |S X|² ≤ kS |X|², a shift Y, and a coarse-block envelope of the augmented block on every depth-n triadic subcell of the form K₀ · 3 ^ (ρ n) with ρ < 1, the squared scale-average seminorm of the applied, shifted cell averages of the optimizer field is at most ((1 - 3 ^ ((ρ - 1) / 2))⁻¹)² times 3 ^ t (kS (2 K₀ ⟨∇v ⬝ symm(b) ∇v⟩_{U_t} + 2 |Y|²)). The proof applies the per-scale pathwise bound at envelope K₀ · 3 ^ (ρ n), then uses 3 ^ (ρ n) ≥ 1 and the nonnegativity of the energy, the shift and kS to move the geometric factor onto the whole per-scale majorant, so that the scale-weighted summation e.response.weak.estimate of AK.HC (2.130) applies.

The all-scale Loewner bound on every triadic subcell

coarseBlock_le_one_add_respAllScaleMax bounds only the terminal cell of the response grid by (1 + respAllScaleMax) E_t. The all-scale maximum (p.response.transfer) is a supremum over every depth, so the same Loewner bound holds on every triadic subcell, with the depth-n weight 3 ^ (Quenched.contrastRho γ * n) made explicit: the weighted normalized recentred block of the depth-n cell enters the defining set of the maximum, so the depth-n spectral bound is 3 ^ (Quenched.contrastRho γ * n) * respAllScaleMax.

theorem HCPolySupport.HighContrast.Multiscale.coarseBlock_subcell_le_one_add_scaled_respAllScaleMax (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ Kg Src) (jStar : ℕ) (hj : 2 * d ≤ 3 ^ jStar) (F : BlockMat d) (hm : Matrix.PosDef (explicitCanonicalMetric F)) (t : ℤ) : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (n : ℕ), ∀ z ∈ triadicIndexBox d n, BlockMatLoewnerLE (coarseBlock (adaptedCellAtCenter (respGrid jStar F) (t - ↑n) z) a) (blockScale (1 + 3 ^ (Quenched.contrastRho γ * ↑n) * respAllScaleMax P γ jStar F t a) (respMean P jStar F t))

The all-scale Loewner bound on every triadic subcell (p.response.transfer): for P-a.e. sample a, every depth-n cell of the response grid is Loewner-dominated by (1 + 3 ^ (Quenched.contrastRho γ * n) * respAllScaleMax) · respMean, with the depth weight explicit.

Deterministic glue facts for the weak-quantity bound

Four independent algebraic facts used to propagate the quadratic-form bounds of the coarse blocks through the recentring and normalization steps of the weak-quantity bound.

• qform_blockCongr_le transports a quadratic-form bound through the congruence Gᵀ A G, using that the flattened quadratic form of blockCongr G A is the form of A evaluated on G X.
• qform_le_of_loewner turns a Loewner comparison against a scalar multiple c E into a scalar multiple of the quadratic-form bound of E.
• qform_add_blockSwap_le adds the swap block 𝐑 to a bounded block and pays exactly one unit of the identity form, by the arithmetic-geometric inequality 2 x · y ≤ x · x + y · y.
• volumeAverage_vecDot_optimizerField_eq identifies the doubled energy of the optimizer state with the symmetric part of the coefficient: ξ · (M ξ) = ξ · (symmPart M) ξ.

Paper: the response quadratic form AK.HC (2.15).

theorem HCPolySupport.HighContrast.Multiscale.qform_blockCongr_le {d : ℕ} (G A : BlockMat d) (K kG : ℝ) (hK : 0 ≤ K) (hA : ∀ (X : BlockVec d), blockVecDot X (blockMatVecMul A X) ≤ K * blockVecDot X X) (hG : ∀ (X : BlockVec d), blockVecDot (blockMatVecMul G X) (blockMatVecMul G X) ≤ kG * blockVecDot X X) (X : BlockVec d) : blockVecDot X (blockMatVecMul (blockCongr G A) X) ≤ K * kG * blockVecDot X X

A congruence Gᵀ A G transports a quadratic-form bound: if A is bounded by K and G is bounded by kG, then blockCongr G A is bounded by K kG. The proof evaluates the congruence form on G X and composes the two bounds. Paper: AK.HC (2.15).

theorem HCPolySupport.HighContrast.Multiscale.qform_le_of_loewner {d : ℕ} {A E : BlockMat d} {c kE : ℝ} (hc : 0 ≤ c) (hA : BlockMatLoewnerLE A (blockScale c E)) (hE : ∀ (X : BlockVec d), blockVecDot X (blockMatVecMul E X) ≤ kE * blockVecDot X X) (X : BlockVec d) : blockVecDot X (blockMatVecMul A X) ≤ c * kE * blockVecDot X X

A Loewner comparison A ≤ c E combines with a quadratic-form bound E ≤ kE on E into the bound A ≤ c kE on the identity form. Paper: AK.HC (2.15).

theorem HCPolySupport.HighContrast.Multiscale.qform_add_blockSwap_le {d : ℕ} {A : BlockMat d} {K : ℝ} (hA : ∀ (X : BlockVec d), blockVecDot X (blockMatVecMul A X) ≤ K * blockVecDot X X) (X : BlockVec d) : blockVecDot X (blockMatVecMul (ofFullBlockMat (toFullBlockMat A + toFullBlockMat (blockSwap d))) X) ≤ (K + 1) * blockVecDot X X

Adding the swap block 𝐑 to a quadratically bounded block costs exactly one unit of the identity form: X ⬝ (A + 𝐑) X ≤ (K + 1) (X ⬝ X). The swap contributes the off-diagonal pairing 2 x · y, which the arithmetic-geometric inequality bounds by x · x + y · y. Paper: AK.HC (2.15).

theorem HCPolySupport.HighContrast.Multiscale.volumeAverage_vecDot_optimizerField_eq {d : ℕ} [NeZero d] (V : Set (Vec d)) (b : CoeffField d) (v : AHarmonicFunction b V) : (volumeAverage V fun (x : Vec d) => vecDot (optimizerField b v x).1 (optimizerField b v x).2) = volumeAverage V (scalarVariationEnergyIntegrand b v)

The doubled energy of the optimizer state is the symmetric energy: pointwise, ξ · (b x ξ) = ξ · (symmPart (b x) ξ) because the antisymmetric part contributes nothing to the quadratic form. The optimizer field is (∇v, b ∇v) and the variation energy integrand is ∇v · (symmPart b) ∇v, so the two volume averages agree.