High-contrast homogenization: Provider.Transport.WindowMomentBound

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

The multiplier's moment is at most two

The coupled window on which the single source multiplier is built places its alignment scale above the source burn j_{\mathcal S} of e.source.lower.scale, and the third entry of that burn is chosen so that the residual source parameter a_{j_*}^{\mathcal S} = \overline K_{\mathcal S}^{4(d+1)}3^{2-j_*} cancels the weak-Orlicz moment multiplier \mathfrak M_Q(\overline K_{\mathcal S}) furnished by the source tail gauge outright:

j_*\geq 2+4(d+1)\log_3\overline K_{\mathcal S} +\log_3\mathfrak M_Q(\overline K_{\mathcal S}) gives 3^{2-j_*}\leq\overline K_{\mathcal S}^{-4(d+1)} \mathfrak M_Q(\overline K_{\mathcal S})^{-1},

and hence a_{j_*}^{\mathcal S}\mathfrak M_Q\leq1. The moment display of the window multiplier then reads ‖Y_P‖_{L^Q}\leq1+a_{j_*}^{\mathcal S}\mathfrak M_Q \leq2, which is the universal bound \mathcal U = 2 the transport uses for every cell of the window, and squaring it closes the terminal loss, the cost of the source multiplier in the normalized moments.

The growth witness \overline K_{\mathcal S} = \max\{2,K_{\Psi_{\mathcal S}}\} is at least two by construction, which is what makes both logarithms and the moment multiplier positive.

The two positive scalar witnesses

theorem HCPolySupport.HighContrast.Transport.two_le_growthBar (K : ℝ) : 2 ≤ growthBar K

The growth witness \overline K_{\mathcal S} = \max\{2,K_{\Psi_{\mathcal S}}\} is at least two.

theorem HCPolySupport.HighContrast.Transport.zero_lt_momentMultiplier {Q K : ℝ} (hQ : 0 < Q) : 0 < momentMultiplier Q (growthBar K)

The weak-Orlicz moment multiplier is positive: its base exceeds one, the growth witness being at least two.

The burn cancels the moment multiplier

theorem HCPolySupport.HighContrast.Transport.sourceRemainderScale_mul_momentMultiplier_le_one {d : ℕ} {Q K : ℝ} (hQ : 0 < Q) {jStar M : ℤ} (hw : IsCoupledWindow d Q K jStar M) : sourceRemainderScale d jStar K * momentMultiplier Q (growthBar K) ≤ 1

The source-remainder scale cancels the moment multiplier. This is what the third entry of the source burn is for: at any alignment scale above the burn the product is at most one.

The universal moment bound and the terminal loss

theorem HCPolySupport.HighContrast.Transport.lqNorm_le_two {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K Cd : ℝ} {jStar M : ℤ} {Y : CoeffSpace d → ℝ} {Q : ℝ} (hQ : 1 ≤ Q) (hw : IsCoupledWindow d Q K jStar M) (hY : IsWindowMultiplier P g E Ψ K Cd jStar M Y) : lqNorm P Q Y ≤ 2

The universal moment bound ‖Y_P‖_{L^Q}\leq\mathcal U = 2. The window multiplier's own moment display, with the source burn absorbing the remainder scale.

theorem HCPolySupport.HighContrast.Transport.integral_le_two {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {Q : ℝ} {Y : CoeffSpace d → ℝ} (hnorm : ENNReal.ofReal (∫ (a : CoeffSpace d), Y a ∂P) ≤ lqNorm P Q Y) (htwo : lqNorm P Q Y ≤ 2) : ∫ (a : CoeffSpace d), Y a ∂P ≤ 2

An L^Q upper bound by two converts an ofReal bound for a multiplier's mean into the corresponding real upper bound.

theorem HCPolySupport.HighContrast.Transport.zero_lt_sourceRemainderScale (d : ℕ) (jStar : ℤ) (K : ℝ) : 0 < sourceRemainderScale d jStar K

The source-remainder scale is positive.

theorem HCPolySupport.HighContrast.Transport.lqNorm_sq_le_four {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K Cd : ℝ} {jStar M : ℤ} {Y : CoeffSpace d → ℝ} {Q : ℝ} (hQ : 1 ≤ Q) (hw : IsCoupledWindow d Q K jStar M) (hY : IsWindowMultiplier P g E Ψ K Cd jStar M Y) : lqNorm P Q Y ^ 2 ≤ 4

The squared moment bound ‖Y_P‖_{L^Q}^2\leq4, the last inequality in the cost of the source multiplier in the normalized moments.