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

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

theorem HCPolySupport.HighContrast.EntryScale.ofReal_terminalCenteredBlockOperatorNorm_le_initialTheta_mul_intermediate {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) (Y : FullBlockMat d) : ENNReal.ofReal (fullBlockOperatorNorm (scalarFullBlockNormalizerMatrixAtScale hP hStruct m * scalarCenteredFullBlockMatrixAtScale hP hStruct j Y * scalarFullBlockNormalizerMatrixAtScale hP hStruct m)) ≤ ENNReal.ofReal (Book.Ch05.widetildeThetaAtScale P 0 hP4) * ENNReal.ofReal (fullBlockOperatorNorm (scalarFullBlockNormalizerMatrixAtScale hP hStruct j * scalarCenteredFullBlockMatrixAtScale hP hStruct j Y * scalarFullBlockNormalizerMatrixAtScale hP hStruct j))

Source label l.union.bound: ENNReal form of the terminal/intermediate normalization comparison, ready to combine with the high-moment envelope.

noncomputable def HCPolySupport.HighContrast.EntryScale.intermediateCenteredFullBlockDeviation {Ω : Type u_1} {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (Y : ℕ → TriadicCube d → Ω → FullBlockMat d) : ℕ → TriadicCube d → Ω → ENNReal

Source label a.HM: concrete intermediate-scale centered full-block deviation. The matrix argument Y j Q ω is the full-block coarse coefficient matrix attached to the cube Q; the normalization and centering are both at scale j.

Equations

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

noncomputable def HCPolySupport.HighContrast.EntryScale.terminalCenteredFullBlockDeviation {Ω : Type u_1} {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (m : ℕ) (Y : ℕ → TriadicCube d → Ω → FullBlockMat d) : ℕ → TriadicCube d → Ω → ENNReal

Source label l.union.bound: terminal-scale normalization of the same full-block matrix centered at scale j.

Equations

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

theorem HCPolySupport.HighContrast.EntryScale.terminalCenteredFullBlockDeviation_le_initialWidetildeTheta_mul_intermediate_of_P4 {Ω : Type u_1} {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (Y : ℕ → TriadicCube d → Ω → FullBlockMat d) {j : ℕ} (hjm : j ≤ m) (Q : TriadicCube d) (ω : Ω) : terminalCenteredFullBlockDeviation hP hStruct m Y j Q ω ≤ ENNReal.ofReal (Book.Ch05.widetildeThetaAtScale P 0 hP4) * intermediateCenteredFullBlockDeviation hP hStruct Y j Q ω

Source labels a.HM and l.union.bound: the terminal-normalized concrete centered full-block deviation is bounded by T = widetildeTheta_0 times the intermediate-normalized deviation from the high-moment hypothesis.

noncomputable def HCPolySupport.HighContrast.EntryScale.coarseFullBlockMatrixAtCubeProcess {Ω : Type u_1} {d : ℕ} (a : Ω → RegCoeffField d) : ℕ → TriadicCube d → Ω → FullBlockMat d

Source label a.HM: the library's full-block coarse matrix process on a triadic cube. The scale parameter is present only to match the high-moment observable shape.

Equations

• HCPolySupport.HighContrast.EntryScale.coarseFullBlockMatrixAtCubeProcess a _j Q ω = HCPolySupport.Book.Ch04.coarseFullBlockMatrixAtCube Q (a ω)

noncomputable def HCPolySupport.HighContrast.EntryScale.intermediateCoarseBlockDeviation {Ω : Type u_1} {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (a : Ω → RegCoeffField d) : ℕ → TriadicCube d → Ω → ENNReal

Source label a.HM: the manuscript's intermediate-normalized centered coarse-block deviation |Ahom_j^{-1/2} (bfA(Q)-Ahom_j) Ahom_j^{-1/2}|.

Equations

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

noncomputable def HCPolySupport.HighContrast.EntryScale.terminalCoarseBlockDeviation {Ω : Type u_1} {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (m : ℕ) (a : Ω → RegCoeffField d) : ℕ → TriadicCube d → Ω → ENNReal

Source label l.union.bound: terminal-normalized centered coarse-block deviation used in the maximal union bound.

Equations

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

theorem HCPolySupport.HighContrast.EntryScale.fullBlockNormalizedFluctuationOperatorNormSqAtScale_eq_terminal_norm_sq {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) : Book.Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) Q a = fullBlockOperatorNorm (scalarFullBlockNormalizerMatrixAtScale hP hStruct m * scalarCenteredFullBlockMatrixAtScale hP hStruct m (Book.Ch04.coarseFullBlockMatrixAtCube Q a) * scalarFullBlockNormalizerMatrixAtScale hP hStruct m) ^ 2

Source label l.S.and.J: the library's squared terminal full-block fluctuation observable is the square of the local full-block operator norm with the same terminal normalization.

theorem HCPolySupport.HighContrast.EntryScale.fullBlockNormalizedFluctuationOperatorNormSqAtScale_le_two_stochastic_add_two_drift {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (j m : ℕ) (Q : TriadicCube d) (a : RegCoeffField d) : Book.Ch04.fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) Q a ≤ 2 * fullBlockOperatorNorm (scalarFullBlockNormalizerMatrixAtScale hP hStruct m * scalarCenteredFullBlockMatrixAtScale hP hStruct j (Book.Ch04.coarseFullBlockMatrixAtCube Q a) * scalarFullBlockNormalizerMatrixAtScale hP hStruct m) ^ 2 + 2 * fullBlockOperatorNorm (scalarFullBlockNormalizerMatrixAtScale hP hStruct m * (toFullBlockMat (Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct ↑j) - toFullBlockMat (Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct ↑m)) * scalarFullBlockNormalizerMatrixAtScale hP hStruct m) ^ 2

Source label l.S.and.J: deterministic split of the library's terminal full-block fluctuation into the stochastic centered-at-j block and the deterministic annealed drift Ahom_j - Ahom_m.

theorem HCPolySupport.HighContrast.EntryScale.terminal_p_le_four_mul_of_ab_bounds {r_m a b rho : ℝ} (hr_nonneg : 0 ≤ r_m) (hrho_le_one : rho ≤ 1) (ha : a ≤ 1 + rho) (hb : b ≤ 1 + rho) : terminalP r_m a b ≤ 4 * r_m

Source label e.P.bound: if a,b ≤ 1 + rho and rho ≤ 1, then P_{k,m} = r_m(a+b) is at most 4 r_m.

theorem HCPolySupport.HighContrast.EntryScale.p_bound_of_no_drop {r_m a b F_k F_m rho P_km : ℝ} (hno : noDropWindow rho F_k F_m) (hF : F_k - F_m = contrastDrop r_m a b) (hP : P_km = terminalP r_m a b) (hFm_le_sq : F_m ≤ r_m ^ 2) (hr_sq_pos : 0 < r_m ^ 2) (hr_nonneg : 0 ≤ r_m) (hrho_pos : 0 < rho) (hrho_le_one : rho ≤ 1) (ha : 1 ≤ a) (hb : 1 ≤ b) : P_km ≤ 4 * r_m

Source label e.P.bound: no-drop version of the terminal prefactor bound.

theorem HCPolySupport.HighContrast.EntryScale.terminalPAtScales_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) {k m : ℕ} (hkm : k ≤ m) : 0 ≤ terminalPAtScales hP hStruct k m

Source label e.P.bound: the concrete terminal prefactor is nonnegative.

theorem HCPolySupport.HighContrast.EntryScale.sqrt_one_add_contrastExcessAtScale_le_terminalPAtScales_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) {k m : ℕ} (hkm : k ≤ m) : √(1 + contrastExcessAtScale hP hStruct m) ≤ terminalPAtScales hP hStruct k m

Source labels p.HC.CR and e.P.bound: the concrete terminal prefactor dominates the terminal square-root scale. Under (P4), the scalar ratios a_{k,m} and b_{k,m} are each at least one, so P_{k,m} = r_m (a_{k,m}+b_{k,m}) is in particular at least r_m.

theorem HCPolySupport.HighContrast.EntryScale.two_mul_sqrtTheta_le_terminalPAtScales_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) {k m : ℕ} (hkm : k ≤ m) : 2 * √(Book.Ch05.thetaAtScale hP hStruct ↑m) ≤ terminalPAtScales hP hStruct k m

Source labels p.HC.CR and e.P.bound: the terminal prefactor dominates twice the library's scalar sqrt(theta_m). Under (P4) both scalar ratios a_{k,m} and b_{k,m} are at least one, so P_{k,m} = r_m (a_{k,m} + b_{k,m}) >= 2 r_m = 2 sqrt(theta_m). This is the sharp pricing needed to pay the summed-weight first-power source split with 2 * r_m instead of the crude 2 * (1 + F_m).

theorem HCPolySupport.HighContrast.EntryScale.localWeakNormScalarWeightAtScales_eq_terminalPAtScales_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) (k m : ℕ) : localWeakNormScalarWeightAtScales hP hStruct k m = terminalPAtScales hP hStruct k m

