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

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

The response-transfer block objects

This file collects the objects used throughout the block-algebra decomposition of the response transfer p.response.transfer, near the canonical imbalance e.response.canonical.imbalance. It fixes the doubled block calculus — the block adjoint, the block congruence, the block square root and the block spectral bound — together with the block response energy, the block response mean and the block centred response built from a coarse coefficient block. It also introduces the cell average and the doubled optimizer field, the canonical mean of a scalar field, the annealed block of a coefficient, an all-scale Besov-type seminorm, and the predicate that a scalar field is a response cutoff. Only the notation and definitions the later decomposition is built from appear here, together with the definitional equation lemmas respLsqMinus_eq_quadratic, respLsqPlus_eq_quadratic and respWPlus_eq recording what respLsqMinus/respLsqPlus/ respWPlus unfold to.

Definitions for the response-transfer decomposition of p.response.transfer

Every definition here transcribes one object of Steps 3-6 of the printed proof of p.response.transfer near e.response.canonical.imbalance. Nothing here is a proof; the substantive steps of the decomposition are proved in CenteredEnergyIdentity and its supporting modules.

Fixed notation (Step 2, p.response.transfer):

• respGrid jStar F is the paper's grid q, i.e. Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F);
• respCell jStar F u is U_u;
• respMean P jStar F u is E_u = Ahom_{u,q};
• respKappa P jStar F u is kappa_u = d(E_u);
• xi = sqrt(eps) * sigma;
• respRatio P jStar F s t is r = det E_s / det E_t.

-- READING: marks each place where the printed text leaves a choice and this file fixes one.

The raw global-selection output

RawOutput bundles the hypotheses of the global-selection output that the response-transfer decomposition below is stated over.

structure HCPolySupport.HighContrast.Multiscale.RawOutput (d : ℕ) (γ : ℝ) (S : SelectionData) (ε σ Cglob Cprof Csrc : ℝ) (H : ℕ) (Bresp : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ) (B : ℝ) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) : Prop

The raw global-selection output, verbatim.

• prob : MeasureTheory.IsProbabilityMeasure P
• stat : IsStationaryLaw P
• unit : IsUnitRangeLaw P
• ell : CoarseEllipticityDagger P γ E Ψ K Src
• hB : max (S.B0 ε σ) Bresp ≤ B
• hj : 2 * d ≤ 3 ^ jStar
• hsrc : ⌈Cglob * (B + 1) * Real.logb 3 (2 + aspectRatio E) + Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar
• symm : IsSymmetricBlockMat F
• pos : Book.Ch02.BlockPosDef F
• hst : s < t
• ht : t = s + ↑H
• hs_lo : ↑jStar + ⌈B * Real.logb 3 (2 + aspectRatio E)⌉ ≤ s
• ht_hi : t ≤ ↑jStar + ⌈(B + Cglob) * Real.logb 3 (2 + aspectRatio E)⌉
• cube : adaptedCell (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) t ⊆ centeredCube d (2 * ↑jStar)
• calib_lo : BlockMatLoewnerLE (blockScale (1 - √ε * σ) F) (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) s)
• calib_hi : BlockMatLoewnerLE (adaptedMean P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) s) (blockScale (1 + √ε * σ) F)
• det : (↑d)⁻¹ * detIncrement P (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) s t < σ
• prof : max (max (profile P γ (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) jStar s s) (profile P γ (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) jStar s t)) (profile P γ (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) jStar t t) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) jStar s + determinantDrift P γ (Geometry.explicitRoundedGrid jStar (explicitCanonicalMetric F)) jStar t ≤ Cprof * σ ^ ((1 - γ) / 8)
• ecc : (‖explicitCanonicalMetric F‖ * ‖(explicitCanonicalMetric F)⁻¹‖) ^ (1 / 2) ≤ (2 + aspectRatio E) ^ Cglob

Step 2 notation (p.response.transfer)

noncomputable def HCPolySupport.HighContrast.Multiscale.respGrid {d : ℕ} (jStar : ℕ) (F : BlockMat d) : Mat d

The selected grid q of p.response.transfer.

Equations

• HCPolySupport.HighContrast.Multiscale.respGrid jStar F = HCPolySupport.HighContrast.Geometry.explicitRoundedGrid jStar (HCPolySupport.HighContrast.explicitCanonicalMetric F)

