High-contrast homogenization: Setup.TransportObjects

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

Carriers for the transport across a change of adapted geometry

The objects the geometry-and-transport section adds to the fixed-grid layer: the canonical block geometry A # B, M(E), m(E), 𝔡(E); the determinant account Ξ(E), Ξ_j^q, σ_q(u,v); the gap function 𝔤_Q; the matrix positive part; the bridge congruence S and its Gram matrix SᵗS; the transport and bridge source coefficients and their remainders; the constant-speed projective path and the hop it selects; and the six continuous error functions of the short test.

Three conventions carry over from the fixed-grid layer and are used again here. Scalar sizes are Loewner, so the operator norm of a doubled block is its size against the identity and no norm symbol enters a scalar quantity. Every quantity whose finiteness is asserted is extended-real valued. The reference text's positive part of a symmetric matrix is its spectral positive part; on the two matrix-valued occurrences that is the continuous functional calculus of x ↦ max x 0, and on the eight scalar occurrences it is the excess already carried by the fixed-grid layer.

The canonical metric and the canonical shear are the characterized factors of the canonical block, taken from the block geometry layer through the flattening map; nothing here re-derives them, and nothing here depends on how they are produced beyond the characterization that layer proves.

The canonical block geometry

noncomputable def HCPolySupport.HighContrast.canonicalBlock {d : ℕ} (E : BlockMat d) : BlockMat d

The canonical block M(E) = E # E^♯ (e.scale.selection.canonical.metric), read on a doubled block through the flattening map.

Equations

• HCPolySupport.HighContrast.canonicalBlock E = HCPolySupport.ofFullBlockMat (HCPolySupport.HighContrast.canonBlock (HCPolySupport.toFullBlockMat E))

noncomputable def HCPolySupport.HighContrast.canonicalMetric {d : ℕ} (E : BlockMat d) : Mat d

The canonical metric m(E) (the symmetric and skew factors of the canonical block), the positive factor of the unique factorization M(E) = G_{-g(E)}^t diag(m(E), m(E)^{-1}) G_{-g(E)}.

Equations

• HCPolySupport.HighContrast.canonicalMetric E = HCPolySupport.HighContrast.canonMetric (HCPolySupport.toFullBlockMat E)

noncomputable def HCPolySupport.HighContrast.canonicalShear {d : ℕ} (E : BlockMat d) : Mat d

The canonical shear g(E) (the symmetric and skew factors of the canonical block), the skew factor of the same factorization.

Equations

• HCPolySupport.HighContrast.canonicalShear E = HCPolySupport.HighContrast.canonShear (HCPolySupport.toFullBlockMat E)

noncomputable def HCPolySupport.HighContrast.blockImbalance {d : ℕ} (E : BlockMat d) : ℝ

The imbalance 𝔡(E) = |M(E)^{-1/2} E M(E)^{-1/2}|² (e.scale.selection.canonical.metric).

Equations

• HCPolySupport.HighContrast.blockImbalance E = HCPolySupport.HighContrast.canonImbalance (HCPolySupport.toFullBlockMat E)

The determinant account

noncomputable def HCPolySupport.HighContrast.detRoot (d : ℕ) (E : BlockMat d) : ℝ

The determinant root Ξ(E) = det(E)^{1/d} of a doubled block, the d-th root of the determinant of a 2d-by-2d matrix (e.scale.selection.logdet.loss).

Equations

• HCPolySupport.HighContrast.detRoot d E = Matrix.det (HCPolySupport.toFullBlockMat E) ^ (↑d)⁻¹

