High-contrast homogenization: Provider.Quenched.SmallContrastSlotBoundsSplit

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

The burn-split slots at a parametrized normalizer

The shallow and deep slot bounds at the burn-split supply: the supply value supplyMscSplit d E = (2d)^{1/2}·(κ_𝐄·4)·8·√2 carries no boundary constant and no grid-norm power.

noncomputable def HCPolySupport.HighContrast.Quenched.supplyMscSplit (d : ℕ) (E : BlockMat d) : ℝ

The burn-split supply value: dimensional up to κ_𝐄.

Equations

• HCPolySupport.HighContrast.Quenched.supplyMscSplit d E = (2 * ↑d) ^ 2⁻¹ * (HCPolySupport.HighContrast.kappaRef E * 4) * (2 * 4) * √2

theorem HCPolySupport.HighContrast.Quenched.supplyMscSplit_nonneg (d : ℕ) (E : BlockMat d) : 0 ≤ supplyMscSplit d E

theorem HCPolySupport.HighContrast.Quenched.entry_supply_slot_bound_of_block_split {d : ℕ} [NeZero d] (hd : 2 ≤ 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) (hstat : IsStationaryLaw P) {lAl : ℤ} (hl : ↑(kZero d) ≤ lAl) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {mAl : Mat d} (hn : Matrix.PosDef mAl) (hgrid : IsRoundedGrid lAl (roundedGrid lAl mAl)) {Gacc : ℕ} (hqnorm : ‖roundedGrid lAl mAl‖ * √↑d ≤ 3 ^ Gacc) (hDbc : boundaryConst Cd g mAl ≤ 3 ^ (Gacc + 1)) (hmeso : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (m : ℤ), S a ≤ 3 ^ m → ∀ k ≤ m, ∀ (w : Fin d → ℤ), standardCellCenter k w ∈ centeredCube d m → BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (g * max (↑m - 2 * ↑(Gacc + 1) - ↑k) 0)) E)) {sKw : ℤ} (hsKw : growthBar K ≤ 3 ^ sKw) {jb p t : ℤ} (hjb : lAl ≤ jb) (hjbp : jb ≤ p) (hpt : p ≤ t) (hsKjb : sKw ≤ jb) (M : ℕ) (hburn : 1 + 2 * ↑(2 + M) * (1 + Real.log (growthBar K)) * growthBar K ^ IndependentSums.natTriangular (2 + M) ≤ 3 ^ (↑M * ↑(jb + ↑(Gacc + 1) - 1 - sKw))) (hsmjb : ↑d * (adaptedHattedContrast P (roundedGrid lAl mAl) jb - 1) ≤ 1 / 2) (hsmp : ↑d * (adaptedHattedContrast P (roundedGrid lAl mAl) p - 1) ≤ 1 / 2) (hdropB : 4 * ↑d * (adaptedHattedContrast P (roundedGrid lAl mAl) jb - adaptedHattedContrast P (roundedGrid lAl mAl) t) ≤ 1) {F : BlockMat d} (hFsym : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) (henvF : BlockMatLoewnerLE (adaptedMean P (roundedGrid lAl mAl) p) F) {Csub : ℝ} (hCsub : 0 < Csub) (hsubdiv : ∀ (j' p' : ℤ), lAl ≤ j' → j' ≤ p' → ∃ (Z : Finset (Fin d → ℤ)), ↑Z = {w : Fin d → ℤ | adaptedCellCenter (roundedGrid lAl mAl) j' w ∈ adaptedCell (roundedGrid lAl mAl) p'} ∧ Z.card = 3 ^ (d * (p' - j').toNat) ∧ Z.Nonempty ∧ lqSchattenSize P 2 (fun (a : CoeffSpace d) => blockSub (ofFullBlockMat ((↑Z.card)⁻¹ • ∑ w ∈ Z, toFullBlockMat (coarseBlock (adaptedCellAt (roundedGrid lAl mAl) j' w) a))) (adaptedMean P (roundedGrid lAl mAl) j')) (adaptedMean P (roundedGrid lAl mAl) p') ≤ ENNReal.ofReal (Csub * ↑Z.card ^ (-2⁻¹)) * lqSchattenSize P 2 (fun (a : CoeffSpace d) => blockSub (coarseBlock (adaptedCell (roundedGrid lAl mAl) j') a) (adaptedMean P (roundedGrid lAl mAl) j')) (adaptedMean P (roundedGrid lAl mAl) p')) (hdropP : 4 * ↑d * (adaptedHattedContrast P (roundedGrid lAl mAl) jb - adaptedHattedContrast P (roundedGrid lAl mAl) p) ≤ 1) : scaleVariance P (roundedGrid lAl mAl) F p ≤ ENNReal.ofReal (slotSourceValue d Csub (supplyMscSplit d E) (p - jb).toNat + slotBaseCoefficient d * hatExcessAt P (roundedGrid lAl mAl) jb)

The shallow slot, at a parametrized normalizer.

theorem HCPolySupport.HighContrast.Quenched.entry_supply_deep_slot_bound_of_block_split {d : ℕ} [NeZero d] (hd : 2 ≤ 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) (hstat : IsStationaryLaw P) {lAl : ℤ} (hl : ↑(kZero d) ≤ lAl) {Cd : ℝ} (hCd : max 1 (12 * ↑d * √↑d) ≤ Cd) {mAl : Mat d} (hn : Matrix.PosDef mAl) (hgrid : IsRoundedGrid lAl (roundedGrid lAl mAl)) {Gacc : ℕ} (hqnorm : ‖roundedGrid lAl mAl‖ * √↑d ≤ 3 ^ Gacc) (hDbc : boundaryConst Cd g mAl ≤ 3 ^ (Gacc + 1)) (hmeso : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (m : ℤ), S a ≤ 3 ^ m → ∀ k ≤ m, ∀ (w : Fin d → ℤ), standardCellCenter k w ∈ centeredCube d m → BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (g * max (↑m - 2 * ↑(Gacc + 1) - ↑k) 0)) E)) {sKw : ℤ} (hsKw : growthBar K ≤ 3 ^ sKw) {p t : ℤ} (hlp : lAl ≤ p) (hpt : p ≤ t) (hsKp : sKw ≤ p) (M : ℕ) (hburn : 1 + 2 * ↑(2 + M) * (1 + Real.log (growthBar K)) * growthBar K ^ IndependentSums.natTriangular (2 + M) ≤ 3 ^ (↑M * ↑(p + ↑(Gacc + 1) - 1 - sKw))) {delta : ℝ} (hsmp : hatExcessAt P (roundedGrid lAl mAl) p ≤ delta) (hdelta2 : delta ≤ 1 / 2) (hdropB : 4 * ↑d * (adaptedHattedContrast P (roundedGrid lAl mAl) p - adaptedHattedContrast P (roundedGrid lAl mAl) t) ≤ 1) {F : BlockMat d} (hFsym : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) (henvF : BlockMatLoewnerLE (adaptedMean P (roundedGrid lAl mAl) p) F) {Csub : ℝ} (hCsub : 0 < Csub) (hsubdiv : ∀ (j' p' : ℤ), lAl ≤ j' → j' ≤ p' → ∃ (Z : Finset (Fin d → ℤ)), ↑Z = {w : Fin d → ℤ | adaptedCellCenter (roundedGrid lAl mAl) j' w ∈ adaptedCell (roundedGrid lAl mAl) p'} ∧ Z.card = 3 ^ (d * (p' - j').toNat) ∧ Z.Nonempty ∧ lqSchattenSize P 2 (fun (a : CoeffSpace d) => blockSub (ofFullBlockMat ((↑Z.card)⁻¹ • ∑ w ∈ Z, toFullBlockMat (coarseBlock (adaptedCellAt (roundedGrid lAl mAl) j' w) a))) (adaptedMean P (roundedGrid lAl mAl) j')) (adaptedMean P (roundedGrid lAl mAl) p') ≤ ENNReal.ofReal (Csub * ↑Z.card ^ (-2⁻¹)) * lqSchattenSize P 2 (fun (a : CoeffSpace d) => blockSub (coarseBlock (adaptedCell (roundedGrid lAl mAl) j') a) (adaptedMean P (roundedGrid lAl mAl) j')) (adaptedMean P (roundedGrid lAl mAl) p')) : scaleVariance P (roundedGrid lAl mAl) F p ≤ ENNReal.ofReal (slotSourceValue d Csub (supplyMscSplit d E) 0 + slotBaseCoefficient d * delta)

The deep slot, at a parametrized normalizer.