High-contrast homogenization: Provider.Window.MultiplierMoment #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The coupled burn gives the uniform multiplier moment #
The third ceiling in sourceBurn was chosen so that the source-remainder
scale times the weak-Orlicz moment multiplier is at most one. This file opens
that ceiling and records the resulting L^Q bound by two.
theorem
HCPolySupport.HighContrast.Window.sourceRemainderScale_mul_momentMultiplier_le_one
{d : ℕ}
{Q K : ℝ}
(hQ : 1 ≤ Q)
{jStar M : ℤ}
(hw : IsCoupledWindow d Q K jStar M)
:
The quantitative content of the third source-burn ceiling.
theorem
HCPolySupport.HighContrast.Window.lqNorm_le_two
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{g : ℝ}
{E : BlockMat d}
{Ψ : ℝ → ℝ}
{K Cd Q : ℝ}
{jStar M : ℤ}
(hQ : 1 ≤ Q)
(hw : IsCoupledWindow d Q K jStar M)
{Y : CoeffSpace d → ℝ}
(hY : IsWindowMultiplier P g E Ψ K Cd jStar M Y)
:
Every common window multiplier has L^Q norm at most two at the coupled
exponent.