High-contrast homogenization: Provider.Quenched.SmallContrastSourceMomentDeepened

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

Deepened source-scale moments: the corrected split

The crude uniform moments 𝔪_N(K) of the normalized source scale are replaced by their deepened values. When the normalization scale sits Δ levels above the growth witness, the moment splits as

𝔼[(max 1 (S·3^{-(s_K+Δ)}))^N] ≤ 1 + 3^{-MΔ}·𝔪_{N+M}(K),

for every reserve order M: a scale-free unit floor plus a K-carrying excess that decays absolutely in the depth Δ. Downstream this is the three-channel source model — the unit floor feeds the lag channel with a K-free coefficient, the excess feeds the absolute channels whose K-burn-in is paid once. The proof is an event split: below the tail event the deepened variable collapses to 1; on the tail event the decayed tail-moment estimate applies.

theorem HCPolySupport.HighContrast.Quenched.normalizedSourceScale_shift {d : ℕ} (S : CoeffSpace d → ℝ) (sK : ℤ) {Delta : ℤ} (hDelta : 0 ≤ Delta) (a : CoeffSpace d) : normalizedSourceScale S (sK + Delta) a = max 1 (normalizedSourceScale S sK a * 3 ^ (-Delta))

The deepening identity. Normalizing Δ ≥ 0 levels deeper is the same as rescaling the normalized variable and re-flooring at 1.

theorem HCPolySupport.HighContrast.Quenched.lintegral_normalizedSourceScale_pow_deepened {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) (N M : ℕ) (hNM : 1 ≤ N + M) {Delta : ℤ} (hDelta : 0 ≤ Delta) : ∫⁻ (a : CoeffSpace d), ENNReal.ofReal (normalizedSourceScale S (sK + Delta) a ^ ↑N) ∂P ≤ ENNReal.ofReal (1 + 3 ^ (-(↑M * ↑Delta)) * (1 + 2 * ↑(N + M) * (1 + Real.log (growthBar K)) * growthBar K ^ IndependentSums.natTriangular (N + M)))

The deepened moment. Δ levels above the growth witness, the N-th moment of the normalized source scale is the unit floor plus a 3^{-MΔ}-decayed growthBar excess, for every reserve order M.

theorem HCPolySupport.HighContrast.Quenched.integral_normalizedSourceScale_deepened {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) (M : ℕ) {Delta : ℤ} (hDelta : 0 ≤ Delta) : ∫ (a : CoeffSpace d), normalizedSourceScale S (sK + Delta) a ∂P ≤ 1 + 3 ^ (-(↑M * ↑Delta)) * (1 + 2 * ↑(1 + M) * (1 + Real.log (growthBar K)) * growthBar K ^ IndependentSums.natTriangular (1 + M))

The deepened first moment, in Bochner form: the unit floor plus the decayed excess, ready for the mean-envelope step.