Coarse-graining support: Support.HighContrast.EntryScale.DeterministicAlgebra.P1

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

Deterministic contrast algebra

Pure-real deterministic algebra from the high-moment paper (Armstrong–Kuusi–Loher, to appear), Section "Deterministic contrast algebra". The scalar drop estimates are paired with the library's operator-norm API for the normalization comparison in e.norm.compare.

def HCPolySupport.HighContrast.EntryScale.contrastDrop (r_m a b : ℝ) : ℝ

The scalar contrast drop r_m^2 (a b - 1).

Source label: e.F.drop.

Equations

• HCPolySupport.HighContrast.EntryScale.contrastDrop r_m a b = r_m ^ 2 * (a * b - 1)

noncomputable def HCPolySupport.HighContrast.EntryScale.terminalTau (r_m a b : ℝ) : ℝ

The terminal additivity defect tau.

Source label: e.tau.terminal.

Equations

• HCPolySupport.HighContrast.EntryScale.terminalTau r_m a b = r_m * (a - 1 + (b - 1)) / 2

def HCPolySupport.HighContrast.EntryScale.noDropWindow (rho F_k F_m : ℝ) : Prop

A no-drop window, written only in terms of the endpoint contrasts.

Source label: e.nodrop.

Equations

• HCPolySupport.HighContrast.EntryScale.noDropWindow rho F_k F_m = (F_k - F_m ≤ rho * F_m)

