High-contrast homogenization: Provider.Quenched.SmallContrastWeakEnergyTailAtLevel

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

The moment package at the matched threshold, and the bad energy it produces

The maximal function's almost-sure envelope is R · (max 1 x) ^ g / 2. The fixed-level package takes the excess above 1 / 2, which is strictly below the envelope's own value on the good set, so a generation-independent constant survives the good part of the moment split.

Here the excess is taken above R / 2, the envelope's value on the good set. The good part of the split then contributes nothing at all, and the fourth moment is the bad part alone — R ^ 4 times the source's crude moment, with no additive term. The bad-event level stays free: the majorant's small-drift branch is guarded by beta < lev, and the matched threshold beta = R / 2 needs a level above it.

Everything else in the argument is the fixed-level one, term for term: the scale identity, the bad-event envelope for the excess, and the source's crude moment are all read at the same places.

theorem HCPolySupport.HighContrast.Quenched.weakMaximum_moment_package_at {d : ℕ} {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {l : ℤ} (hl : ↑(kZero d) ≤ l) {n : Mat d} (hn : Matrix.PosDef n) {rho : ℝ} (t : ℤ) {G : ℕ} {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) (hDelta : 0 ≤ t + ↑G - 1 - sK) {F : BlockMat d} (hFsym : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {R : ℝ} (hR1 : 1 ≤ R) (henvMax : ∀ᵐ (a : CoeffSpace d) ∂P, Response.diagonalWeakMaximum rho (roundedGrid l n) t F a ≤ ENNReal.ofReal (R * (max 1 (3 * S a * 3 ^ (-(↑t + ↑G))) ^ g / 2))) : ∃ (W : CoeffSpace d → ENNReal), AEMeasurable W P ∧ (∀ (a : CoeffSpace d), Response.diagonalWeakMaximum rho (roundedGrid l n) t F a ≤ W a + ENNReal.ofReal (R / 2)) ∧ MeasureTheory.eLpNorm (Response.diagonalWeakMaximum rho (roundedGrid l n) t F) (ENNReal.ofReal 4) P ≤ ENNReal.ofReal ((R ^ 4 * badMomentMajorant K (t + ↑G - 1 - sK)) ^ 4⁻¹ + R / 2) ∧ ∫⁻ (a : CoeffSpace d), W a ^ 4 ∂P ≤ ENNReal.ofReal (R ^ 4 * badMomentMajorant K (t + ↑G - 1 - sK))

The moment package at the matched threshold. The excess above R / 2, its fourth moment against R ^ 4 times the crude moment — with no residue — and the maximum's own L⁴ norm.

The bad energies at the matched threshold

theorem HCPolySupport.HighContrast.Quenched.profileBadEnergyAt_of_maximum_envelope {d : ℕ} {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {l : ℤ} (hl : ↑(kZero d) ≤ l) {n : Mat d} (hn : Matrix.PosDef n) {rho : ℝ} (t : ℤ) {G : ℕ} {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) (hDelta : 0 ≤ t + ↑G - 1 - sK) {F : BlockMat d} (hFsym : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {R lev : ℝ} (hR1 : 1 ≤ R) (hlev : 1 ≤ lev) (henvMax : ∀ᵐ (a : CoeffSpace d) ∂P, Response.diagonalWeakMaximum rho (roundedGrid l n) t F a ≤ ENNReal.ofReal (R * (max 1 (3 * S a * 3 ^ (-(↑t + ↑G))) ^ g / 2))) (p r : Vec d) : (Response.profileBadEnergyAt P (ENNReal.ofReal lev) (Response.diagonalWeakMaximum rho (roundedGrid l n) t F) fun (a : CoeffSpace d) => Response.diagonalWeakEnergy ⋯ t a p r) ≤ ENNReal.ofReal (√2 * Response.profileEnergyLoad (Response.diagonalWeakLoadMinus F p r) p r * Response.profileBadMajorantAt 4 (R ^ 4 * badMomentMajorant K (t + ↑G - 1 - sK)) (R / 2) lev)

The primal bad-event energy at the matched threshold and a free level. The residue-free majorant R ^ 4 · badMomentMajorant in place of the scaled one, at the threshold pair (R / 2, lev).

theorem HCPolySupport.HighContrast.Quenched.profileBadEnergyAt_adjoint_of_maximum_envelope {d : ℕ} {g : ℝ} (hg : g ∈ Set.Ico 0 1) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {l : ℤ} (hl : ↑(kZero d) ≤ l) {n : Mat d} (hn : Matrix.PosDef n) {rho : ℝ} (t : ℤ) {G : ℕ} {sK : ℤ} (hsK : growthBar K ≤ 3 ^ sK) (hDelta : 0 ≤ t + ↑G - 1 - sK) {F : BlockMat d} (hFsym : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {R lev : ℝ} (hR1 : 1 ≤ R) (hlev : 1 ≤ lev) (henvMax : ∀ᵐ (a : CoeffSpace d) ∂P, Response.diagonalWeakMaximum rho (roundedGrid l n) t F a ≤ ENNReal.ofReal (R * (max 1 (3 * S a * 3 ^ (-(↑t + ↑G))) ^ g / 2))) (p r : Vec d) : (Response.profileBadEnergyAt P (ENNReal.ofReal lev) (Response.diagonalWeakMaximum rho (roundedGrid l n) t F) fun (a : CoeffSpace d) => Response.diagonalWeakAdjointEnergy ⋯ t a p r) ≤ ENNReal.ofReal (√2 * Response.profileEnergyLoad (Response.diagonalWeakLoadPlus F p r) p r * Response.profileBadMajorantAt 4 (R ^ 4 * badMomentMajorant K (t + ↑G - 1 - sK)) (R / 2) lev)

The adjoint bad-event energy at the matched threshold and a free level. The same package, the mirrored load.