noncomputable def HCPolySupport.HighContrast.adaptedDetRoot {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (j : ℤ) : ℝ

The determinant root Ξ_j^q = Ξ(E_j^q) of an annealed adapted block.

Equations

• HCPolySupport.HighContrast.adaptedDetRoot P q j = HCPolySupport.HighContrast.detRoot d (HCPolySupport.HighContrast.adaptedMean P q j)

noncomputable def HCPolySupport.HighContrast.detLoss {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (u v : ℤ) : ℝ

The determinant loss σ_q(u,v) = log Ξ_u^q - log Ξ_v^q (e.scale.selection.logdet.loss).

Equations

• HCPolySupport.HighContrast.detLoss P q u v = Real.log (HCPolySupport.HighContrast.adaptedDetRoot P q u) - Real.log (HCPolySupport.HighContrast.adaptedDetRoot P q v)

The gap function and the matrix positive part

noncomputable def HCPolySupport.HighContrast.blockOpSize {d : ℕ} (H : BlockMat d) : ℝ

The operator size ‖H‖_op of a doubled block, in the Loewner form of the fixed-grid layer: the least t ≥ 0 with -tI ≤ H ≤ tI.

Equations

• HCPolySupport.HighContrast.blockOpSize H = HCPolySupport.HighContrast.blockSize H (HCPolySupport.Book.Ch02.blockIdentity d)

noncomputable def HCPolySupport.HighContrast.gapG {d : ℕ} (Q : ℝ) (Pm : BlockMat d) : ℝ

The gap function 𝔤_Q(P) = ‖P‖_op^{Q-1} tr(P - I) + (tr(P - I))^Q, for P ≥ I (the gap functional of the positive-gap estimate).

Equations

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

noncomputable def HCPolySupport.HighContrast.blockPosPart {d : ℕ} (H : BlockMat d) : BlockMat d

The matrix positive part (H)_+ of a symmetric doubled block: its spectral positive part, the continuous functional calculus of x ↦ max x 0. This is the matrix-valued reading of the reference text's positive part, used at the two sites where the positive part is a matrix rather than a number.

Equations

• HCPolySupport.HighContrast.blockPosPart H = HCPolySupport.ofFullBlockMat (cfc (fun (x : ℝ) => max x 0) (HCPolySupport.toFullBlockMat H))

The bridge congruence

noncomputable def HCPolySupport.HighContrast.bridgeMap {d : ℕ} (H F : BlockMat d) : FullBlockMat d

The bridge congruence S = H^{1/2} F^{-1/2} of the near-isometric comparison (p.two.grid.transport, at the bridge data).

Equations

• HCPolySupport.HighContrast.bridgeMap H F = HCPolySupport.HighContrast.matSqrt (HCPolySupport.toFullBlockMat H) * HCPolySupport.HighContrast.matSqrt (HCPolySupport.toFullBlockMat F)⁻¹

noncomputable def HCPolySupport.HighContrast.bridgeGram {d : ℕ} (H F : BlockMat d) : BlockMat d

The Gram matrix SᵗS of the bridge congruence.

Equations

• HCPolySupport.HighContrast.bridgeGram H F = HCPolySupport.ofFullBlockMat (Matrix.transpose (HCPolySupport.HighContrast.bridgeMap H F) * HCPolySupport.HighContrast.bridgeMap H F)

The transport source coefficients

noncomputable def HCPolySupport.HighContrast.transportContCoeff {d : ℕ} (Cd g : ℝ) (E : BlockMat d) (jStar : ℤ) (mu mu' : Mat d) : ℝ

The continued transport coefficient 𝖣_cont^{tr,S}(q,q') = C_d K(q,q') κ_𝐄 B_q B_{q'} χ_g 𝒰², with 𝒰 = 2 (the source coefficients of the transport estimate).

Equations

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

noncomputable def HCPolySupport.HighContrast.transportEarlyCoeff {d : ℕ} (Cd g : ℝ) (E : BlockMat d) (mu' : Mat d) : ℝ

The early transport coefficient 𝖣_early^{tr,S}(q') = C_d κ_𝐄 B_{q'}² 𝒰², with 𝒰 = 2 (the source coefficients of the transport estimate).

Equations

• HCPolySupport.HighContrast.transportEarlyCoeff Cd g E mu' = Cd * HCPolySupport.HighContrast.kappaRef E * HCPolySupport.HighContrast.boundaryConst Cd g mu' ^ 2 * 4

noncomputable def HCPolySupport.HighContrast.transportSrcCoeff {d : ℕ} (Cd g : ℝ) (E : BlockMat d) (jStar : ℤ) (mu mu' : Mat d) : ℝ

The total transport source coefficient 𝖣_src^{tr,S} = 1 + 𝖣_cont^{tr,S} + 𝖣_early^{tr,S} (the source coefficients of the transport estimate).

Equations

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

noncomputable def HCPolySupport.HighContrast.transportSrcRemainder {d : ℕ} (Cd g Q a : ℝ) (E : BlockMat d) (jStar : ℤ) (mu mu' : Mat d) (n : ℤ) : ℝ

The transported source majorant 𝓡_src^{tr,S}(q,q';n,j_*) = (𝖣_src^{tr,S} + (𝖣_src^{tr,S})^Q)3^{-a(n-j_*)} (the transported source majorant).

Equations

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

The bridge source coefficients

noncomputable def HCPolySupport.HighContrast.bridgeContCoeff {d : ℕ} (Cd g : ℝ) (E : BlockMat d) (jStar : ℤ) (mp mv mr : Mat d) : ℝ

The continued bridge coefficient 𝖣_cont^S(p,v;r) = C_d K(p,v) κ_𝐄 B_p B_r χ_g 𝒰², with 𝒰 = 2 (the source coefficients in the two-grid comparison).

Equations

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

noncomputable def HCPolySupport.HighContrast.bridgeEarlyCoeff {d : ℕ} (Cd g : ℝ) (E : BlockMat d) (mv mr : Mat d) : ℝ

The early bridge coefficient 𝖣_early^S(v;r) = C_d κ_𝐄 B_v B_r 𝒰², with 𝒰 = 2 (the source coefficients in the two-grid comparison).

Equations

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

noncomputable def HCPolySupport.HighContrast.bridgeSrcCoeff {d : ℕ} (Cd g : ℝ) (E : BlockMat d) (jStar : ℤ) (mq mq' : Mat d) : ℝ

The total bridge source coefficient 𝖣_src^{br,S}(q,q'): one plus the maximum of 𝖣_cont^S(p,v;r) + 𝖣_early^S(v;r) over the two ordered pairs (p,v) and the two terminal grids r (the source coefficients in the two-grid comparison).

Equations

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

noncomputable def HCPolySupport.HighContrast.bridgeCmpRemainder {d : ℕ} (C Cd g rhoDr : ℝ) (E : BlockMat d) (jStar : ℤ) (mq mq' : Mat d) (v : ℤ) : ℝ

The comparison remainder 𝓡_cmp^S(q,q';v) = C 𝖣_src^{br,S}(q,q')(1 + v - j_*)3^{-ρ_dr(v-j_*)} (the source remainder in the two-grid comparison).

Equations

• HCPolySupport.HighContrast.bridgeCmpRemainder C Cd g rhoDr E jStar mq mq' v = C * HCPolySupport.HighContrast.bridgeSrcCoeff Cd g E jStar mq mq' * (1 + (↑v - ↑jStar)) * 3 ^ (-rhoDr * (↑v - ↑jStar))

noncomputable def HCPolySupport.HighContrast.bridgeShiftedRemainder {d : ℕ} (C Cd g rhoDr : ℝ) (E : BlockMat d) (jStar : ℤ) (mq mq' : Mat d) (n l : ℤ) : ℝ

The shifted remainder 𝓡_sh^S(q,q';n,ℓ) = C 𝖣_src^{br,S}(q,q')3^{ρ_dr ℓ}(1 + n - j_*)3^{-ρ_dr(n-j_*)} (e.two.grid.drift.source.convolution).

Equations

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

The two-grid comparison errors

noncomputable def HCPolySupport.HighContrast.bridgeErrUpper {d : ℕ} (C Cd g rhoDr K : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (jStar : ℤ) (mq mq' : Mat d) (n l : ℤ) : ℝ

The upper comparison error ε_+^S(n,ℓ) = CK(3^{-ℓ} + 3^{-(1-ρ_dr)ℓ}D_{q,j_*}(n)) + 𝓡_cmp^S(q,q';n) (e.successful.short.preliminary.comparison).

Equations

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

noncomputable def HCPolySupport.HighContrast.bridgeErrLower {d : ℕ} (C Cd g rhoDr K : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (jStar : ℤ) (mq mq' : Mat d) (n l : ℤ) : ℝ

The lower comparison error `ε_-^S(n,ℓ) = CK(1-CK3^{-ℓ})^{-1}(3^{-ℓ} + 3^{-(1-ρ_dr)ℓ}D_{q,j_*}(n+ℓ))

• 𝓡_cmp^S(q',q;n+ℓ) (e.successful.short.preliminary.comparison`).

Equations

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

The constant-speed projective path and the hop it selects

noncomputable def HCPolySupport.HighContrast.matPow {d : ℕ} (theta : ℝ) (A : Mat d) : Mat d

The real power A^θ of a positive matrix, by the continuous functional calculus.

Equations

• HCPolySupport.HighContrast.matPow theta A = cfc (fun (x : ℝ) => x ^ theta) A

noncomputable def HCPolySupport.HighContrast.projPath {d : ℕ} (m0 m1 : Mat d) (theta : ℝ) : Mat d

The constant-speed projective path m(θ) = m₀^{1/2}(m₀^{-1/2}m₁m₀^{-1/2})^θ m₀^{1/2} (e.renormalization.geometry.update).

Equations

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

noncomputable def HCPolySupport.HighContrast.projPathStep {d : ℕ} (c : ℝ) (m0 m1 : Mat d) : Mat d

The next point on the fixed constant-speed path from m₀ to m₁ at projective distance at most c: the path point at parameter min{c/d_pr([m₀],[m₁]), 1}, and the endpoint m₁ when the two projective classes agree (p.successful.short.bridge, at the candidate construction).

Equations

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

The six continuous error functions of the short test

noncomputable def HCPolySupport.HighContrast.shortDriftNew (d : ℕ) (rhoDr : ℝ) (l0 : ℤ) (b delta : ℝ) : ℝ

d_n(b,δ) = (1+δ)^d 3^{-ρ_dr ℓ₀} b + 2d((1+δ)^d - 1), the new-scale drift envelope of the short test (p.successful.short.bridge, first of the six error functions).

Equations

• HCPolySupport.HighContrast.shortDriftNew d rhoDr l0 b delta = (1 + delta) ^ d * 3 ^ (-rhoDr * ↑l0) * b + 2 * ↑d * ((1 + delta) ^ d - 1)

noncomputable def HCPolySupport.HighContrast.shortDriftTerm (d : ℕ) (rhoDr : ℝ) (l0 : ℤ) (b delta : ℝ) : ℝ

d_t(b,δ) = (1+δ)^d 3^{-2ρ_dr ℓ₀} b + 2d((1+δ)^d - 1), the terminal-scale drift envelope of the short test (second of the six).

Equations

• HCPolySupport.HighContrast.shortDriftTerm d rhoDr l0 b delta = (1 + delta) ^ d * 3 ^ (-2 * rhoDr * ↑l0) * b + 2 * ↑d * ((1 + delta) ^ d - 1)

noncomputable def HCPolySupport.HighContrast.shortErrUpper (d : ℕ) (C Khop rhoDr : ℝ) (l0 : ℤ) (b delta R1 : ℝ) : ℝ

e_+(b,δ,R₁) = CK_hop(3^{-ℓ₀} + 3^{-(1-ρ_dr)ℓ₀}d_n(b,δ)) + R₁, the upper comparison envelope of the short test (third of the six).

Equations

• HCPolySupport.HighContrast.shortErrUpper d C Khop rhoDr l0 b delta R1 = C * Khop * (3 ^ (-↑l0) + 3 ^ (-(1 - rhoDr) * ↑l0) * HCPolySupport.HighContrast.shortDriftNew d rhoDr l0 b delta) + R1

noncomputable def HCPolySupport.HighContrast.shortErrLower (d : ℕ) (C Khop rhoDr : ℝ) (l0 : ℤ) (b delta R2 : ℝ) : ℝ

`e_-(b,δ,R₂) = CK_hop(1 - CK_hop3^{-ℓ₀})^{-1}(3^{-ℓ₀}

• 3^{-(1-ρ_dr)ℓ₀}d_t(b,δ)) + R₂`, the lower comparison envelope of the short test (fourth of the six).

Equations

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

noncomputable def HCPolySupport.HighContrast.shortBridgeErr (d : ℕ) (C Khop rhoDr : ℝ) (l0 : ℤ) (b delta R1 R2 : ℝ) : ℝ

η_br(b,δ,R₁,R₂) = max{e_-(b,δ,R₂), (1 + e_+(b,δ,R₁))(1+δ)^d - 1}, the bridge-error envelope of the short test (fifth of the six).

Equations

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

noncomputable def HCPolySupport.HighContrast.shortNewDrift (d : ℕ) (C Khop rhoDr : ℝ) (l0 : ℤ) (b delta R2 R3 : ℝ) : ℝ

`𝔡_new(b,δ,R₂,R₃) = C(e_-(b,δ,R₂) + K_hop3^{-ℓ₀}

• (1+K_hop)3^{2ρ_dr ℓ₀}d_t(b,δ) + R₃)`, the new-grid drift envelope of the short test (sixth of the six). The reference text displays this envelope with a further argument that its body never reads; the display is a typo for the four-argument form written here, and the source correction is recorded.

Equations

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