Source labels p.HC.CR and e.P.bound: the local weak-norm scalar coefficient is exactly the manuscript terminal prefactor P_{k,m}.

theorem HCPolySupport.HighContrast.EntryScale.terminalPAtScales_le_four_mul_sqrt_contrastExcess_of_noDrop_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) {k m : ℕ} (hkm : k ≤ m) {rho : ℝ} (hno : noDropWindow rho (contrastExcessAtScale hP hStruct k) (contrastExcessAtScale hP hStruct m)) (hrho_pos : 0 < rho) (hrho_le_one : rho ≤ 1) : terminalPAtScales hP hStruct k m ≤ 4 * √(1 + contrastExcessAtScale hP hStruct m)

Source label e.P.bound: on a no-drop window, the concrete terminal prefactor satisfies P_{k,m} <= 4 r_m.

theorem HCPolySupport.HighContrast.EntryScale.linearEdgeMemory_factor_le_four_of_le {H terminalP F_k F_m : ℝ} (hH_nonneg : 0 ≤ H) (hFm_nonneg : 0 ≤ F_m) (hFm_le_Fk : F_m ≤ F_k) (hP_le : terminalP ≤ 4 * √(1 + F_m)) : H / (1 + F_k) * terminalP ≤ 4 * H

Scalar KEY CHECK for the linear edge-memory channel (Layer B).

