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

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

The weak-norm estimate, assembled over both signs

The weak-norm estimate response_weak_estimate - e.response.weak.estimate, part 4 of the decomposition adapted_response_core of R1 - bounds, for each sign of the recentring, the supremum over families of response maximizers of the per-family weak energy by (C(3^{-αH} + C_H η^{1/(2Q)}) κ_s^{1/2})^2. It is obtained from the two per-family bounds by taking the larger of the two constants, using the scale-average seminorm of the cell-average lemma on the selected grid rather than the compact-test dual norm of the theorem statements. Bundled with this assembly are two cutoff-argument facts: the integrated centred cutoff decomposition of AK.HC (3.45)-(3.54), and the defining properties of the response cutoff class IsResponseCutoff.

The weak-norm estimate, assembled over the two signs

response_weak_estimate_of_route is e.response.weak.estimate: the supremum over families of response maximizers of the per-family weak energy is bounded by (C (3^{-αH} + C_H η^{1/(2Q)}) κ_s^{1/2})^2 for each sign. It is obtained from the two per-family bounds by taking the larger of the two constants and reading the supremum off through the two conjuncts of the definition of W^±.

theorem HCPolySupport.HighContrast.Multiscale.response_weak_estimate_of_route (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (Cc Ce Cl Cm Cs : ℝ) (hCc : 0 < Cc) (hCe : 0 < Ce) (hCl : 0 < Cl) (hCm : 0 < Cm) (hCs : 0 < Cs) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (C : ℝ) (CH : ℕ → ℝ), 0 < C ∧ (∀ (n : ℕ), 0 < CH n) ∧ ∀ (ε σ : ℝ), ε ∈ Set.Ioc 0 S.eps0 → σ ∈ Set.Ioc 0 ε → ∀ (Cglob Cprof Bresp : ℝ), 0 ≤ Cglob → ∀ (H : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ), RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ Kg Src B jStar F s t → RespCalibrated Cc P jStar F s t → ∀ η ∈ Set.Ioo 0 (1 / 2), Cprof * σ ^ ((1 - γ) / 8) ≤ η → RespSourceSmall d γ Cs η E F jStar s t → ∫ (a : CoeffSpace d), respAllScaleAbs P γ jStar F t a ^ bigQ d γ ∂P ≤ Cm * η → ∀ (e : Vec d), vecDot e e = 1 → RespEnergyDefect Ce P jStar F s t e → RespLoadMean Cl P jStar F s t e → RespWeakBound C CH d γ P jStar F H η s t e

e.response.weak.estimate. For each sign, W^± ≥ 0 and (W^±)^{1/2} ≤ C (3^{-αH} + C_H η^{1/(2Q)}) κ_s^{1/2}.

W^± is a supremum over all families of response maximizers, so the bound follows from the per-family bounds respWeakEnergyOf_minus_le and respWeakEnergyOf_plus_le once the two constants are replaced by their maxima; the supremum is then bounded because every member of the defining set is.

R1 decomposition, part 4: the weak-norm estimate

The weak-norm estimate of the decomposition of R1 adapted_response_core is e.response.weak.estimate.

The concrete scale-average seminorm used here is the one of the cell-average lemma of the high-contrast reference, on the selected grid, not the compact-test dual norm of the theorem statements. The estimate splits as 3^{-αH} from the scales older than the response window plus C_H η^{1/(2Q)} from the recent cell fluctuations, the mean differences, and the correction from random to annealed centering. This is where the histories retained through the iteration enter the response argument: small fluctuations at the terminal scale alone would not control the cell averages in this seminorm.

The weak-norm estimate

theorem HCPolySupport.HighContrast.Multiscale.response_weak_estimate (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (S : SelectionData) (hS : S.Selects d γ) (Cc Ce Cl Cm Cs : ℝ) (hCc : 0 < Cc) (hCe : 0 < Ce) (hCl : 0 < Cl) (hCm : 0 < Cm) (hCs : 0 < Cs) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (C : ℝ) (CH : ℕ → ℝ), 0 < C ∧ (∀ (n : ℕ), 0 < CH n) ∧ ∀ (ε σ : ℝ), ε ∈ Set.Ioc 0 S.eps0 → σ ∈ Set.Ioc 0 ε → ∀ (Cglob Cprof Bresp : ℝ), 0 ≤ Cglob → ∀ (H : ℕ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (Kg : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ), RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ Kg Src B jStar F s t → RespCalibrated Cc P jStar F s t → ∀ η ∈ Set.Ioo 0 (1 / 2), Cprof * σ ^ ((1 - γ) / 8) ≤ η → RespSourceSmall d γ Cs η E F jStar s t → ∫ (a : CoeffSpace d), respAllScaleAbs P γ jStar F t a ^ bigQ d γ ∂P ≤ Cm * η → ∀ (e : Vec d), vecDot e e = 1 → RespEnergyDefect Ce P jStar F s t e → RespLoadMean Cl P jStar F s t e → RespWeakBound C CH d γ P jStar F H η s t e

The weak-norm estimate e.response.weak.estimate: (W^±)^{1/2} ≤ C (3^{-αH} + C_H η^{1/(2Q)}) κ_s^{1/2}, with α = (1-γ)/4.

K_0 = |M_0^{-1/2} Ê_t^± M_0^{-1/2}|^{1/2} ≤ C κ_s^{1/4}, and the variational bound on the mean of a gradient–solenoidal field holds on every Lipschitz cell, so the cell-average argument applies on the selected grid with exponent 1/2, decay exponent ρ, cutoff 1 and window H. The recent-cell differences contribute C_H K_0 L^± η^{1/(2Q)} through the mean penalty; the energy split at the cutoff 1 contributes C K_0 L^± (η^{1/2} + 3^{-αH}) using E[M^Q] ≤ C η; the random-to-annealed recentering costs the same order. Finally K_0 L^± ≤ C κ_s^{1/2} by the calibrated-block and load bounds.

The integrated centred cutoff decomposition (AK.HC (3.45)-(3.54))

The cutoff pairing cutoffPairingOnCellAux U φ Y b v tests the optimizer state X = (∇v, b ∇v) against the annealed mean Y of AK.HC (2.32), weighted by the cutoff φ. Its pathwise expansion exhibits the half-pairing as the cutoff-weighted half-energy cutoffHalfEnergyAux minus the two mean pairings plus half the self-pairing of Y.

Integrating that expansion against the law P and applying the triangle inequality exhibits the centred response as the sum of the absolute cutoff pairing, the absolute energy defect cutoffHalfEnergyAux - J, and the two integrated cutoff-mean terms. This is the first step of the variational calculation of e.response.cutoff.estimate (AK.HC (3.45)-(3.54)), taken before the products are separated by Young's inequality.

The statement is the integrated form of cutoff_halfPairing_eq_sub. The cell U and the coefficient b are arbitrary: no ellipticity of b, no boundedness of U, and no positivity of φ enter, only the integrabilities of the sample functions and of the coordinates of the optimizer state.

noncomputable def HCPolySupport.HighContrast.Multiscale.cutoffPairingOnCellAux {d : ℕ} (U : Set (Vec d)) (φ : Vec d → ℝ) (Y : BlockVec d) (b : CoeffField d) (v : AHarmonicFunction b U) : ℝ

The cutoff pairing term on the cell U: the cutoff-weighted recentred pairing (φ (X₁ - Y₁) · (X₂ - Y₂))_U of the optimizer state X = (∇v, b ∇v) at the annealed mean Y of AK.HC (2.32). This is the local spelling of the pairing consumed by the cutoff estimate of AK.HC (3.45)-(3.54).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.Multiscale.cutoffStateMeanAux {d : ℕ} (U : Set (Vec d)) (φ : Vec d → ℝ) (b : CoeffField d) (v : AHarmonicFunction b U) : BlockVec d

The cutoff-weighted mean of the doubled optimizer state X = (∇v, b ∇v) on the cell U: the pair whose coordinates are the cutoff averages of the coordinates of X. Its two components are the mean pairings appearing in the centred decomposition of AK.HC (3.45)-(3.54).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.Multiscale.cutoffHalfEnergyAux {d : ℕ} (U : Set (Vec d)) (φ : Vec d → ℝ) (b : CoeffField d) (v : AHarmonicFunction b U) : ℝ

The cutoff-weighted half-energy of the optimizer state X = (∇v, b ∇v): one half of the cutoff average of φ (X₁ · X₂). This is the energy term subtracted from the response on the right-hand side of the centred decomposition of AK.HC (3.45)-(3.54).

Equations

• One or more equations did not get rendered due to their size.

The defining properties of the response cutoff class

IsResponseCutoff qq t φ is the class of cutoffs used by the cutoff estimate e.response.cutoff.estimate: a function supported in the adapted cell HighContrast.adaptedCell qq t, bounded between 0 and 2, of volume average one there, and carrying the first- and second-derivative bounds at the scale 3 ^ t in qq-coordinates. Each defining property is exposed here as a named theorem, so that consumers can refer to a property by name rather than by a positional projection.

theorem HCPolySupport.HighContrast.Multiscale.IsResponseCutoff.nonneg {d : ℕ} {qq : Mat d} {t : ℤ} {φ : Vec d → ℝ} (h : IsResponseCutoff qq t φ) (x : Vec d) : 0 ≤ φ x

A cutoff φ of the class of the cutoff estimate e.response.cutoff.estimate is nonnegative everywhere.

theorem HCPolySupport.HighContrast.Multiscale.IsResponseCutoff.le_two {d : ℕ} {qq : Mat d} {t : ℤ} {φ : Vec d → ℝ} (h : IsResponseCutoff qq t φ) (x : Vec d) : φ x ≤ 2

A cutoff φ of the class of the cutoff estimate e.response.cutoff.estimate is bounded above by 2 everywhere.

theorem HCPolySupport.HighContrast.Multiscale.IsResponseCutoff.zero_of_notMem {d : ℕ} {qq : Mat d} {t : ℤ} {φ : Vec d → ℝ} (h : IsResponseCutoff qq t φ) (x : Vec d) : x ∉ adaptedCell qq t → φ x = 0

A cutoff φ of the class of the cutoff estimate e.response.cutoff.estimate vanishes at every point outside the adapted cell HighContrast.adaptedCell qq t.

theorem HCPolySupport.HighContrast.Multiscale.IsResponseCutoff.volumeAverage_eq_one {d : ℕ} {qq : Mat d} {t : ℤ} {φ : Vec d → ℝ} (h : IsResponseCutoff qq t φ) : volumeAverage (adaptedCell qq t) φ = 1

A cutoff φ of the class of the cutoff estimate e.response.cutoff.estimate has volume average one on the adapted cell HighContrast.adaptedCell qq t.

theorem HCPolySupport.HighContrast.Multiscale.IsResponseCutoff.lipschitz {d : ℕ} {qq : Mat d} {t : ℤ} {φ : Vec d → ℝ} (h : IsResponseCutoff qq t φ) : LipschitzWith (32 * ↑d ^ 2 * responseCutoffProfileConst * 3 ^ (-t)).toNNReal fun (y : Vec d) => φ (matVecMul qq y)

The pullback y ↦ φ (qq y) of a cutoff φ of the class of the cutoff estimate e.response.cutoff.estimate is Lipschitz with constant 32 * d ^ 2 * responseCutoffProfileConst * 3 ^ (-t).

theorem HCPolySupport.HighContrast.Multiscale.IsResponseCutoff.contDiff {d : ℕ} {qq : Mat d} {t : ℤ} {φ : Vec d → ℝ} (h : IsResponseCutoff qq t φ) : ContDiff ℝ (↑⊤) φ

A cutoff φ of the class of the cutoff estimate e.response.cutoff.estimate is smooth, i.e. C^∞.

theorem HCPolySupport.HighContrast.Multiscale.IsResponseCutoff.hasCompactSupport {d : ℕ} {qq : Mat d} {t : ℤ} {φ : Vec d → ℝ} (h : IsResponseCutoff qq t φ) : HasCompactSupport φ

A cutoff φ of the class of the cutoff estimate e.response.cutoff.estimate has compact support.

theorem HCPolySupport.HighContrast.Multiscale.IsResponseCutoff.tsupport_subset {d : ℕ} {qq : Mat d} {t : ℤ} {φ : Vec d → ℝ} (h : IsResponseCutoff qq t φ) : tsupport φ ⊆ adaptedCell qq t

The topological support of a cutoff φ of the class of the cutoff estimate e.response.cutoff.estimate is contained in the adapted cell HighContrast.adaptedCell qq t.