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

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

theorem HCPolySupport.HighContrast.EntryScale.abs_sub_one_le_mul_sub_one_of_one_le {a b : ℝ} (ha : 1 ≤ a) (hb : 1 ≤ b) : |a - 1| ≤ a * b - 1 ∧ |b - 1| ≤ a * b - 1

Source label e.drift.general: if both scalar ratios are at least one, then each diagonal drift entry is bounded by the product excess a b - 1.

noncomputable def HCPolySupport.HighContrast.EntryScale.fullBlockOperatorNorm {d : ℕ} (A : FullBlockMat d) : ℝ

Euclidean/L2 operator norm of a full block matrix. This is the matrix norm used by the full Ahom_m^{-1/2} (...) Ahom_m^{-1/2} observable in source label l.union.bound.

Equations

• HCPolySupport.HighContrast.EntryScale.fullBlockOperatorNorm A = ‖Matrix.toEuclideanCLM A‖

theorem HCPolySupport.HighContrast.EntryScale.fullBlockOperatorNorm_eq_l2_opNorm {d : ℕ} (A : FullBlockMat d) : fullBlockOperatorNorm A = ‖A‖

theorem HCPolySupport.HighContrast.EntryScale.fullBlockOperatorNorm_nonneg {d : ℕ} (A : FullBlockMat d) : 0 ≤ fullBlockOperatorNorm A

theorem HCPolySupport.HighContrast.EntryScale.fullBlockOperatorNorm_mul_le {d : ℕ} (A B : FullBlockMat d) : fullBlockOperatorNorm (A * B) ≤ fullBlockOperatorNorm A * fullBlockOperatorNorm B

theorem HCPolySupport.HighContrast.EntryScale.fullBlockOperatorNorm_add_sq_le_two_mul_add {d : ℕ} (A B : FullBlockMat d) : fullBlockOperatorNorm (A + B) ^ 2 ≤ 2 * fullBlockOperatorNorm A ^ 2 + 2 * fullBlockOperatorNorm B ^ 2

Source label l.S.and.J: squared triangle inequality for the full-block operator norm, in the form used to split A(cu_j) - Ahom_m = (A(cu_j) - Ahom_j) + (Ahom_j - Ahom_m).

theorem HCPolySupport.HighContrast.EntryScale.fullBlockOperatorNorm_diagonal {d : ℕ} (v : BlockCoord d → ℝ) : fullBlockOperatorNorm (Matrix.diagonal v) = ‖v‖

theorem HCPolySupport.HighContrast.EntryScale.fullBlockOperatorNorm_diagonal_le_of_forall_norm_le {d : ℕ} {v : BlockCoord d → ℝ} {R : ℝ} (hR : 0 ≤ R) (hv : ∀ (α : BlockCoord d), ‖v α‖ ≤ R) : fullBlockOperatorNorm (Matrix.diagonal v) ≤ R

theorem HCPolySupport.HighContrast.EntryScale.fullBlockOperatorNorm_diagonal_le_of_forall_abs_le {d : ℕ} {v : BlockCoord d → ℝ} {R : ℝ} (hR : 0 ≤ R) (hv : ∀ (α : BlockCoord d), |v α| ≤ R) : fullBlockOperatorNorm (Matrix.diagonal v) ≤ R

theorem HCPolySupport.HighContrast.EntryScale.fullBlockOperatorNorm_two_sided_mul_le {d : ℕ} (L X R : FullBlockMat d) {CL CR : ℝ} (hCL_nonneg : 0 ≤ CL) (hL : fullBlockOperatorNorm L ≤ CL) (hR : fullBlockOperatorNorm R ≤ CR) : fullBlockOperatorNorm (L * X * R) ≤ CL * CR * fullBlockOperatorNorm X

Source label l.union.bound: full-block operator-norm bridge for changing both sides of the terminal normalization. Once the two diagonal change matrices have norm bounds, this converts them into the corresponding bound for the full centered block observable.

noncomputable def HCPolySupport.HighContrast.EntryScale.terminalNormalizerChangeDiag {d : ℕ} (upperRatio invStarRatio : ℝ) : BlockCoord d → ℝ

Source label l.union.bound: diagonal entries of the full-block terminal/intermediate normalization-change matrix, written in terms of the two scalar ratios barSigma_j / barSigma_m and barSigmaStar_j^{-1} / barSigmaStar_m^{-1}.

Equations

• HCPolySupport.HighContrast.EntryScale.terminalNormalizerChangeDiag upperRatio invStarRatio (Sum.inl val) = √upperRatio
• HCPolySupport.HighContrast.EntryScale.terminalNormalizerChangeDiag upperRatio invStarRatio (Sum.inr val) = √invStarRatio

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

Source label l.union.bound: concrete diagonal entries of Ahom_m^{-1/2} Ahom_j^{1/2} in the scalar-block coordinates.

Equations

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

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

Source label l.union.bound: concrete full-block diagonal matrix for Ahom_m^{-1/2} Ahom_j^{1/2}.

