Coarse-graining support: Support.Book.Ch05.Theorems.Section54.GoodScale.ScalarBounds #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Scalar bounds for the good-scale lemma #
This file supplies the (P4)-based scalar positivity, monotonicity, and
special-vector formula rewrites used by the good-scale parameter bounds.
Euclidean vector norm of a scalar multiple.
theorem
HCPolySupport.Book.Ch05.Section54.GoodScale.vecNormSq_eq_one_of_vecNorm_eq_one
{d : ℕ}
{e : Vec d}
(he : Ch02.vecNorm e = 1)
:
A Euclidean unit vector has squared project norm one.
theorem
HCPolySupport.Book.Ch05.Section54.GoodScale.sigmaHatAtScale_pos_of_P4
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(m : ℕ)
:
Under (P4), \widehat\sigma_m is strictly positive.
theorem
HCPolySupport.Book.Ch05.Section54.GoodScale.thetaAtScale_mono_of_P4
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
{n m : ℕ}
(hnm : n ≤ m)
:
Under (P4), the contrast is monotone along nonnegative scales.
theorem
HCPolySupport.Book.Ch05.Section54.GoodScale.one_le_thetaAtScale_of_P4
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(m : ℕ)
:
Under (P4), the scalar contrast is at least one.
theorem
HCPolySupport.Book.Ch05.Section54.GoodScale.scaled_specialP_centering_vecNorm_eq_of_P4
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(m : ℕ)
(e : Vec d)
(he : Ch02.vecNorm e = 1)
:
have p_e := specialPAtScale hP hStruct (↑m) e;
have q_e := specialQAtScale hP hStruct (↑m) e;
have p0_e := (hP.barSigmaStarAtScale hStruct ↑m)⁻¹ • q_e - p_e;
Ch02.vecNorm ((sigmaHatAtScale hP hStruct ↑m).rpow (1 / 2) • p0_e) = |√(thetaAtScale hP hStruct ↑m) - 1|
The scaled p_e centering has the manuscript norm.
theorem
HCPolySupport.Book.Ch05.Section54.GoodScale.scaled_specialQ_centering_vecNorm_eq_of_P4
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(m : ℕ)
(e : Vec d)
(he : Ch02.vecNorm e = 1)
:
have p_e := specialPAtScale hP hStruct (↑m) e;
have q_e := specialQAtScale hP hStruct (↑m) e;
have q0_e := q_e - hP.barSigmaAtScale hStruct ↑m • p_e;
Ch02.vecNorm ((sigmaHatAtScale hP hStruct ↑m).rpow (-(1 / 2)) • q0_e) = |√(thetaAtScale hP hStruct ↑m) - 1|
The scaled q_e centering has the manuscript norm.
theorem
HCPolySupport.Book.Ch05.Section54.GoodScale.expectedJScalarFormula_special_eq_of_P4
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(m k : ℕ)
(e : Vec d)
(he : vecNormSq e = 1)
:
have p_e := specialPAtScale hP hStruct (↑m) e;
have q_e := specialQAtScale hP hStruct (↑m) e;
expectedJScalarFormula hP hStruct (↑k) p_e q_e = 1 / 2 * (sigmaHatAtScale hP hStruct ↑m)⁻¹ * hP.barSigmaAtScale hStruct ↑k + 1 / 2 * sigmaHatAtScale hP hStruct ↑m * (hP.barSigmaStarAtScale hStruct ↑k)⁻¹ - 1
The special-vector scalar formula for the expected response.
theorem
HCPolySupport.Book.Ch05.Section54.GoodScale.tauScalarFormula_special_eq_of_P4
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
(m k : ℕ)
(e : Vec d)
(he : vecNormSq e = 1)
:
have p_e := specialPAtScale hP hStruct (↑m) e;
have q_e := specialQAtScale hP hStruct (↑m) e;
tauScalarFormula hP hStruct (↑m) (↑k) p_e q_e = 1 / 2 * (sigmaHatAtScale hP hStruct ↑m)⁻¹ * (hP.barSigmaAtScale hStruct ↑k - hP.barSigmaAtScale hStruct ↑m) + 1 / 2 * sigmaHatAtScale hP hStruct ↑m * ((hP.barSigmaStarAtScale hStruct ↑k)⁻¹ - (hP.barSigmaStarAtScale hStruct ↑m)⁻¹)
The special-vector scalar formula for the additivity defect.