High-contrast homogenization: Entry.Response.Core.AbsoluteScaleDefect

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

The absolute all-scale defect bound

This file proves the unsigned counterpart of the all-scale energy-and-defect estimate of p.response.transfer: it bounds respAllScaleAbs by the fluctuation and source terms and shows it is nonnegative whenever every term in the defining family is. It proves the operator norm of a block is controlled by its spectral bound and by the Loewner order, that the difference of a normalized block from the identity is bounded in norm, and that the coarse block and the normalized block on an adapted cell are positive semidefinite.

The two-sided response transfer estimate

The two-sided carrier respAllScaleAbs

The ONE-SIDED all-scale maximum is respAllScaleMax (ResponseBlockObjects.lean). The η-kernel twins consume the TWO-SIDED respAllScaleAbs (ResponseBlockObjects.lean); response_allscale_abs below discharges that premise. The two-sided bound has the one-sided bound's statement verbatim except for the carrier, so it is exactly the same estimate with respAllScaleAbs in place of respAllScaleMax.

The route is the same one, two-sided at every step:

• the Step-5 split is the TRIANGLE INEQUALITY, not a Loewner comparison: normalizedBlock is linear in its first argument, so N^q_{k,t}(z) - I = V^q_{k,t}(z) + (P^q_{k,t} - I) (split_term_le);
• the fluctuation summand V^q_{k,t}(z) is ALREADY carried by blockOpNorm in fluctuationHistory (HCPoly/Entry/Setup/Profile.lean), so scale_index_le applies with no change at all;
• the mean summand P^q_{k,t} - I is positive semidefinite (normalizedBlock_gap_posSemidef through Annealed.adaptedMean_antitone), and on a positive semidefinite block the spectral positive part IS the operator norm, so mean_part_le_determinantDrift carries blockOpNorm on the left (blockOpNorm_mean_part_le_determinantDrift);
• only the source branch k < j_* is genuinely one-sided. There the lower side is free -- coarseBlock (adaptedCellAtCenter...) a >= 0, hence N^q_{k,t}(z) >= 0 and N^q_{k,t}(z) - I >= -I -- and costs the single extra summand 3^{-rho n} |I| <= 3^{-rho n}. That branch runs only for n > (t - j_*).toNat, where 3^{-rho n} <= 3^{-rho_max (t - j_*)} <= eta^{1/Q} / C_s by RespSourceSmall (source_term_le), so the extra summand is eta-small -- which is exactly what the conclusion <= C eta needs.

No new analytic input is used. The only positive semidefiniteness invoked is Annealed.blockPosDef_coarseBlock_adapted (AdaptedDomainLocality.lean) at the aligned cell centre.

theorem HCPolySupport.HighContrast.Multiscale.fluctuation_term_le (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) (mt : Mat d) (hm : Matrix.PosDef mt) (t : ℤ) (ht : ↑jStar ≤ t) (a : CoeffSpace d) (n : ℕ) (hn : n ∈ Set.Icc 0 (t - ↑jStar).toNat) (z : Fin d → ℤ) (hz : z ∈ triadicIndexBox d n) : 3 ^ (-(Quenched.contrastRho γ * ↑n)) * blockOpNorm (blockSub (normalizedBlock (coarseBlock (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar mt) (t - ↑n) z) a) (adaptedMean P (Geometry.explicitRoundedGrid jStar mt) t)) (Book.Ch02.blockIdentity d)) ≤ (⨆ j ∈ Set.Icc (↑jStar) t, 3 ^ (-↑(bigQ d γ) * rhoMax d γ * (↑t - ↑j)) * ⨆ y ∈ adaptedLatticeAtScale (Geometry.explicitRoundedGrid jStar mt) j ∩ adaptedCell (Geometry.explicitRoundedGrid jStar mt) t, blockOpNorm (normalizedFluctuation P (Geometry.explicitRoundedGrid jStar mt) j t y a) ^ bigQ d γ) ^ (↑(bigQ d γ))⁻¹ + determinantDrift P γ (Geometry.explicitRoundedGrid jStar mt) jStar t

