Coarse-graining support: Support.Book.Ch05.Theorems.Section57.ProbeEnvelope

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Concrete finite-probe envelope

This file packages the deterministic finite-basis envelope used by the quenched bad-pair estimates.

noncomputable def HCPolySupport.Book.Ch05.Section57.quenchedProbeEnvelopeConst (d : ℕ) : ℝ

Dimension-only finite-probe constant in the quenched envelope.

Equations

• HCPolySupport.Book.Ch05.Section57.quenchedProbeEnvelopeConst d = 4 * ↑(Fintype.card (HCPolySupport.BlockCoord d)) * ↑(Fintype.card (HCPolySupport.Book.Ch05.Section57.NormalizedProbeIndex d))

theorem HCPolySupport.Book.Ch05.Section57.quenchedProbeEnvelopeConst_nonneg (d : ℕ) : 0 ≤ quenchedProbeEnvelopeConst d

theorem HCPolySupport.Book.Ch05.Section57.quenchedProbeEnvelopeConst_pos (d : ℕ) [NeZero d] : 0 < quenchedProbeEnvelopeConst d

noncomputable def HCPolySupport.Book.Ch05.Section57.quenchedProbeEnvelope {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m n : ℕ) : RegCoeffField d → ℝ

The finite-probe envelope controlling all localized unit-vector responses.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section57.localizedLimitNormalizedJMax_le_quenchedProbeEnvelope_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {m n : ℕ} (hnm : n ≤ m) (e : FullBlockVec d) (he : e ⬝ᵥ e ≤ 1) : localizedLimitNormalizedJMax hP hStruct m n e ≤ᵐ[P] quenchedProbeEnvelope hP hStruct m n