The linear residual factor terminalP / (1 + F_k) collapses to a bounded constant 4 whenever F_m ≤ F_k (contrast antitonicity on a window with k ≤ m), 0 ≤ F_m, and terminalP ≤ 4 √(1 + F_m): the 1 / (1 + F_k) denominator eats the √(1 + F_m) numerator down to at most 1, because √(1 + F_m) ≤ 1 + F_m ≤ 1 + F_k. Hence the H-linear residual (H / (1 + F_k)) · terminalP is at most 4 · H, with no leftover √(1 + F).

theorem HCPolySupport.HighContrast.EntryScale.linearEdgeMemory_terminalPAtScales_factor_le_four_of_noDrop_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) {k m : ℕ} (hkm : k ≤ m) {rho H : ℝ} (hno : noDropWindow rho (contrastExcessAtScale hP hStruct k) (contrastExcessAtScale hP hStruct m)) (hrho_pos : 0 < rho) (hrho_le_one : rho ≤ 1) (hH_nonneg : 0 ≤ H) : H / (1 + contrastExcessAtScale hP hStruct k) * terminalPAtScales hP hStruct k m ≤ 4 * H

Concrete KEY CHECK for the linear edge-memory channel (Layer B): on a no-drop window k = i-1, m = i with k ≤ m, the H-linear edge-memory residual factor terminalPAtScales / (1 + F_k) collapses so that (H / (1 + F_k)) · terminalPAtScales ≤ 4 · H. The terminalPAtScales factor is thus fully absorbable into an A·H (linear-memory) channel: it reduces to 4·H up to fixed no-drop constants, leaving no residual √(1+F).

theorem HCPolySupport.HighContrast.EntryScale.expectedResponseJCubeSet_special_le_two_mul_sqrt_contrastExcess_of_noDrop_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) {k m : ℕ} (hkm : k ≤ m) {rho : ℝ} (hno : noDropWindow rho (contrastExcessAtScale hP hStruct k) (contrastExcessAtScale hP hStruct m)) (hrho_pos : 0 < rho) (hrho_le_one : rho ≤ 1) (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) ≤ 2 * √(1 + contrastExcessAtScale hP hStruct m)

Source label e.sqrt.tau.absorb: on a no-drop window, the expected lower-scale response of the special terminal pair is at most 2 r_m.

theorem HCPolySupport.HighContrast.EntryScale.terminal_p_mul_tau_le_two_mul_drop {r_m P tau drop : ℝ} (hP_le : P ≤ 4 * r_m) (htau_nonneg : 0 ≤ tau) (hrt : r_m * tau ≤ 1 / 2 * drop) : P * tau ≤ 2 * drop

Source label e.tau.sum.absorb: scalar absorption step behind the weighted additivity-defect estimate.

theorem HCPolySupport.HighContrast.EntryScale.weighted_terminal_tau_absorb {ι : Type u_1} (s : Finset ι) {w tau drop : ι → ℝ} {r_m P rho F_m Cw : ℝ} (hP_le : P ≤ 4 * r_m) (hw_nonneg : ∀ i ∈ s, 0 ≤ w i) (htau_nonneg : ∀ i ∈ s, 0 ≤ tau i) (hrt : ∀ i ∈ s, r_m * tau i ≤ 1 / 2 * drop i) (hdrop : ∀ i ∈ s, drop i ≤ rho * F_m) (hCw : ∑ i ∈ s, w i ≤ Cw) (hrhoF_nonneg : 0 ≤ rho * F_m) : P * ∑ i ∈ s, w i * tau i ≤ 2 * Cw * (rho * F_m)

Source label e.tau.sum.absorb: finite weighted version of the no-drop additivity-defect absorption. The geometric estimate for the concrete weights is supplied later by the scale iteration.

theorem HCPolySupport.HighContrast.EntryScale.sqrt_tau_response_absorb {tau response B : ℝ} (htau_nonneg : 0 ≤ tau) (hresponse_nonneg : 0 ≤ response) (hB_nonneg : 0 ≤ B) (hprod : tau * response ≤ B ^ 2) : √tau * √response ≤ B

Source label e.sqrt.tau.absorb: square-root absorption once the product of the additivity defect and the lower-scale response has the required bound.

theorem HCPolySupport.HighContrast.EntryScale.sqrt_tau_response_absorb_delta {tau response C rho delta F_m : ℝ} (htau_nonneg : 0 ≤ tau) (hresponse_nonneg : 0 ≤ response) (hC_nonneg : 0 ≤ C) (hdelta_pos : 0 < delta) (hF_nonneg : 0 ≤ F_m) (hprod : tau * response ≤ (C * √rho * √delta⁻¹ * F_m) ^ 2) : √tau * √response ≤ C * √rho * √delta⁻¹ * F_m

Source label e.sqrt.tau.absorb: formula-facing version with the ρ^{1/2} δ^{-1/2} F_m scale.