The fluctuation-and-mean branch, two-sided (p.response.transfer): the two-sided counterpart of fluctuation_term_le_max. Both summands of the triangle split are already two-sided -- the fluctuation part is blockOpNorm in fluctuationHistory itself, and the mean part is positive semidefinite -- so this branch costs nothing extra at all.

theorem HCPolySupport.HighContrast.Multiscale.source_term_le (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 : ℤ) (ht : ↑jStar ≤ t) (hcube : adaptedCell (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t ⊆ centeredCube d (2 * ↑jStar)) (C₀ Cn Cs η : ℝ) (hC₀ : 0 < C₀) (hCn : 0 < Cn) (hCs : 0 < Cs) (X : CoeffSpace d → ℝ) (a : CoeffSpace d) (hXa : 0 < X a) (hpath : ∀ (mm : Mat d), Matrix.PosDef mm → ∀ (j : ℤ) (y : Vec d), adaptedCellTranslate (Geometry.explicitRoundedGrid jStar mm) j y ⊆ centeredCube d (2 * ↑jStar) → BlockMatLoewnerLE (coarseBlock (adaptedCellTranslate (Geometry.explicitRoundedGrid jStar mm) j y) a) (blockScale (C₀ * √(‖mm‖ * ‖mm⁻¹‖) * X a * 3 ^ (γ * max (↑jStar - ↑j) 0)) E)) (hnormt : BlockMatLoewnerLE E (blockScale (Cn * aspectRatio E * √(‖explicitCanonicalMetric F‖ * ‖(explicitCanonicalMetric F)⁻¹‖)) (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t))) (hsrcsmall : Cs * aspectRatio E * (‖explicitCanonicalMetric F‖ * ‖(explicitCanonicalMetric F)⁻¹‖) * 3 ^ (-(rhoMax d γ * (↑t - ↑jStar))) ≤ η ^ (1 / ↑(bigQ d γ))) (n : ℕ) (hn : (t - ↑jStar).toNat < n) (z : Fin d → ℤ) (hz : z ∈ triadicIndexBox d n) : 3 ^ (-(Quenched.contrastRho γ * ↑n)) * blockOpNorm (blockSub (normalizedBlock (coarseBlock (adaptedCellAtCenter (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) (t - ↑n) z) a) (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t)) (Book.Ch02.blockIdentity d)) ≤ C₀ * Cn / Cs * η ^ (1 / ↑(bigQ d γ)) * X a + η ^ (1 / ↑(bigQ d γ)) / Cs

The source branch, two-sided (p.response.transfer): the two-sided counterpart of source_term_le_max. The upper Loewner side is unchanged; the lower side is coarseBlock (adaptedCellAtCenter...) a >= 0 normalized by E_t, which costs the single extra summand 3^{-rho n} |I| <= 3^{-rho n}. Because this branch runs only for n > (t - j_*).toNat, 3^{-rho n} <= 3^{-rho_max (t - j_*)} and RespSourceSmall makes that at most eta^{1/Q} / C_s -- so the extra summand is eta-small, which is what the two-sided conclusion needs.

theorem HCPolySupport.HighContrast.Multiscale.respAllScaleAbs_nonneg {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (a : CoeffSpace d) : 0 ≤ respAllScaleAbs P γ jStar F t a

respAllScaleAbs is nonnegative: every member of the defining set is, and Real.sSup takes the junk value 0 on an unbounded set.

theorem HCPolySupport.HighContrast.Multiscale.respAllScaleAbs_le_of_forall {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (a : CoeffSpace d) (M : ℝ) (hM : 0 ≤ M) (h : ∀ (n : ℕ), ∀ z ∈ triadicIndexBox d n, 3 ^ (-(Quenched.contrastRho γ * ↑n)) * blockOpNorm (blockSub (normalizedBlock (coarseBlock (adaptedCellAtCenter (respGrid jStar F) (t - ↑n) z) a) (respMean P jStar F t)) (Book.Ch02.blockIdentity d)) ≤ M) : respAllScaleAbs P γ jStar F t a ≤ M

The bounded-supremum lemma for the two-sided all-scale maximum, the twin of respAllScaleMax_le_of_forall: a single nonnegative bound valid at every scale and index bounds A pathwise, whether or not the family is bounded above.