noncomputable def HCPolySupport.HighContrast.EntryScale.contrastExcessAtScale {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (m : ℕ) : ℝ

The scalar contrast excess F_m = Theta_m - 1.

Source label: e.F.drop.

Equations

• HCPolySupport.HighContrast.EntryScale.contrastExcessAtScale hP hStruct m = HCPolySupport.Book.Ch05.thetaAtScale hP hStruct ↑m - 1

theorem HCPolySupport.HighContrast.EntryScale.sqrt_thetaAtScale_eq_r_m_of_sq_contrastExcess {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (m : ℕ) {r_m : ℝ} (hr_nonneg : 0 ≤ r_m) (hr_sq : r_m ^ 2 = 1 + contrastExcessAtScale hP hStruct m) : √(Book.Ch05.thetaAtScale hP hStruct ↑m) = r_m

Source label e.J.moment.bound: conversion from the library's sqrt(theta_m) scalar to the manuscript's r_m normalization, under the source hypothesis r_m^2 = 1 + F_m.

theorem HCPolySupport.HighContrast.EntryScale.sqrt_thetaAtScale_sub_one_sq_le_contrastExcessAtScale {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : (√(Book.Ch05.thetaAtScale hP hStruct ↑m) - 1) ^ 2 ≤ contrastExcessAtScale hP hStruct m

Source labels p.HC.CR and e.HC.CR: the library's centered coarse-fluctuation term (sqrt(theta_m) - 1)^2 is controlled by the manuscript contrast excess F_m = theta_m - 1.

def HCPolySupport.HighContrast.EntryScale.terminalP (r_m a b : ℝ) : ℝ

The terminal scalar prefactor P_{k,m}.

Source label: e.P.bound.

Equations

• HCPolySupport.HighContrast.EntryScale.terminalP r_m a b = r_m * (a + b)

noncomputable def HCPolySupport.HighContrast.EntryScale.terminalPAtScales {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (k m : ℕ) : ℝ

The concrete terminal scalar prefactor at scales k <= m: P_{k,m} = r_m (a_{k,m} + b_{k,m}).

Source label: e.P.bound.

Equations

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

noncomputable def HCPolySupport.HighContrast.EntryScale.localWeakNormScalarWeightAtScales {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (k m : ℕ) : ℝ

Local weak-norm scalar weight at the left edge of the window. This is the coefficient produced by the raw high-contrast computation before the library's final scale-zero baseline conversion.

Source labels: p.HC.CR and e.P.bound.

Equations

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

@[simp]

theorem HCPolySupport.HighContrast.EntryScale.contrast_drop_eq (r_m a b : ℝ) : contrastDrop r_m a b = r_m ^ 2 * (a * b - 1)

Source label e.F.drop: the contrast drop is r_m^2 (a b - 1).

theorem HCPolySupport.HighContrast.EntryScale.terminalTau_eq_of_barSigma_ratios {sigma theta bm cm bk ck : ℝ} (hbm : 0 < bm) (hcm : 0 < cm) (hck : 0 < ck) (hsigma : sigma = √(bm * cm)) (htheta : theta = bm * cm⁻¹) : 1 / 2 * sigma⁻¹ * (bk - bm) + 1 / 2 * sigma * (ck⁻¹ - cm⁻¹) = terminalTau (√theta) (bk / bm) (ck⁻¹ / cm⁻¹)

Source label e.tau.terminal: real algebra rewriting the library's special-vector tau scalar formula into the paper's r_m, a_{j,m}, b_{j,m} notation.

theorem HCPolySupport.HighContrast.EntryScale.half_terminalP_sub_one_eq_of_barSigma_ratios {sigma theta bm cm bk ck : ℝ} (hbm : 0 < bm) (hcm : 0 < cm) (hck : 0 < ck) (hsigma : sigma = √(bm * cm)) (htheta : theta = bm * cm⁻¹) : 1 / 2 * sigma⁻¹ * bk + 1 / 2 * sigma * ck⁻¹ - 1 = 1 / 2 * terminalP (√theta) (bk / bm) (ck⁻¹ / cm⁻¹) - 1

Source label e.sqrt.tau.absorb: real algebra rewriting the library's special-vector expected-response scalar formula into the paper's terminal prefactor notation.

theorem HCPolySupport.HighContrast.EntryScale.tauAtScale_special_eq_terminalTau_of_P4 {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) (m k : ℕ) (_hk_le_m : k ≤ m) (e : Vec d) (he : Book.Ch02.vecNorm e = 1) : Book.Ch05.tauAtScale P (↑m) (↑k) (Book.Ch05.specialPAtScale hP hStruct (↑m) e) (Book.Ch05.specialQAtScale hP hStruct (↑m) e) = terminalTau (√(Book.Ch05.thetaAtScale hP hStruct ↑m)) (hP.barSigmaAtScale hStruct ↑k / hP.barSigmaAtScale hStruct ↑m) ((hP.barSigmaStarAtScale hStruct ↑k)⁻¹ / (hP.barSigmaStarAtScale hStruct ↑m)⁻¹)

Source label e.tau.terminal: library-facing terminal-pair formula. For the special vectors p_e,q_e, tauAtScale is exactly the local scalar terminalTau with r_m = sqrt Theta_m and the paper ratios a_{k,m}, b_{k,m}.

theorem HCPolySupport.HighContrast.EntryScale.thetaAtScale_le_initialWidetildeTheta_of_P4 {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : Book.Ch05.thetaAtScale hP hStruct ↑m ≤ Book.Ch05.widetildeThetaAtScale P 0 hP4

Source label l.union.bound: the library's Section 52 scalar preliminaries compare the scale-m scalar contrast to the corrected note's initial budget T = widetildeTheta_0.

theorem HCPolySupport.HighContrast.EntryScale.one_le_initialWidetildeTheta_of_P4 {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) : 1 ≤ Book.Ch05.widetildeThetaAtScale P 0 hP4

Source label l.union.bound: the corrected initial contrast budget T = widetildeTheta_0 is at least one under (P4).

theorem HCPolySupport.HighContrast.EntryScale.contrastExcessAtScale_nonneg_of_P4 {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : 0 ≤ contrastExcessAtScale hP hStruct m

Source label e.F.drop: F_m = Theta_m - 1 is nonnegative under (P4).

theorem HCPolySupport.HighContrast.EntryScale.contrastExcessAtScale_antitone_of_P4 {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) : Antitone fun (m : ℕ) => contrastExcessAtScale hP hStruct m

Source label l.det.memory: the manuscript contrast sequence F_m = Theta_m - 1 is nonincreasing in the scale.

theorem HCPolySupport.HighContrast.EntryScale.terminalScalarRatioProduct_eq_theta_ratio {barSigma_j barSigma_m barSigmaStar_j barSigmaStar_m : ℝ} (hbarSigma_m : barSigma_m ≠ 0) (hbarSigmaStar_j : barSigmaStar_j ≠ 0) (hbarSigmaStar_m : barSigmaStar_m ≠ 0) : barSigma_j / barSigma_m * (barSigmaStar_j⁻¹ / barSigmaStar_m⁻¹) = barSigma_j * barSigmaStar_j⁻¹ / (barSigma_m * barSigmaStar_m⁻¹)

Source label l.union.bound: real algebra for the product of the two scalar normalization ratios. In source notation this is a_{j,m} b_{j,m} = Theta_j / Theta_m.

theorem HCPolySupport.HighContrast.EntryScale.terminalScalarRatioProduct_le_initialWidetildeTheta_of_P4 {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) {j m : ℕ} (_hjm : j ≤ m) : hP.barSigmaAtScale hStruct ↑j / hP.barSigmaAtScale hStruct ↑m * ((hP.barSigmaStarAtScale hStruct ↑j)⁻¹ / (hP.barSigmaStarAtScale hStruct ↑m)⁻¹) ≤ Book.Ch05.widetildeThetaAtScale P 0 hP4

Source label l.union.bound: for j <= m, the product of the upper and inverse-star scalar normalization ratios is controlled by the corrected initial budget T = widetildeTheta_0.

theorem HCPolySupport.HighContrast.EntryScale.terminalUpperScalarRatio_le_initialWidetildeTheta_of_P4 {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) {j m : ℕ} (hjm : j ≤ m) : hP.barSigmaAtScale hStruct ↑j / hP.barSigmaAtScale hStruct ↑m ≤ Book.Ch05.widetildeThetaAtScale P 0 hP4

Source label l.union.bound: the upper scalar block of the terminal/intermediate normalization change is controlled by the initial budget T = widetildeTheta_0.

theorem HCPolySupport.HighContrast.EntryScale.terminalInvStarScalarRatio_le_initialWidetildeTheta_of_P4 {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) {j m : ℕ} (hjm : j ≤ m) : (hP.barSigmaStarAtScale hStruct ↑j)⁻¹ / (hP.barSigmaStarAtScale hStruct ↑m)⁻¹ ≤ Book.Ch05.widetildeThetaAtScale P 0 hP4

Source label l.union.bound: the inverse-star scalar block of the terminal/intermediate normalization change is controlled by the initial budget T = widetildeTheta_0.

@[simp]

theorem HCPolySupport.HighContrast.EntryScale.no_drop_window_iff (rho F_k F_m : ℝ) : noDropWindow rho F_k F_m ↔ F_k - F_m ≤ rho * F_m

Source label e.nodrop: unfolding the no-drop condition.

theorem HCPolySupport.HighContrast.EntryScale.rtau_drop (r_m a b : ℝ) (ha : 1 ≤ a) (hb : 1 ≤ b) : r_m * terminalTau r_m a b ≤ 1 / 2 * contrastDrop r_m a b

Source label e.rtau.drop: if a,b ≥ 1, the terminal additivity defect is absorbed by half of the deterministic contrast drop.

theorem HCPolySupport.HighContrast.EntryScale.rtau_drop_of_eq {r_m a b F_j F_m tau : ℝ} (hF : F_j - F_m = contrastDrop r_m a b) (htau : tau = terminalTau r_m a b) (ha : 1 ≤ a) (hb : 1 ≤ b) : r_m * tau ≤ 1 / 2 * (F_j - F_m)

Source label e.rtau.drop: formula-facing version using explicit contrast and terminal-tau hypotheses.

theorem HCPolySupport.HighContrast.EntryScale.sqrt_contrastExcess_mul_tauAtScale_special_le_half_contrastExcess_drop_of_P4 {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) {j m : ℕ} (hjm : j ≤ m) (e : Vec d) (he : Book.Ch02.vecNorm e = 1) : √(1 + contrastExcessAtScale hP hStruct m) * Book.Ch05.tauAtScale P (↑m) (↑j) (Book.Ch05.specialPAtScale hP hStruct (↑m) e) (Book.Ch05.specialQAtScale hP hStruct (↑m) e) ≤ 1 / 2 * (contrastExcessAtScale hP hStruct j - contrastExcessAtScale hP hStruct m)

Source label e.rtau.drop: library-facing terminal-pair version. The special vectors p_e,q_e identify tauAtScale with the terminal scalar tau, and the contrast excesses give the deterministic drop F_j - F_m.

theorem HCPolySupport.HighContrast.EntryScale.expectedResponseJCubeSet_special_eq_half_terminalP_sub_one_of_P4 {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) (m k : ℕ) (e : Vec d) (he : Book.Ch02.vecNorm e = 1) : Book.Ch04.expectedResponseJCubeSet P (originCube d ↑k) (Book.Ch05.specialPAtScale hP hStruct (↑m) e) (Book.Ch05.specialQAtScale hP hStruct (↑m) e) = 1 / 2 * terminalP (√(Book.Ch05.thetaAtScale hP hStruct ↑m)) (hP.barSigmaAtScale hStruct ↑k / hP.barSigmaAtScale hStruct ↑m) ((hP.barSigmaStarAtScale hStruct ↑k)⁻¹ / (hP.barSigmaStarAtScale hStruct ↑m)⁻¹) - 1

Source label e.sqrt.tau.absorb: library-facing formula for the lower-scale expected response of the special terminal pair.

theorem HCPolySupport.HighContrast.EntryScale.mul_le_one_add_rho_of_no_drop {r_m a b F_j F_k F_m rho : ℝ} (hno : noDropWindow rho F_k F_m) (hj_le_k : F_j - F_m ≤ F_k - F_m) (hF : F_j - F_m = contrastDrop r_m a b) (hFm_le_sq : F_m ≤ r_m ^ 2) (hr_sq_pos : 0 < r_m ^ 2) (hrho_pos : 0 < rho) : a * b ≤ 1 + rho

Source label e.no.drop.ab: on a no-drop window, the product excess satisfies a * b ≤ 1 + rho.

theorem HCPolySupport.HighContrast.EntryScale.no_drop_ab_bounds {r_m a b F_j F_k F_m rho : ℝ} (hno : noDropWindow rho F_k F_m) (hj_le_k : F_j - F_m ≤ F_k - F_m) (hF : F_j - F_m = contrastDrop r_m a b) (hFm_le_sq : F_m ≤ r_m ^ 2) (hr_sq_pos : 0 < r_m ^ 2) (hrho_pos : 0 < rho) (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a ∧ a ≤ 1 + rho ∧ 1 ≤ b ∧ b ≤ 1 + rho

Source label e.no.drop.ab: on a no-drop window, scalar terminal ratios stay between 1 and 1 + rho.