High-contrast homogenization: Provider.Persistence.TransferGauge

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

The transfer gauge, the comparison sizes, and the two decay gaps

The comparison between adapted and Euclidean cubes measures its error in units of the reference block, with the source gauge Γ_{g,S}(j) = (1-g)^{-1}(1 + K_{Ψ_S}^2 3^{-j})^g as the coefficient. This file collects the scalar account that turns such an error into a tolerance on the entry mean.

Three facts about the gauge come first. Above the alignment scale the burn e.source.lower.scale has already paid for the growth witness: its second term puts 3^{j_*} above K_bar_S^2 ≥ K_{Ψ_S}^2, so K_{Ψ_S}^23^{-j} never exceeds one there. The gauge is therefore below 2^g/(1-g) from the alignment on, and it is antitone in the scale on every branch.

The two transfer sizes come next. The actual size 𝒯_{q,S}(j) = C_AE 𝔢_q Γ_{g,S}(j) Λ_t carries the random normalization Λ_t = |(E_t^q)^{-1/2}𝐄(E_t^q)^{-1/2}|; the deterministic size 𝒯_bar_{q,S}(j) replaces it by U κ_𝐄 B_q. The terminal normalization e.two.grid.source.normalization bounds the first by the second, which is the envelope for the transfer size: only the constant U, never the multiplier, survives.

Last is the gap arithmetic. Each gap is the ceiling of a truncated logarithm, so it is at least one — which makes both adapter chains strict — and it always dominates the untruncated logarithm, which is what the forward and the reverse comparison error need. The degenerate branch where the comparison size is nonpositive is trivial, so no positivity of the size is assumed anywhere.

The source gauge

theorem HCPolySupport.HighContrast.Persistence.zero_lt_transferGauge {g : ℝ} (hg : g < 1) (K : ℝ) (j : ℤ) : 0 < transferGauge g K j

The source gauge is positive below the critical exponent: its base exceeds one and its prefactor is the reciprocal of a positive number.

theorem HCPolySupport.HighContrast.Persistence.sq_mul_zpow_le_one {d : ℕ} {Q K : ℝ} {jStar M j : ℤ} (hK : 1 < K) (hw : IsCoupledWindow d Q K jStar M) (hj : jStar ≤ j) : K ^ 2 * 3 ^ (-j) ≤ 1

The growth witness is burned above the alignment scale. The second term of the maximum defining the source burn e.source.lower.scale puts 3^{j_*} above K_bar_S^2, the enlarged witness dominates the witness, and 3^{-j} decreases.

theorem HCPolySupport.HighContrast.Persistence.transferGauge_le {d : ℕ} {Q K g : ℝ} {jStar M j : ℤ} (hg0 : 0 ≤ g) (hg1 : g < 1) (hK : 1 < K) (hw : IsCoupledWindow d Q K jStar M) (hj : jStar ≤ j) : transferGauge g K j ≤ 2 ^ g / (1 - g)

The gauge is bounded above the alignment scale, from the source burn e.source.lower.scale.

The size envelope

The two decay gaps

theorem HCPolySupport.HighContrast.Persistence.one_le_gapCeil (x : ℝ) : 1 ≤ ⌈max 1 (max 0 x)⌉

Each gap is at least one, on every branch of its truncated logarithm; this is what makes both adapter chains strict.

theorem HCPolySupport.HighContrast.Persistence.logb_le_gapCeil (x : ℝ) : Real.logb 3 x ≤ ↑⌈max 1 (max 0 (Real.logb 3 x))⌉

Each gap dominates the untruncated logarithm it is built from.

theorem HCPolySupport.HighContrast.Persistence.mul_zpow_neg_le_of_logb_le {T eta : ℝ} (heta : 0 < eta) {l : ℤ} (hl : Real.logb 3 (T / eta) ≤ ↑l) : T * 3 ^ (-l) ≤ eta

The decay gap defeats the comparison size. If the gap exponent dominates log_3(T/η), then T·3^{-gap} ≤ η. The degenerate branch T ≤ 0, where the logarithm is at its junk value, is trivial, so no positivity of T is needed.

theorem HCPolySupport.HighContrast.Persistence.transferSizeBar_mul_zpow_le {d : ℕ} {U CAE Cd g K eta : ℝ} {E : BlockMat d} {m0 : Mat d} {j l : ℤ} (heta : 0 < eta) (hl : l = ⌈max 1 (max 0 (Real.logb 3 (transferSizeBar U CAE Cd g K E m0 j / eta)))⌉) : transferSizeBar U CAE Cd g K E m0 j * 3 ^ (-l) ≤ eta

The gap inequality at the printed gap of e.response.transfer.gaps, for the forward and for the reverse gap: the deterministic comparison size, discounted by the gap it defines, is below the tolerance that defines it.

theorem HCPolySupport.HighContrast.Persistence.rpow_neg_sub_eq_zpow {t m l : ℤ} (h : m = t + l) : 3 ^ (-(↑m - ↑t)) = 3 ^ (-l)

The adapter's error exponent, read on a chain whose two ends differ by the gap, is the gap discount.