High-contrast homogenization: Provider.Response.ProfileRecentCellLp #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The probabilistic recent-cell bound #
The centered maximum has exactly the terminal centered history as its
Q-moment. Monotonicity of probability-space L^p seminorms then turns the
pointwise recent-cell estimate into its printed L² bound.
theorem
HCPolySupport.HighContrast.Response.aemeasurable_profileCenteredMaximum
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{q : Mat d}
(hq : Matrix.PosDef q)
{rhoMax : ℝ}
{jStar t : ℤ}
(hEt : Book.Ch02.BlockPosDef (adaptedMean P q t))
:
AEMeasurable (profileCenteredMaximum P rhoMax q jStar t) P
The centered terminal maximum is an a.e. measurable statistic.
theorem
HCPolySupport.HighContrast.Response.eLpNorm_profileCenteredMaximum_eq
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
{q : Mat d}
{rhoMax Q : ℝ}
(hQ : 0 < Q)
(jStar t : ℤ)
(hmeas : MeasureTheory.AEStronglyMeasurable (profileCenteredMaximum P rhoMax q jStar t) P)
:
MeasureTheory.eLpNorm (profileCenteredMaximum P rhoMax q jStar t) (ENNReal.ofReal Q) P = centeredHistory P Q rhoMax q jStar t ^ Q⁻¹
The L^Q seminorm of the centered maximum is the Q-th root of its
defining history.
theorem
HCPolySupport.HighContrast.Response.eLpNorm_two_profileCenteredMaximum_le
{d : ℕ}
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{q : Mat d}
(hq : Matrix.PosDef q)
{rhoMax Q : ℝ}
(hQ : 2 ≤ Q)
{jStar t : ℤ}
(hEt : Book.Ch02.BlockPosDef (adaptedMean P q t))
:
MeasureTheory.eLpNorm (profileCenteredMaximum P rhoMax q jStar t) 2 P ≤ centeredHistory P Q rhoMax q jStar t ^ Q⁻¹
On a probability space the centered maximum has L² seminorm at most
the Q-th root of the centered history.
theorem
HCPolySupport.HighContrast.Response.eLpNorm_ofReal_mul_le
{d : ℕ}
{X : CoeffSpace d → ENNReal}
{P : MeasureTheory.Measure (CoeffSpace d)}
(hX : MeasureTheory.AEStronglyMeasurable X P)
(c : ℝ)
(p : ENNReal)
:
MeasureTheory.eLpNorm (fun (x : CoeffSpace d) => ENNReal.ofReal c * X x) p P ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm X p P
Multiplication by a finite nonnegative scalar costs at most that scalar in
an extended-real L^p seminorm.