High-contrast homogenization: Provider.Quenched.SmallContrastBurnSplitSource

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

The coarse-ellipticity datum at the window's successor scale

The burn-split envelope is stated over the successor scale of a window, so the moment estimates that consume it need a coarse-ellipticity datum carried by that scale rather than by the original source. The window's own tail (e.source.multiplier) supplies it: above the window threshold the successor scale has the source gauge dilated by that threshold, and below it the gauge is flat, which is what an admissible gauge is allowed to be.

The datum is stated at the enlarged scale max 𝒮 S_hat, so the coarse bound of e.coarse.ellipticity transfers by monotonicity and the tail is the union of the two. The dilation and the union factor both enter the growth witness, that is, a scale threshold — which is where the printed account puts them.

noncomputable def HCPolySupport.HighContrast.Quenched.burnSplitSource {d : ℕ} (g : ℝ) (E : BlockMat d) (h : ℤ) (S : CoeffSpace d → ℝ) : CoeffSpace d → ℝ

The enlarged source scale: the original source scale joined with the window's successor scale.

Equations

• HCPolySupport.HighContrast.Quenched.burnSplitSource g E h S a = max (S a) (HCPolySupport.HighContrast.successorScale g E h a).toReal

noncomputable def HCPolySupport.HighContrast.Quenched.burnSplitThreshold (d : ℕ) (K : ℝ) (jStar M : ℤ) : ℝ

The window threshold above which the successor scale carries the source gauge.

Equations

• HCPolySupport.HighContrast.Quenched.burnSplitThreshold d K jStar M = max (3 ^ M) (HCPolySupport.HighContrast.growthBar K ^ (4 * (d + 1)) * 3 ^ (M - jStar + 1))

noncomputable def HCPolySupport.HighContrast.Quenched.burnSplitGauge (Ψ : ℝ → ℝ) (B : ℝ) : ℝ → ℝ

The dilated gauge, flat below the dilation.

Equations

• HCPolySupport.HighContrast.Quenched.burnSplitGauge Ψ B u = max 1 (Ψ (u / B) / (2 * Ψ 1))

theorem HCPolySupport.HighContrast.Quenched.one_le_burnSplitGauge (Ψ : ℝ → ℝ) (B u : ℝ) : 1 ≤ burnSplitGauge Ψ B u

theorem HCPolySupport.HighContrast.Quenched.admissiblePsi_burnSplitGauge {Ψ : ℝ → ℝ} (hadm : IndependentSums.AdmissiblePsi Ψ) {B : ℝ} (hB : 0 < B) : IndependentSums.AdmissiblePsi (burnSplitGauge Ψ B)

theorem HCPolySupport.HighContrast.Quenched.hasPsiGrowth_burnSplitGauge {Ψ : ℝ → ℝ} {K : ℝ} (hadm : IndependentSums.AdmissiblePsi Ψ) (hgrowth : IndependentSums.HasPsiGrowth Ψ K) (hK : 1 < K) {B : ℝ} (hB : 1 ≤ B) {n : ℕ} (hn : 2 * Ψ 1 ≤ K ^ n) : IndependentSums.HasPsiGrowth (burnSplitGauge Ψ B) (B * K ^ (n + 1))

theorem HCPolySupport.HighContrast.Quenched.one_le_burnSplitThreshold {d : ℕ} {K : ℝ} {jStar M : ℤ} (hjM : jStar + 1 ≤ M) : 1 ≤ burnSplitThreshold d K jStar M

The window threshold is at least one.

theorem HCPolySupport.HighContrast.Quenched.measureReal_burnSplitSource_tail {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K Q : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {jStar M : ℤ} (hQ : 1 ≤ Q) (hw : IsCoupledWindow d Q K jStar M) (u : ℝ) : 0 < u → P.real (IndependentSums.upperTailEvent (burnSplitSource g E (M - jStar) S) u) ≤ (burnSplitGauge Ψ (burnSplitThreshold d K jStar M * K) u)⁻¹

The tail of the enlarged source scale. The union of the source tail and the window's successor tail, at the dilated gauge.

theorem HCPolySupport.HighContrast.Quenched.coarseEllipticityDagger_burnSplitSource {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K Q : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {jStar M : ℤ} (hQ : 1 ≤ Q) (hw : IsCoupledWindow d Q K jStar M) {n : ℕ} (hn : 2 * Ψ 1 ≤ K ^ n) : CoarseEllipticityDagger P g E (burnSplitGauge Ψ (burnSplitThreshold d K jStar M * K)) (burnSplitThreshold d K jStar M * K * K ^ (n + 1)) (burnSplitSource g E (M - jStar) S)

The coarse-ellipticity datum at the enlarged source scale. Every clause of e.coarse.ellipticity transfers: the coarse bound by monotonicity of the scale, the tail from the window.

theorem HCPolySupport.HighContrast.Quenched.henvMax_burnsplit_at_burnSplitSource {d : ℕ} [NeZero d] (hd : 2 ≤ d) {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (hstat : IsStationaryLaw P) {g : ℝ} (hg : g ∈ Set.Ico 0 1) {E : BlockMat d} {Ψ : ℝ → ℝ} {K Q : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) {jStar M : ℤ} (hQ : 1 ≤ Q) (hw : IsCoupledWindow d Q K jStar M) {D : ℕ} (hdepth : M - jStar = ↑(2 * D)) {l : ℤ} (hl : ↑(kZero d) ≤ l) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {nu : Mat d} (hnu : Matrix.PosDef nu) (hD : boundaryConst Cd g nu ≤ 3 ^ D) {rho : ℝ} (hrho : g ≤ rho) (t : ℤ) (hgeom : ∀ k ≤ t, ∀ w ∈ Response.alignedIndex (roundedGrid l nu) k t, adaptedCellAt (roundedGrid l nu) k w ⊆ centeredCube d (t + ↑D)) {cIso : ℝ} (hcIso : 0 ≤ cIso) : ∀ᵐ (a : CoeffSpace d) ∂P, Response.diagonalWeakMaximum rho (roundedGrid l nu) t (isotropyReference cIso E) a ≤ ENNReal.ofReal (4 / (1 + cIso) * (max 1 (3 * burnSplitSource g E (M - jStar) S a * 3 ^ (-(↑t + ↑D))) ^ g / 2))

The maximal envelope at the enlarged source scale. The burn-split envelope re-read at the scale carrying the coarse-ellipticity datum.