High-contrast homogenization: Provider.Transport.WindowBelowStart

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

The below-start quantity

The last clause of e.source.adapted.bound that a bounded-window estimate reads is the below-start source maximum \mathsf S_{t,<j_*}(F): the supremum, over the scales strictly below the alignment and over an arbitrary family of centers at each such scale, of the F-normalized excess of the adapted response, weighted by 3^{-\rho(t-k)}. It obeys a pathwise bound, and the three consequences drawn from that bound are its first moment, its L^Q norm and its source-tail form.

Everything follows from one weighted cell bound and the fact that the multiplier is common to every cell of every family. On a cell of scale k < j_* the burn discount is 3^{g(j_*-k)}, and the weight 3^{-\rho(t-k)} absorbs it completely when \rho > g:

3^{-\rho(t-k)}3^{g(j_*-k)} = 3^{-\rho(t-j_*)}3^{-(\rho-g)(j_*-k)} \leq 3^{-\rho(t-j_*)},

so no multiplicity in the scale, and none in the centers either, since the same Y_P serves them all on one event of full measure. The excess is below the scalar size, a change of reference block costs Λ(F;𝐄), and the cell bound of the window supplies the rest. The three consequences are then the expectation, the L^Q norm and the decomposition Y_P = 1 + (Y_P - 1) applied to a single pathwise majorant proportional to Y_P.

The countability of the center families, which the printed statement assumes, is not used: the bound holds term by term, so the supremum inherits it whatever the index set.

The two elementary steps

theorem HCPolySupport.HighContrast.Transport.blockExcess_le_blockSize {d : ℕ} {H F : BlockMat d} (hH : IsSymmetricBlockMat H) (hHps : Matrix.PosSemidef (toFullBlockMat H)) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) : blockExcess H F ≤ blockSize H F

The size of the positive part of the normalized excess is below the scalar size of the same pair: both are read off one relative size, and the excess subtracts one from it before truncating at zero.

theorem HCPolySupport.HighContrast.Transport.rpow_mul_burnDiscount_le {g rho : ℝ} (hrho : g < rho) {jStar k : ℤ} (hk : k < jStar) (t : ℤ) : 3 ^ (-rho * (↑t - ↑k)) * burnDiscount g jStar k ≤ 3 ^ (-rho * (↑t - ↑jStar))

The weight absorbs the burn discount. Below the alignment scale the discount is 3^{g(j_*-k)}, and the weight 3^{-\rho(t-k)} beats it by 3^{-(\rho-g)(j_*-k)} \leq 1 exactly because \rho > g.

The pathwise bound

theorem HCPolySupport.HighContrast.Transport.ae_belowStartSup_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K Cd : ℝ} {jStar M : ℤ} {Y : CoeffSpace d → ℝ} (hCd : 0 ≤ Cd) (hg : g < 1) (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hY : IsWindowMultiplier P g E Ψ K Cd jStar M Y) {nu : Mat d} (hnu : Matrix.PosDef nu) (hq : IsRoundedGrid jStar (roundedGrid jStar nu)) {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {rho : ℝ} (hrho : g < rho) (t : ℤ) {Z : ℤ → Set (Vec d)} (hZ : ∀ k < jStar, ∀ z ∈ Z k, adaptedCellTranslate (roundedGrid jStar nu) k z ⊆ centeredCube d M) : ∀ᵐ (a : CoeffSpace d) ∂P, belowStartSup rho (roundedGrid jStar nu) jStar t Z F a ≤ ENNReal.ofReal (boundaryConst Cd g nu * Y a * blockSize E F * 3 ^ (-rho * (↑t - ↑jStar)))

The below-start quantity, pathwise: one event of full measure carries the bound for every scale below the alignment and every center of every family.

The three consequences

theorem HCPolySupport.HighContrast.Transport.eLpNorm_belowStartSup_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K Cd : ℝ} {jStar M : ℤ} {Y : CoeffSpace d → ℝ} (hCd : 0 ≤ Cd) (hg : g < 1) (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hY : IsWindowMultiplier P g E Ψ K Cd jStar M Y) {nu : Mat d} (hnu : Matrix.PosDef nu) (hq : IsRoundedGrid jStar (roundedGrid jStar nu)) {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {rho : ℝ} (hrho : g < rho) (t : ℤ) {Z : ℤ → Set (Vec d)} (hZ : ∀ k < jStar, ∀ z ∈ Z k, adaptedCellTranslate (roundedGrid jStar nu) k z ⊆ centeredCube d M) (Q : ℝ) (hS : MeasureTheory.AEStronglyMeasurable (belowStartSup rho (roundedGrid jStar nu) jStar t Z F) P) : MeasureTheory.eLpNorm (belowStartSup rho (roundedGrid jStar nu) jStar t Z F) (ENNReal.ofReal Q) P ≤ ENNReal.ofReal (boundaryConst Cd g nu * blockSize E F * 3 ^ (-rho * (↑t - ↑jStar))) * lqNorm P Q Y

The L^Q norm of the below-start source maximum. The supremum is assumed a.e. strongly measurable, since it runs over an arbitrary family of centers.

theorem HCPolySupport.HighContrast.Transport.isShiftedBigOWithTop_belowStartSup {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K Cd : ℝ} {jStar M : ℤ} {Y : CoeffSpace d → ℝ} (hCd : 0 ≤ Cd) (hg : g < 1) (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hY : IsWindowMultiplier P g E Ψ K Cd jStar M Y) {nu : Mat d} (hnu : Matrix.PosDef nu) (hq : IsRoundedGrid jStar (roundedGrid jStar nu)) {F : BlockMat d} (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {rho : ℝ} (hrho : g < rho) (t : ℤ) {Z : ℤ → Set (Vec d)} (hZ : ∀ k < jStar, ∀ z ∈ Z k, adaptedCellTranslate (roundedGrid jStar nu) k z ⊆ centeredCube d M) : IsShiftedBigOWithTop P Ψ (belowStartSup rho (roundedGrid jStar nu) jStar t Z F) (boundaryConst Cd g nu * blockSize E F * 3 ^ (-rho * (↑t - ↑jStar))) (boundaryConst Cd g nu * blockSize E F * sourceRemainderScale d jStar K * 3 ^ (-rho * (↑t - ↑jStar)))

The source-tail form of the below-start bound.