High-contrast homogenization: Provider.Quenched.SmallContrastSourceMoment

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

Source-scale moments from the Dagger tail

The normalized source scale max 1 (S·3^{-s_K}), with 3^{s_K} above the growth witness, has the strong Ψ-tail t ↦ (t·Ψ(t))⁻¹, hence bounded moments of every integer order with the explicit growthBar constants; on the tail event {3^Δ < max 1 (S·3^{-s_K})} any fixed moment of the Δ-rescaled variable decays like 3^{-MΔ}. This is the printed crude-moments display 𝔼[𝒮^{2γ}(𝒮 3^{-n})^{2(1-γ)}] ≤ C(K,Ψ) 3^{-2n} in the form the weak-norm caps consume — no window multiplier, no coupled window, no portable history.

noncomputable def HCPolySupport.HighContrast.Quenched.normalizedSourceScale {d : ℕ} (S : CoeffSpace d → ℝ) (sK : ℤ) : CoeffSpace d → ℝ

The normalized source scale.

Equations

• HCPolySupport.HighContrast.Quenched.normalizedSourceScale S sK a = max 1 (S a * 3 ^ (-sK))

theorem HCPolySupport.HighContrast.Quenched.one_le_normalizedSourceScale {d : ℕ} (S : CoeffSpace d → ℝ) (sK : ℤ) (a : CoeffSpace d) : 1 ≤ normalizedSourceScale S sK a

theorem HCPolySupport.HighContrast.Quenched.measureReal_normalizedSourceScale_tail {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) ⦃t : ℝ⦄ (ht : 1 ≤ t) : P.real {a : CoeffSpace d | t < normalizedSourceScale S sK a} ≤ (t * Ψ t)⁻¹

The strong tail. Above the growth witness, the normalized source scale has the strong Ψ-tail.

theorem HCPolySupport.HighContrast.Quenched.lintegral_normalizedSourceScale_pow_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) (N : ℕ) (hN : 1 ≤ N) : ∫⁻ (a : CoeffSpace d), ENNReal.ofReal (normalizedSourceScale S sK a ^ ↑N) ∂P ≤ ENNReal.ofReal (1 + 2 * ↑N * (1 + Real.log (growthBar K)) * growthBar K ^ IndependentSums.natTriangular N)

The moments. Every integer moment of the normalized source scale is bounded by the explicit growthBar constant.

theorem HCPolySupport.HighContrast.Quenched.setLintegral_normalizedSourceScale_pow_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) (N M : ℕ) (hNM : 1 ≤ N + M) {Delta : ℤ} (hDelta : 0 ≤ Delta) : ∫⁻ (a : CoeffSpace d) in {a : CoeffSpace d | 3 ^ Delta < normalizedSourceScale S sK a}, ENNReal.ofReal ((normalizedSourceScale S sK a * 3 ^ (-Delta)) ^ ↑N) ∂P ≤ ENNReal.ofReal (3 ^ (-(↑M * ↑Delta))) * ENNReal.ofReal (1 + 2 * ↑(N + M) * (1 + Real.log (growthBar K)) * growthBar K ^ IndependentSums.natTriangular (N + M))

The decayed tail moment. On the tail event {3^Δ < V}, the N-th moment of the Δ-rescaled normalized source scale decays like 3^{-MΔ}, for every reserve order M.