Equations

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

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

Source label l.union.bound: the library's scalar full-block normalizer at one scale, as the diagonal matrix Ahom_n^{-1/2}.

Equations

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

noncomputable def HCPolySupport.HighContrast.EntryScale.scalarCenteredFullBlockMatrixAtScale {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (center : ℕ) (Y : FullBlockMat d) : FullBlockMat d

Source label l.union.bound: full-block matrix centered by the scalar annealed block at scale center.

Equations

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

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

Source label e.drift.general: diagonal entries of the terminal-normalized annealed drift Ahom_m^{-1/2} (Ahom_j - Ahom_m) Ahom_m^{-1/2}.

Equations

• HCPolySupport.HighContrast.EntryScale.terminalAnnealedFullBlockDriftDiagAtScales hP hStruct j m (Sum.inl val) = hP.barSigmaAtScale hStruct ↑j / hP.barSigmaAtScale hStruct ↑m - 1
• HCPolySupport.HighContrast.EntryScale.terminalAnnealedFullBlockDriftDiagAtScales hP hStruct j m (Sum.inr val) = (hP.barSigmaStarAtScale hStruct ↑j)⁻¹ / (hP.barSigmaStarAtScale hStruct ↑m)⁻¹ - 1

theorem HCPolySupport.HighContrast.EntryScale.terminalAnnealedFullBlockDriftMatrix_eq_diagonal {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 : ℕ) : scalarFullBlockNormalizerMatrixAtScale hP hStruct m * (toFullBlockMat (Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct ↑j) - toFullBlockMat (Book.Ch04.scalarAnnealedBlockMatrixAtScale hP hStruct ↑m)) * scalarFullBlockNormalizerMatrixAtScale hP hStruct m = Matrix.diagonal (terminalAnnealedFullBlockDriftDiagAtScales hP hStruct j m)

Source label e.drift.general: the deterministic annealed-drift matrix is exactly diagonal after terminal scalar normalization.

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

Source label e.drift.general: deterministic annealed-drift norm D_{j,m} from the source proof.

Equations

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

theorem HCPolySupport.HighContrast.EntryScale.terminalAnnealedFullBlockDriftAtScales_nonneg {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} (hP : Book.Ch04.RestrictionLawCarrier P) (hStruct : Book.Ch04.RestrictionStructuralLaw P) (j m : ℕ) : 0 ≤ terminalAnnealedFullBlockDriftAtScales hP hStruct j m

Source label e.drift.general: D_{j,m} is nonnegative.

theorem HCPolySupport.HighContrast.EntryScale.terminalAnnealedFullBlockDriftAtScales_le_of_diag_bounds {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 : ℕ) {R : ℝ} (hR : 0 ≤ R) (hdiag : ∀ (α : BlockCoord d), |terminalAnnealedFullBlockDriftDiagAtScales hP hStruct j m α| ≤ R) : terminalAnnealedFullBlockDriftAtScales hP hStruct j m ≤ R

Source label e.drift.general: bound D_{j,m} by uniform bounds on the two scalar diagonal entries.

theorem HCPolySupport.HighContrast.EntryScale.terminalAnnealedFullBlockDriftAtScales_le_of_scalar_ratio_bounds {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 : ℕ) {R : ℝ} (hR : 0 ≤ R) (hupper : |hP.barSigmaAtScale hStruct ↑j / hP.barSigmaAtScale hStruct ↑m - 1| ≤ R) (hlower : |(hP.barSigmaStarAtScale hStruct ↑j)⁻¹ / (hP.barSigmaStarAtScale hStruct ↑m)⁻¹ - 1| ≤ R) : terminalAnnealedFullBlockDriftAtScales hP hStruct j m ≤ R

Source label e.drift.general: source-facing scalar-ratio form of the pointwise deterministic drift bound.

theorem HCPolySupport.HighContrast.EntryScale.terminalAnnealedFullBlockDriftAtScales_le_scalar_ratio_product_sub_one {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 : ℕ) (hupper_one : 1 ≤ hP.barSigmaAtScale hStruct ↑j / hP.barSigmaAtScale hStruct ↑m) (hlower_one : 1 ≤ (hP.barSigmaStarAtScale hStruct ↑j)⁻¹ / (hP.barSigmaStarAtScale hStruct ↑m)⁻¹) : terminalAnnealedFullBlockDriftAtScales hP hStruct j m ≤ hP.barSigmaAtScale hStruct ↑j / hP.barSigmaAtScale hStruct ↑m * ((hP.barSigmaStarAtScale hStruct ↑j)⁻¹ / (hP.barSigmaStarAtScale hStruct ↑m)⁻¹) - 1

Source label e.drift.general: the pointwise deterministic drift is bounded by the product excess of the two scalar terminal ratios.

theorem HCPolySupport.HighContrast.EntryScale.terminalAnnealedFullBlockDriftAtScales_le_scalar_ratio_product_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) {j m : ℕ} (hjm : j ≤ m) : terminalAnnealedFullBlockDriftAtScales hP hStruct j m ≤ hP.barSigmaAtScale hStruct ↑j / hP.barSigmaAtScale hStruct ↑m * ((hP.barSigmaStarAtScale hStruct ↑j)⁻¹ / (hP.barSigmaStarAtScale hStruct ↑m)⁻¹) - 1

