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

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

The integrated weak-norm estimate

This file integrates the pathwise weak bound over the coefficient law to assemble the weak-norm estimate e.response.weak.estimate for one family of response maximizers. The pathwise bound 3^{-t/2}[M_0^{1/2}(X_t - Y)] splits into three summands - the recent cell and averaged-defect sums, the old-scale tail carrying the optimizer energy, and the random-to-annealed recentring correction - each squared and integrated separately: the recent sums against the η^{1/Q} bound on the cell defects, the tail against the Q-th moment of the all-scale maximum through its good/bad branches, and the recentring against the Q-th moment of the two-sided all-scale maximum. The purely arithmetic composition of the three resulting constants into the printed bound is isolated as a single lemma independent of matrices, cells or measures.

The squared scale-average seminorm bound

The scale-average seminorm [X] of AK.HC (2.130) is defined in ResponseBlockObjects.lean as a real tsum; this file records its nonnegativity and the nonnegativity of the squared L² cell mean. The Jensen/partition bound, in squared form, bounds the seminorm itself (rather than 3^{-t/2} times it) by the L²(U_t) mean of the field.

theorem HCPolySupport.HighContrast.Multiscale.besovSeminorm_nonneg {d : ℕ} (t : ℤ) (avg : ℕ → (Fin d → ℤ) → BlockVec d) : 0 ≤ besovSeminorm t avg

The scale-average seminorm [X] of AK.HC (2.130) is nonnegative, the junk value of a divergent defining series being 0.

The per-family integrated weak energy

This module integrates the pathwise weak bound over the coefficient law and assembles the weak-norm estimate e.response.weak.estimate for one family of response maximizers.

The pathwise bound splits 3^{-t/2}[M_0^{1/2}(X_t - Y)] into three summands: the recent cell and averaged-defect sums, the old-scale tail carrying the optimizer energy, and the correction from the random cell average to the annealed centre. Squaring costs a factor three, and each square is then integrated separately: the recent sums against the η^{1/Q} bound on the cell defects, the tail against the Q-th moment of the all-scale maximum through the good/bad split at the cutoff 1, and the recentring against the Q-th moment bound on the two-sided all-scale maximum.

The arithmetic of the three constants is isolated in weakEstimate_arith_engine, which knows nothing about matrices or cells: it is the statement that an integral of a square dominated by three such terms is bounded by K_0^2 (L^±)^2 (A_H η^{1/Q} + B (3^{-αH})^2).

Elementary nonnegativity of the pathwise carriers

theorem HCPolySupport.HighContrast.Multiscale.weakOptimizerEnergy_nonneg {d : ℕ} (U : Set (Vec d)) (b : CoeffField d) (u : AHarmonicFunction b U) : 0 ≤ weakOptimizerEnergy U b u

The pathwise optimizer energy is a square root.

theorem HCPolySupport.HighContrast.Multiscale.RawOutput.of_le_csrc {d : ℕ} {γ : ℝ} {S : SelectionData} {ε σ Cglob Cprof Csrc Csrc' : ℝ} {H : ℕ} {Bresp : ℝ} {P : MeasureTheory.Measure (CoeffSpace d)} {E : BlockMat d} {Ψ : ℝ → ℝ} {Kg : ℝ} {Src : CoeffSpace d → ℝ} {B : ℝ} {jStar : ℕ} {F : BlockMat d} {s t : ℤ} (raw : RawOutput d γ S ε σ Cglob Cprof Csrc H Bresp P E Ψ Kg Src B jStar F s t) (h : Csrc' ≤ Csrc) : RawOutput d γ S ε σ Cglob Cprof Csrc' H Bresp P E Ψ Kg Src B jStar F s t

The raw response output is antitone in the source threshold constant.

The integration engine

The per-family integrated bound, minus sign

theorem HCPolySupport.HighContrast.Multiscale.respWeakEnergyOf_minus_le (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 → ∀ (u : (a : CoeffSpace d) → AHarmonicFunction (respCoeffMinus F a) (adaptedCell (respGrid jStar F) t)), (∀ (a : CoeffSpace d), IsResponseMaximizer (adaptedCell (respGrid jStar F) t) (respP (respMean P jStar F t) e) (respqMinus P jStar F t e) (respCoeffMinus F a) (u a)) → respWeakEnergyOf P (respGrid jStar F) t (respM0 F) (respCoeffMinus F) (respYMinus P jStar F t e) u ≤ (C * (3 ^ (-(Quenched.contrastAlpha γ * ↑H)) + CH H * η ^ (1 / (2 * ↑(bigQ d γ)))) * √(respKappa P jStar F s)) ^ 2

e.response.weak.estimate, one maximizer family, minus sign. For a single family u of response maximizers, 3^{-t} E[[M_0^{1/2}(X_t^- - Y^-)]^2] ≤ (C (3^{-αH} + C_H η^{1/(2Q)}) κ_s^{1/2})^2.

The pathwise three-term split is integrated by weakEstimate_arith_engine: the recent finite sums carry η^{1/Q}, the old-scale tail carries E[M^Q] + 3^{-2αH} through the good/bad split at the cutoff 1, and the random-to-annealed recentring carries η^{2/Q}; the product K_0^2 (L^-)^2 is then turned into C κ_s by the calibrated-block and load bounds.

The per-family integrated bound, plus sign

theorem HCPolySupport.HighContrast.Multiscale.respWeakEnergyOf_plus_le (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 → ∀ (u : (a : CoeffSpace d) → AHarmonicFunction (respCoeffPlus F a) (adaptedCell (respGrid jStar F) t)), (∀ (a : CoeffSpace d), IsResponseMaximizer (adaptedCell (respGrid jStar F) t) (respP (respMean P jStar F t) e) (respqPlus P jStar F t e) (respCoeffPlus F a) (u a)) → respWeakEnergyOf P (respGrid jStar F) t (respM0 F) (respCoeffPlus F) (respYPlus P jStar F t e) u ≤ (C * (3 ^ (-(Quenched.contrastAlpha γ * ↑H)) + CH H * η ^ (1 / (2 * ↑(bigQ d γ)))) * √(respKappa P jStar F s)) ^ 2

e.response.weak.estimate, one maximizer family, plus sign. The plus twin of respWeakEnergyOf_minus_le, on the adjoint recentred sample. For a single family u of response maximizers, 3^{-t} E[[M_0^{1/2}(X_t^+ - Y^+)]^2] ≤ (C (3^{-αH} + C_H η^{1/(2Q)}) κ_s^{1/2})^2.

The pathwise three-term split is integrated by weakEstimate_arith_engine: the recent finite sums carry η^{1/Q}, the old-scale tail carries E[M^Q] + 3^{-2αH} through the good/bad split at the cutoff 1, and the random-to-annealed recentring carries η^{2/Q}; the product K_0^2 (L^+)^2 is then turned into C κ_s by the calibrated-block and load bounds.