def HCPolySupport.HighContrast.Multiscale.respCell {d : ℕ} (jStar : ℕ) (F : BlockMat d) (u : ℤ) : Set (Vec d)

U_u (p.response.transfer).

Equations

• HCPolySupport.HighContrast.Multiscale.respCell jStar F u = HCPolySupport.HighContrast.adaptedCell (HCPolySupport.HighContrast.Multiscale.respGrid jStar F) u

noncomputable def HCPolySupport.HighContrast.Multiscale.respMean {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (u : ℤ) : BlockMat d

E_u = Ahom_{u,q} (p.response.transfer).

Equations

• HCPolySupport.HighContrast.Multiscale.respMean P jStar F u = HCPolySupport.HighContrast.adaptedMean P (HCPolySupport.HighContrast.Multiscale.respGrid jStar F) u

noncomputable def HCPolySupport.HighContrast.Multiscale.respKappa {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (u : ℤ) : ℝ

kappa_u = d(E_u) (p.response.transfer).

Equations

• HCPolySupport.HighContrast.Multiscale.respKappa P jStar F u = HCPolySupport.HighContrast.Multiscale.canonicalImbalance (HCPolySupport.HighContrast.Multiscale.respMean P jStar F u)

noncomputable def HCPolySupport.HighContrast.Multiscale.respRatio {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) : ℝ

r = det E_s / det E_t (p.response.transfer). -- READING: det is the determinant of the flattened 2d x 2d matrix, as everywhere else in the development (blockLogDet, one_le_det_adaptedMean).

Equations

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

Step 3, the response coordinates (p.response.transfer)

noncomputable def HCPolySupport.HighContrast.Multiscale.respSkew {d : ℕ} (A : BlockMat d) : Mat d

h_t = (K - K^t)/2, the skew half of the Schur coefficient K of E_t (p.response.transfer).

Equations

• HCPolySupport.HighContrast.Multiscale.respSkew A = (1 / 2) • (HCPolySupport.HighContrast.schurSkew A - HCPolySupport.matTranspose (HCPolySupport.HighContrast.schurSkew A))

noncomputable def HCPolySupport.HighContrast.Multiscale.respSym {d : ℕ} (A : BlockMat d) : Mat d

r_t = (K + K^t)/2, the symmetric half of K (p.response.transfer).

Equations

• HCPolySupport.HighContrast.Multiscale.respSym A = (1 / 2) • (HCPolySupport.HighContrast.schurSkew A + HCPolySupport.matTranspose (HCPolySupport.HighContrast.schurSkew A))

noncomputable def HCPolySupport.HighContrast.Multiscale.respBlockB {d : ℕ} (A : BlockMat d) : Mat d

b_t = S + (K+K^t) S_*^{-1} (K+K^t)/4 = S + r_t S_*^{-1} r_t (p.response.transfer). -- READING: S_*^{-1} is the lower-right block of A (schurSigmaStar A = A.lowerRight -- inverse).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respM {d : ℕ} (A : BlockMat d) : Mat d

m_t = b_t # S_*, the geometric mean of b_t and S_* (p.response.transfer).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respP {d : ℕ} (A : BlockMat d) (e : Vec d) : Vec d

The primal load p = m_t^{-1/2} e (p.response.transfer).

Equations

• HCPolySupport.HighContrast.Multiscale.respP A e = HCPolySupport.matVecMul (HCPolySupport.HighContrast.matSqrt (HCPolySupport.HighContrast.Multiscale.respM A)⁻¹) e

noncomputable def HCPolySupport.HighContrast.Multiscale.respQ {d : ℕ} (A : BlockMat d) (e : Vec d) : Vec d

The dual load q = m_t^{1/2} e (p.response.transfer).

Equations

• HCPolySupport.HighContrast.Multiscale.respQ A e = HCPolySupport.matVecMul (HCPolySupport.HighContrast.matSqrt (HCPolySupport.HighContrast.Multiscale.respM A)) e

Step 3, the pathwise and centred responses (p.response.transfer)

noncomputable def HCPolySupport.HighContrast.Multiscale.respJ {d : ℕ} (qq : Mat d) (u : ℤ) (p q' : Vec d) (b : CoeffField d) : ℝ

The pathwise response J(U, p, q'; b) of AK.HC (2.9), i.e. CoarseGraining's ResponseJ on the adapted cell (p.response.transfer). -- READING: the admissible class of the printed display is CoarseGraining's AHarmonicFunction b U, and the printed sup is ResponseJ; this is the identification already used by Annealed.responseJ_eq_coarseBlock_adapted.

Equations

• HCPolySupport.HighContrast.Multiscale.respJ qq u p q' b = HCPolySupport.ResponseJ (HCPolySupport.HighContrast.adaptedCell qq u) p q' b

noncomputable def HCPolySupport.HighContrast.Multiscale.blockResponseEnergy {d : ℕ} (A : BlockMat d) (p q' : Vec d) : ℝ

The block energy x. A x / 2 - p. q' with x = (-p, q'): the right-hand side of AK.HC (2.15) (p.response.transfer), i.e. the printed p.Sp/2 + (q'+Kp).S_*^{-1}(q'+Kp)/2 - p.q' in flattened coordinates. This is exactly the right-hand side of Annealed.responseJ_eq_coarseBlock_adapted.

Equations

• HCPolySupport.HighContrast.Multiscale.blockResponseEnergy A p q' = 1 / 2 * HCPolySupport.blockVecDot (-p, q') (HCPolySupport.blockMatVecMul A (-p, q')) - HCPolySupport.vecDot p q'

def HCPolySupport.HighContrast.Multiscale.blockResponseMean {d : ℕ} (A : BlockMat d) (x : BlockVec d) : BlockVec d

The mean identity AK.HC (2.32): Y = (I_{2d} + R A) x (e.response.energy.and.defect). Its two components are the printed gradient and flux means -p + S_*^{-1}(q'+Kp) and q' - K^t S_*^{-1}(q'+Kp) - Sp (p.response.transfer).

Equations

• HCPolySupport.HighContrast.Multiscale.blockResponseMean A x = x + HCPolySupport.blockMatVecMul (HCPolySupport.HighContrast.blockSwap d) (HCPolySupport.blockMatVecMul A x)

noncomputable def HCPolySupport.HighContrast.Multiscale.blockCenteredResponse {d : ℕ} (A : BlockMat d) (p q' : Vec d) : ℝ

The centred response Jtilde = E[J] - E[(grad v)_U]. E[(b grad v)_U] / 2 (p.response.transfer) evaluated through the block formulas. -- READING: the checkout has no annealed optimizer-average object, so the centring is written with the block means of AK.HC (2.32), which is the only form the printed proof ever uses (the two means are read off the block at p.response.transfer).

Equations

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

def HCPolySupport.HighContrast.Multiscale.blockCongr {d : ℕ} (G A : BlockMat d) : BlockMat d

Congruence G^t A G of doubled blocks (p.response.transfer).

Equations

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

def HCPolySupport.HighContrast.Multiscale.blockD (d : ℕ) : BlockMat d

D = diag(Id, -Id) (p.response.transfer).

Equations

• HCPolySupport.HighContrast.Multiscale.blockD d = { upperLeft := 1, upperRight := 0, lowerLeft := 0, lowerRight := -1 }

def HCPolySupport.HighContrast.Multiscale.blockAdjoint {d : ℕ} (A : BlockMat d) : BlockMat d

The adjoint block: replacing K by -K is congruence by D (p.response.transfer, "For the adjoint, replace K by -K").

Equations

• HCPolySupport.HighContrast.Multiscale.blockAdjoint A = HCPolySupport.HighContrast.Multiscale.blockCongr (HCPolySupport.HighContrast.Multiscale.blockD d) A

noncomputable def HCPolySupport.HighContrast.Multiscale.respCenteredJMinus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : ℝ

Jtilde^-(e), the centred response for (a; p, q - h_t p) (p.response.transfer).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respCenteredJPlus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : ℝ

Jtilde^+(e), the centred response for (a^t; p, q + h_t p) (p.response.transfer).

Equations

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

Step 4, the self-dual mean and the recentred data

(p.response.transfer)

noncomputable def HCPolySupport.HighContrast.Multiscale.canonicalMean {d : ℕ} (A : BlockMat d) : BlockMat d

The canonical mean M(F): the geometric mean of F and F# = R F^{-1} R, the unique positive solution of the Riccati equation M(F) F^{-1} M(F) = F# (p.response.transfer, Riccati).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respg {d : ℕ} (F : BlockMat d) : Mat d

The skew Schur coefficient g of M(F) (p.response.transfer).

Equations

• HCPolySupport.HighContrast.Multiscale.respg F = HCPolySupport.HighContrast.schurSkew (HCPolySupport.HighContrast.Multiscale.canonicalMean F)

noncomputable def HCPolySupport.HighContrast.Multiscale.respG {d : ℕ} (F : BlockMat d) : BlockMat d

G = ((Id, 0), (g, Id)) (p.response.transfer).

Equations

• HCPolySupport.HighContrast.Multiscale.respG F = { upperLeft := 1, upperRight := 0, lowerLeft := HCPolySupport.HighContrast.Multiscale.respg F, lowerRight := 1 }

noncomputable def HCPolySupport.HighContrast.Multiscale.respM0 {d : ℕ} (F : BlockMat d) : BlockMat d

M_0 = diag(m, m^{-1}) (p.response.transfer). -- READING: the paper's m is the canonical metric m(F): the Schur coefficients of M(F) are (m, m, g) by self-duality , and explicitCanonicalMetric F is by definition the inverse of the lower-right block of M(F), i.e. the Schur sigma_* of M(F).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.blockSqrt {d : ℕ} (A : BlockMat d) : BlockMat d

The positive square root M^{1/2} of a doubled block.

Equations

• HCPolySupport.HighContrast.Multiscale.blockSqrt A = HCPolySupport.ofFullBlockMat (HCPolySupport.HighContrast.matSqrt (HCPolySupport.toFullBlockMat A))

noncomputable def HCPolySupport.HighContrast.Multiscale.respEhatMinus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (u : ℤ) : BlockMat d

Ehat_u^- = G^t E_u G (p.response.transfer).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respEhatPlus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (u : ℤ) : BlockMat d

Ehat_u^+ = D Ehat_u^- D (p.response.transfer).

Equations

• HCPolySupport.HighContrast.Multiscale.respEhatPlus P jStar F u = HCPolySupport.HighContrast.Multiscale.blockAdjoint (HCPolySupport.HighContrast.Multiscale.respEhatMinus P jStar F u)

noncomputable def HCPolySupport.HighContrast.Multiscale.respCoeffMinus {d : ℕ} (F : BlockMat d) (a : CoeffSpace d) : CoeffField d

a_- = a - g (p.response.transfer).

Equations

• HCPolySupport.HighContrast.Multiscale.respCoeffMinus F a x = ↑↑a x - HCPolySupport.HighContrast.Multiscale.respg F

noncomputable def HCPolySupport.HighContrast.Multiscale.respCoeffPlus {d : ℕ} (F : BlockMat d) (a : CoeffSpace d) : CoeffField d

a_+ = a^t + g (p.response.transfer).

Equations

• HCPolySupport.HighContrast.Multiscale.respCoeffPlus F a x = HCPolySupport.matTranspose (↑↑a x) + HCPolySupport.HighContrast.Multiscale.respg F

noncomputable def HCPolySupport.HighContrast.Multiscale.respqMinus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : Vec d

q^- = q + (g - h_t)p (p.response.transfer).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respqPlus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : Vec d

q^+ = q + (h_t - g)p (p.response.transfer).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respxMinus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : BlockVec d

x^- = (-p, q^-) (p.response.transfer).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respxPlus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : BlockVec d

x^+ = (-p, q^+) (p.response.transfer).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respLsqMinus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : ℝ

(L^-)^2 = x^-. Ehat_t^- x^- (p.response.transfer).

Equations

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

theorem HCPolySupport.HighContrast.Multiscale.respLsqMinus_eq_quadratic {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : respLsqMinus P jStar F t e = blockVecDot (respxMinus P jStar F t e) (blockMatVecMul (respEhatMinus P jStar F t) (respxMinus P jStar F t e))

respLsqMinus is definitionally the quadratic form of respxMinus under respEhatMinus.

noncomputable def HCPolySupport.HighContrast.Multiscale.respLsqPlus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : ℝ

(L^+)^2 = x^+. Ehat_t^+ x^+ (p.response.transfer).

Equations

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

theorem HCPolySupport.HighContrast.Multiscale.respLsqPlus_eq_quadratic {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : respLsqPlus P jStar F t e = blockVecDot (respxPlus P jStar F t e) (blockMatVecMul (respEhatPlus P jStar F t) (respxPlus P jStar F t e))

respLsqPlus is definitionally the quadratic form of respxPlus under respEhatPlus.

noncomputable def HCPolySupport.HighContrast.Multiscale.respYMinus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : BlockVec d

Y^- = (I_{2d} + R Ehat_t^-) x^- (e.response.energy.and.defect).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respYPlus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : BlockVec d

Y^+ = (I_{2d} + R Ehat_t^+) x^+ (e.response.energy.and.defect).

Equations

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

Step 4, the annealed energies and the defect (p.response.transfer)

noncomputable def HCPolySupport.HighContrast.Multiscale.respEJMinus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : ℝ

E[J_t^-] = E[J(U_t, p, q^-; a_-)] (p.response.transfer).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respEJPlus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : ℝ

E[J_t^+] = E[J(U_t, p, q^+; a_+)] (p.response.transfer).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respTauMinus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) (e : Vec d) : ℝ

tau^- = E[J(U_s, p, q^-; a_-) - J_t^-] (e.response.energy.and.defect).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respTauPlus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) (e : Vec d) : ℝ

tau^+ = E[J(U_s, p, q^+; a_+) - J_t^+] (e.response.energy.and.defect).

Equations

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

Step 5, the grid sums and the weak seminorm (p.response.transfer)

def HCPolySupport.HighContrast.Multiscale.triadicIndexBox (d n : ℕ) : Finset (Fin d → ℤ)

The index set of the scale-(t-n) triadic subcells of the cube of generation t: the w in Z^d with |w i| <= (3^n-1)/2. -- READING: the printed sums run over z in 3^k q Z^d meeting U_t, with k = t - n; on the aligned grid these are exactly the 3^{nd} cells adaptedCellAtCenter q (t-n) w of the triadic partition of U_t, indexed by this box.

Equations

• HCPolySupport.HighContrast.Multiscale.triadicIndexBox d n = Fintype.piFinset fun (x : Fin d) => Finset.Icc (-↑((3 ^ n - 1) / 2)) ↑((3 ^ n - 1) / 2)

noncomputable def HCPolySupport.HighContrast.Multiscale.cellAverage {d : ℕ} (V : Set (Vec d)) (X : Vec d → BlockVec d) : BlockVec d

The cell average (X)_V of a doubled field.

Equations

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

def HCPolySupport.HighContrast.Multiscale.optimizerField {d : ℕ} {U : Set (Vec d)} (b : CoeffField d) (u : AHarmonicFunction b U) : Vec d → BlockVec d

The doubled optimizer field X = (grad v, b grad v) (e.response.energy.and.defect).

Equations

• HCPolySupport.HighContrast.Multiscale.optimizerField b u x = (u.toH1.grad x, HCPolySupport.matVecMul (b x) (u.toH1.grad x))

noncomputable def HCPolySupport.HighContrast.Multiscale.besovSeminorm {d : ℕ} (t : ℤ) (avg : ℕ → (Fin d → ℤ) → BlockVec d) : ℝ

The concrete scale-average seminorm of AK.HC (2.130) on the selected grid (p.response.transfer): sum_{k <= t} 3^{k/2} (avg_{z} |(Z)_{z+U_k}|^2)^{1/2}, with k = t - n. -- READING: avg n w is the cell average (Z)_{z+U_k} at the cell indexed by w at scale k = t - n; the inner bars are the Euclidean norm of the doubled vector.

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respWeakEnergy {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (qq : Mat d) (t : ℤ) (M0 : BlockMat d) (p q' : Vec d) (b : CoeffSpace d → CoeffField d) (Y : BlockVec d) : ℝ

W = 3^{-t} E[ [M_0^{1/2}(X_t - Y)]^2 ] (p.response.transfer). -- READING: the checkout exports IsResponseMaximizer as a predicate but no existence theorem producing a maximizer term, so W is the supremum of the weak energies over all families of maximizers of J(U_t, p, q'; b a); the junk value on an empty family is 0. Every printed use of W is an upper bound on it, so the supremum is the conservative reading.

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respWMinus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : ℝ

W^- (p.response.transfer).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respWPlus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : ℝ

W^+ (p.response.transfer).

Equations

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

theorem HCPolySupport.HighContrast.Multiscale.respWPlus_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (e : Vec d) : respWPlus P jStar F t e = respWeakEnergy P (respGrid jStar F) t (respM0 F) (respP (respMean P jStar F t) e) (respqPlus P jStar F t e) (respCoeffPlus F) (respYPlus P jStar F t e)

W^+ is the weak energy of the recentred coefficient a_+ = a^t + g at the load q^+: by definition W^+ = W(U_t, p, q^+; a_+, Y^+) for the weak response energy W.

noncomputable def HCPolySupport.HighContrast.Multiscale.blockSpecBound {d : ℕ} (Hb : BlockMat d) : ℝ

The norm of the spectral positive part of a symmetric doubled block: the least c >= 0 with H <= c I_{2d} (p.response.transfer, "the subscript + denotes the spectral positive part").

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respAllScaleMax {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (jStar : ℕ) (F : BlockMat d) (t : ℤ) (a : CoeffSpace d) : ℝ

The all-scale maximum M = sup_{k <= t} 3^{-rho(t-k)} max_z |(E_t^{-1/2} A_k(z) E_t^{-1/2} - I_{2d})_+| (p.response.transfer), pathwise in the sample a.

Equations

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

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

The two-sided all-scale maximum A = sup_{k <= t} 3^{-rho(t-k)} |E_t^{-1/2} A_k(z) E_t^{-1/2} - I_{2d}|, pathwise in the sample a: exactly respAllScaleMax with the spectral positive part blockSpecBound replaced by the full operator norm blockOpNorm (HCPoly/Entry/Setup/ProjectiveDistance.lean). It dominates respAllScaleMax termwise, since blockSpecBound N <= blockOpNorm N always.

Equations

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

Step 6, the source load and the cutoff class (p.response.transfer)

noncomputable def HCPolySupport.HighContrast.Multiscale.annealedBlockOf {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (V : Set (Vec d)) (b : CoeffSpace d → CoeffField d) : BlockMat d

The annealed block E[A(V; b)] of a field family b that need not be a member of the coefficient carrier (the recentred fields a_-, a_+); entrywise, as annealedBlock.

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respSourceLoad {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s : ℤ) (b : CoeffSpace d → CoeffField d) (Y : BlockVec d) : ℝ

L_s = sum_{k <= s} 3^{3(k-s)/2} avg_z (|b_{k,z}^{1/2} P| + |(S_{*,k,z})^{-1/2} Q|)^2 (p.response.transfer), with b_{k,z} and (S_{*,k,z})^{-1} the two diagonal blocks of E[A(z+U_k; b)] and (P, Q) = Y. -- READING: |b^{1/2}P|^2 = P.bP and |(S_*)^{-1/2}Q|^2 = Q.S_*^{-1}Q, and S_*^{-1} is the lower-right block, as in schurSigmaStar.

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respLsMinus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) (e : Vec d) : ℝ

L_s^- (p.response.transfer).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.respLsPlus {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (jStar : ℕ) (F : BlockMat d) (s t : ℤ) (e : Vec d) : ℝ

L_s^+ (p.response.transfer).

Equations

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

noncomputable def HCPolySupport.HighContrast.Multiscale.responseCutoffProfileConst : ℝ

The universal profile constant of the smooth cutoff construction: max 1 (max θ' θ'') for the fixed one-dimensional transition profile HCPolySupport.smoothTransitionProfile (Real.smoothTransition) used by CoarseGraining's QuantitativeCubeCutoff.canonicalFun. It is a single real number ≥ 1 depending on NOTHING -- not on d, not on t, not on the grid -- so every constant built with it below is still a dimensional constant in the sense of the manuscript.

It is carried explicitly because the pinned package supplies only NONCOMPUTABLE compactness bounds for the derivatives of Real.smoothTransition (Sobolev/Foundations/Cutoff/Profile.lean, both Classical.choose of an existence statement), so no numeral bounds them; and the cutoff constants carry exactly this factor (1024 * d ^ 4 * (max 1 (max derivBound secondDerivBound)) ^ 2 * 3 ^ (-2 * t)).

Equations

• HCPolySupport.HighContrast.Multiscale.responseCutoffProfileConst = max 1 (max HCPolySupport.smoothTransitionProfile.derivBound HCPolySupport.smoothTransitionProfile.secondDerivBound)

theorem HCPolySupport.HighContrast.Multiscale.one_le_responseCutoffProfileConst : 1 ≤ responseCutoffProfileConst

responseCutoffProfileConst is at least 1, immediate from its definition as a max with 1.

theorem HCPolySupport.HighContrast.Multiscale.responseCutoffProfileConst_pos : 0 < responseCutoffProfileConst

responseCutoffProfileConst is strictly positive, since it is at least 1.

def HCPolySupport.HighContrast.Multiscale.IsResponseCutoff {d : ℕ} (qq : Mat d) (t : ℤ) (φ : Vec d → ℝ) : Prop

The cutoff class of p.response.transfer: a cutoff phi in U_t with 0 <= phi <= 2, mean one on U_t, and derivatives at the scale 3^t in q-coordinates. -- READING: "smooth, with derivatives at the scale 3^t in q-coordinates" is rendered as: the pullback y -> phi (q y) is Lipschitz with constant C(d) * 3^{-t}, C(d) = 32 d^2. Only this quantitative form is used in the cutoff estimate.

The Lipschitz constant carries the dimensional factor 3 ^ (-t): without it the class is empty, since every point of a cube of side 3^t lies at sup-distance at most 3^t/2 from the complement, so a 3^{-t}-Lipschitz function vanishing off the cube is at most 1/2 everywhere and cannot have mean one. The class is inhabited -- exists_isResponseCutoff constructs a member.

The coefficient 32 * d ^ 2 * 3 ^ (-t) is the explicit dimensional constant of the smooth cutoff construction. The pullback gradient of the normalized canonical product cutoff is bounded by 32 * d ^ 2 * smoothTransitionProfile.derivBound * 3 ^ (-t) -- reciprocal collar width 16 * d * 3 ^ (-t), doubled by the normalization A⁻¹ ≤ 2 -- and that is precisely the coefficient used in the cutoff estimates. Taking the one-dimensional transition profile piecewise linear, i.e. derivBound = 1, turns that coefficient into the numeral 32 * d ^ 2 used here; the witness built in exists_isResponseCutoff is such a piecewise-linear cutoff and in fact achieves 8 * d * 3 ^ (-t).

The cutoff estimate abs_cutoffProductTermOnCube_le_scaledWeakNormProduct consumes smoothness and a second-derivative scale, so the class carries four further conjuncts beyond the first five (the first five keep their names, their order and their meaning, so every existing projection hphi.1, hphi.2.1,... is unchanged):

• ContDiff R (top : N-infty) phi -- the paper's "SMOOTH cutoff", p.response.transfer;
• HasCompactSupport phi;
• tsupport phi subseteq HighContrast.adaptedCell qq t -- the adapted-geometry form of tsupport phi subseteq openCubeSet Q, sharpening the pointwise vanishing conjunct to vanishing on a neighbourhood of the complement (HighContrast.adaptedCell qq t is open);
• the second-derivative bound in q-coordinates, forall x, ‖iteratedFDeriv R 2 (phi o q) x‖ <= 1024 * d ^ 4 * Theta ^ 2 * 3 ^ (-2 * t), the second-order coefficient of the smooth cutoff construction.

The two second-block coefficients are not the flat numerals 32 * d ^ 2 and 1024 * d ^ 4 (their values at derivBound = secondDerivBound = 1): those numerals are not attainable by any smooth cutoff reachable from the pinned package. The coefficients carried by the smooth construction are 32 * d ^ 2 * derivBound * 3 ^ (-t) and 1024 * d ^ 4 * (max 1 (max derivBound secondDerivBound)) ^ 2 * 3 ^ (-2 * t), whose profile factors equal 1 only for the piecewise-linear profile, which is not C^infinity; and the pinned package's smooth profile HCPolySupport.smoothTransitionProfile carries only the noncomputable compactness bounds smoothTransitionProfile.derivBound/secondDerivBound (.lake/packages/CoarseGraining/HCPolySupport/Sobolev/Foundations/Cutoff/Profile.lean, each Classical.choose of a bare existence statement), which no numeral bounds. Both coefficients therefore carry the universal factor Theta = responseCutoffProfileConst >= 1 above. Since Theta >= 1 this only widens the class, so the estimates that consume membership are strengthened, exists_isResponseCutoff (which produces membership) still discharges the paper's choice, and response_cutoff_estimate is unaffected.

Equations

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