Source label e.drift.general: under (P4) and j <= m, the scalar-chain monotonicity supplies the hypotheses for the product-excess drift bound.

theorem HCPolySupport.HighContrast.EntryScale.terminalAnnealedFullBlockDriftAtScales_le_contrastExcess_drop_div_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) : terminalAnnealedFullBlockDriftAtScales hP hStruct j m ≤ (contrastExcessAtScale hP hStruct j - contrastExcessAtScale hP hStruct m) / (1 + contrastExcessAtScale hP hStruct m)

Source label e.drift.general: library-facing pointwise drift bound in the paper's scalar excess notation F_n = Theta_n - 1.

theorem HCPolySupport.HighContrast.EntryScale.contrastExcess_drop_le_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) {rho : ℝ} {k j m : ℕ} (hno : noDropWindow rho (contrastExcessAtScale hP hStruct k) (contrastExcessAtScale hP hStruct m)) (hkj : k ≤ j) : contrastExcessAtScale hP hStruct j - contrastExcessAtScale hP hStruct m ≤ rho * contrastExcessAtScale hP hStruct m

Source label e.tau.sum.absorb: on a no-drop window [k,m], every intermediate contrast drop is bounded by the endpoint no-drop budget.

theorem HCPolySupport.HighContrast.EntryScale.terminalAnnealedFullBlockDriftAtScales_le_noDrop_contrastExcess_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) {rho : ℝ} {k j m : ℕ} (hno : noDropWindow rho (contrastExcessAtScale hP hStruct k) (contrastExcessAtScale hP hStruct m)) (hkj : k ≤ j) (hjm : j ≤ m) : terminalAnnealedFullBlockDriftAtScales hP hStruct j m ≤ rho * contrastExcessAtScale hP hStruct m / (1 + contrastExcessAtScale hP hStruct m)

Source label e.drift.general: on a no-drop window, the pointwise drift bound becomes the paper's no-drop form with F_m = Theta_m - 1.

theorem HCPolySupport.HighContrast.EntryScale.terminalNormalizerChangeMatrixAtScales_mul_scalarFullBlockNormalizerMatrixAtScale_eq {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 : ℕ) : terminalNormalizerChangeMatrixAtScales hP hStruct j m * scalarFullBlockNormalizerMatrixAtScale hP hStruct j = scalarFullBlockNormalizerMatrixAtScale hP hStruct m

theorem HCPolySupport.HighContrast.EntryScale.scalarFullBlockNormalizerMatrixAtScale_mul_terminalNormalizerChangeMatrixAtScales_eq {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 : ℕ) : scalarFullBlockNormalizerMatrixAtScale hP hStruct j * terminalNormalizerChangeMatrixAtScales hP hStruct j m = scalarFullBlockNormalizerMatrixAtScale hP hStruct m

theorem HCPolySupport.HighContrast.EntryScale.fullBlockOperatorNorm_terminalNormalizerChangeDiag_le_sqrt_of_bounds {d : ℕ} {upperRatio invStarRatio T : ℝ} (hupper : upperRatio ≤ T) (hinvStar : invStarRatio ≤ T) : fullBlockOperatorNorm (Matrix.diagonal (terminalNormalizerChangeDiag upperRatio invStarRatio)) ≤ √T

theorem HCPolySupport.HighContrast.EntryScale.terminalNormalizer_operatorNorm_le_sqrt_widetildeTheta {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) : fullBlockOperatorNorm (terminalNormalizerChangeMatrixAtScales hP hStruct j m) ≤ √(Book.Ch05.widetildeThetaAtScale P 0 hP4)

Source label l.union.bound: the concrete terminal/intermediate diagonal normalization-change matrix has full-block operator norm at most sqrt widetildeTheta_0.

theorem HCPolySupport.HighContrast.EntryScale.fullBlockOperatorNorm_terminalNormalizerChange_two_sided_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) (X : FullBlockMat d) : fullBlockOperatorNorm (terminalNormalizerChangeMatrixAtScales hP hStruct j m * X * terminalNormalizerChangeMatrixAtScales hP hStruct j m) ≤ Book.Ch05.widetildeThetaAtScale P 0 hP4 * fullBlockOperatorNorm X

Source label l.union.bound: changing both sides of a full-block observable from intermediate scale j to terminal scale m costs at most the corrected initial contrast budget T = widetildeTheta_0.

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

Source label l.union.bound: terminal normalization of a block centered at scale j costs at most T = widetildeTheta_0 times the same centered block with its intermediate-scale normalization.