NormalizedLoading

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The sigma0-loaded scalar response is one of the normalized block responses

The homogenization error mathcal E_{s,p,q}(cu_m; a, a0) of ABK26, Definition d.mathcal.E, is built from the doubled local responses bfJ(z + cu_l, bfA_0^{-1/2} e, bfA_0^{1/2} e; a), e in R^{2d}, |e| = 1,

whereas the subadditivity display opening the proof of l.J.sensitivity.no.conditions uses the scalar responses J(z + cu_{-h}, sigma0^{-1/2} e, sigma0^{1/2} e; a) with e in R^d.

This module supplies the exact passage between the two. For a0 = sigma0 I one has kappa0 = 0, hence bfA_0 = diag(sigma0, sigma0^{-1}) and, for a unit vector e in R^d, the doubled unit probe E := (e / sqrt 2, - e / sqrt 2) in R^{2d}, |E| = 1,

produces bfA_0^{-1/2} E = (c sigma0^{-1/2} e, -c sigma0^{1/2} e) and bfA_0^{1/2} E = (c sigma0^{1/2} e, -c sigma0^{-1/2} e) with c = 2^{-1/2}. CoarseGraining's scalar splitting of the doubled response then collapses the adjoint half-sum completely: the a-transpose summand is evaluated at the zero loading, and the a-summand carries the loading (sqrt 2 sigma0^{-1/2} e, sqrt 2 sigma0^{1/2} e), whose quadratic homogeneity contributes exactly the factor 2 that cancels the 1/2. Consequently J(R, sigma0^{-1/2} e, sigma0^{1/2} e; a) = bfJ(R, bfA_0^{-1/2} E, bfA_0^{1/2} E; a)

is a member of the value set whose supremum is the one-cube max_{|e| = 1}, and the supremum bound follows. Nothing here is an inequality of ellipticity type; the only quantitative input is the unconditional boundedness of the normalized block-response value set proved in CoarseGraining.

The normalization is stated through blockVecDot P (bfA_0 P) = 1, which is CoarseGraining's representation-free spelling of |bfA_0^{1/2} P| = 1; it is what lets us avoid ever computing the matrix square root bfA_0^{1/2} explicitly.

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.HomogBridge.scalarLoadingProbe {d : ℕ} (σ0 : ℝ) (e : HCPolySupport.Vec d) : HCPolySupport.BlockVec d

The doubled probe attached to a unit vector e and a positive scalar background sigma0: P = (c sigma0^{-1/2} e, -c sigma0^{1/2} e) with c = 2^{-1/2}.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.HomogBridge.scalarLoadingProbe σ0 e = ((√2)⁻¹ • (√σ0)⁻¹ • e, -(√2)⁻¹ • √σ0 • e)

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.HomogBridge.scalarLoadingCoProbe {d : ℕ} (σ0 : ℝ) (e : HCPolySupport.Vec d) : HCPolySupport.BlockVec d

The image of scalarLoadingProbe under the constant block matrix of sigma0 I, namely bfA_0^{1/2} E = (c sigma0^{1/2} e, -c sigma0^{-1/2} e).

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.HomogBridge.scalarLoadingCoProbe σ0 e = ((√2)⁻¹ • √σ0 • e, -(√2)⁻¹ • (√σ0)⁻¹ • e)

theorem Algsuperdiff.Section24.Sensitivity.Provider.HomogBridge.responseJ_scalarLoading_le_normalizedBlockResponseMax {d : ℕ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (R : HCPolySupport.TriadicCube d) {σ0 : ℝ} (hσ0 : 0 < σ0) {e : HCPolySupport.Vec d} (he : HCPolySupport.Book.Ch02.vecNorm e = 1) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) ((√σ0)⁻¹ • e) (√σ0 • e) ≤ HCPolySupport.Book.Ch02.normalizedBlockResponseMax R F (HCPolySupport.scalarMatrix σ0)

The local passage from the scalar sigma0-loading to the normalized block response. For a positive scalar background sigma0 and a unit vector e in R^d, the scalar response with loading (sigma0^{-1/2} e, sigma0^{1/2} e) on a triadic cube is bounded by the normalized block-response maximum of that cube, i.e. by the one-cube building block of mathcal E_{s,p,q}( .; a, sigma0).