Coarse-graining support: Support.HighContrast.EntryScale.BadMaximal.P1 #

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

Bad maximal observable #

This file isolates the manuscript bad-event maximal slot from the scalar post-split bound used in the no-drop response estimate.

source

noncomputable def HCPolySupport.HighContrast.EntryScale.badEventTruncation {Ω : Type u_1} (M : Ω → ℝ) :

Ω → ℝ

Threshold a nonnegative maximal observable to the bad event {1 < M}.

Equations

HCPolySupport.HighContrast.EntryScale.badEventTruncation M ω = if 1 < M ω then M ω else 0

Instances For

source

theorem HCPolySupport.HighContrast.EntryScale.badEventTruncation_nonneg {Ω : Type u_1} {M : Ω → ℝ} {ω : Ω} (hM_nonneg : 0 ≤ M ω) :

0 ≤ badEventTruncation M ω

Nonnegativity of the bad-event truncation for a nonnegative observable.

source

theorem HCPolySupport.HighContrast.EntryScale.badEventTruncation_le_self_of_nonneg {Ω : Type u_1} {M : Ω → ℝ} {ω : Ω} (hM_nonneg : 0 ≤ M ω) :

badEventTruncation M ω ≤ M ω

The bad-event truncation is bounded by the original nonnegative observable.

source

theorem HCPolySupport.HighContrast.EntryScale.le_min_one_add_badEventTruncation {Ω : Type u_1} {M : Ω → ℝ} {ω : Ω} :

M ω ≤ min (M ω) 1 + badEventTruncation M ω

Sharp good/bad split of a nonnegative maximal observable: on the good event {M <= 1} the observable equals min M 1, and on the bad event {1 < M} it is paid by the bad-event truncation at first power (with the harmless extra min M 1 = 1). This is the first-power replacement for the crude split M <= 1 + badEventTruncation M.

source

theorem HCPolySupport.HighContrast.EntryScale.maximal_mul_le_min_one_mul_add_badEventTruncation_mul {Ω : Type u_1} {M : Ω → ℝ} {ω : Ω} {J : ℝ} (hJ_nonneg : 0 ≤ J) :

M ω * J ≤ min (M ω) 1 * J + badEventTruncation M ω * J

First-power good/bad split of a nonnegative maximal factor against a nonnegative response: M * J is paid by min M 1 * J on the good event and by badEventTruncation M * J on the bad event. No squaring and no deterministic cap on J is introduced.

source

theorem HCPolySupport.HighContrast.EntryScale.aestronglyMeasurable_badEventTruncation {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {M : Ω → ℝ} (hM : MeasureTheory.AEStronglyMeasurable M μ) :

MeasureTheory.AEStronglyMeasurable (badEventTruncation M) μ

The bad-event truncation of an a.e. strongly measurable observable is a.e. strongly measurable.

source

noncomputable def HCPolySupport.HighContrast.EntryScale.terminalBadMaximalDriftSup {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hc : HighContrastExponents d) {N m : ℕ} (hNm : N ≤ m) :

ℝ

The deterministic weighted drift supremum in the manuscript split of \mathcal M_m.

Equations

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

Instances For

source

noncomputable def HCPolySupport.HighContrast.EntryScale.terminalBadMaximalSplitEnvelope {Ω : Type u_1} {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hc : HighContrastExponents d) {N m : ℕ} (hNm : N ≤ m) (Q : TriadicCube d) (a : Ω → RegCoeffField d) (M_sub : ℕ → Ω → ℝ) :

Ω → ℝ

The stochastic/subthreshold/deterministic random envelope that appears after the manuscript positive-part split. This is not the source observable itself; it is the pointwise upper envelope whose square is later integrated.

Equations

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

Instances For

source

theorem HCPolySupport.HighContrast.EntryScale.terminalCoarseBlockStochasticMax_nonneg {Ω : Type u_1} {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hc : HighContrastExponents d) (N m : ℕ) (Q : TriadicCube d) (a : Ω → RegCoeffField d) (ω : Ω) :

0 ≤ terminalCoarseBlockStochasticMax hP hStruct hc N m Q a ω

source

theorem HCPolySupport.HighContrast.EntryScale.terminalBadMaximalDriftSup_nonneg {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hc : HighContrastExponents d) {N m : ℕ} (hNm : N ≤ m) :

0 ≤ terminalBadMaximalDriftSup hP hStruct hc hNm

source

theorem HCPolySupport.HighContrast.EntryScale.weighted_terminalAnnealedFullBlockDriftAtScales_le_terminalBadMaximalDriftSup {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hc : HighContrastExponents d) {N m j : ℕ} (hNm : N ≤ m) (hj : j ∈ Finset.Icc N m) :

3 ^ (-(hc.rhoM * ↑(m - j))) * terminalAnnealedFullBlockDriftAtScales hP hStruct j m ≤ terminalBadMaximalDriftSup hP hStruct hc hNm

Any scale term in the deterministic drift split is selected by the drift supremum over the high-scale window.

source

theorem HCPolySupport.HighContrast.EntryScale.fullBlockOperatorNorm_add_le {d : ℕ} (A B : FullBlockMat d) :

fullBlockOperatorNorm (A + B) ≤ fullBlockOperatorNorm A + fullBlockOperatorNorm B

source

theorem HCPolySupport.HighContrast.EntryScale.fullBlockOperatorNorm_posPart_le {d : ℕ} (M : FullBlockMat d) :

fullBlockOperatorNorm M⁺ ≤ fullBlockOperatorNorm M

The operator norm of the C-star positive part is bounded by the operator norm of the original full-block matrix.

This is the local analytic bridge behind the manuscript step |(X)_+| ≤ |X|. It is proved by diagonalizing self-adjoint matrices and using unitary invariance of the C-star norm; non-self-adjoint matrices have zero positive part by the Mathlib definition.

source

noncomputable def HCPolySupport.HighContrast.EntryScale.terminalSpectralPositivePartAtScale {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (m : ℕ) (Q : TriadicCube d) (a : RegCoeffField d) :

ℝ

The literal terminally-normalized spectral positive part on one block.

This uses the library's normalized full-block fluctuation matrix for Ahom_m^{-1/2} (bfA(Q) - Ahom_m) Ahom_m^{-1/2} and mathlib's C-star positive part M⁺.

Equations