Coarse-graining support: Support.Book.Ch05.Theorems.Section54.OneStepContraction.GoodScaleInputs #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Good-scale inputs for the one-step contraction #
This file repackages the public good-scale parameter bounds into the exact pieces consumed by the one-step contraction proof.
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.goodScale_J_zero_le
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
{delta : ℝ}
(hdelta_pos : 0 < delta)
(hdelta_le : delta ≤ 1 / 2)
{m : ℕ}
(hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m)
(hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑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;
Ch04.annealedResponseJAtScale P 0 p_e q_e ≤ (1 + delta) * √(thetaAtScale hP hStruct 0)
At a good scale, the unit-scale annealed response for the special vectors
is controlled by sqrt(Theta_0).
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.goodScale_tau_le
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
{delta : ℝ}
(hdelta_pos : 0 < delta)
(hdelta_le : delta ≤ 1 / 2)
{m j : ℕ}
(hj : j ≤ m)
(hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m)
(hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑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;
tauAtScale P (↑m) (↑j) p_e q_e ≤ delta * √(thetaAtScale hP hStruct 0)
At a good scale, all lower-scale additivity defects for the special
vectors are controlled by delta * sqrt(Theta_0).
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.goodScale_sigmaHat_inv_barSigma_zero_le
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
{delta : ℝ}
(hdelta_pos : 0 < delta)
(hdelta_le : delta ≤ 1 / 2)
{m : ℕ}
(hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m)
(hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹)
(e : Vec d)
(he : Ch02.vecNorm e = 1)
:
(sigmaHatAtScale hP hStruct ↑m)⁻¹ * hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * √(thetaAtScale hP hStruct 0)
Good-scale upper scalar-chain comparison in the normalized variables.
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.goodScale_sigmaHat_barSigmaStar_zero_inv_le
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
{delta : ℝ}
(hdelta_pos : 0 < delta)
(hdelta_le : delta ≤ 1 / 2)
{m : ℕ}
(hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m)
(hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹)
(e : Vec d)
(he : Ch02.vecNorm e = 1)
:
sigmaHatAtScale hP hStruct ↑m * (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * √(thetaAtScale hP hStruct 0)
Good-scale lower scalar-chain comparison in the normalized variables.
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.goodScale_oneStepScalarWeight_le
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
{delta : ℝ}
(hdelta_pos : 0 < delta)
(hdelta_le : delta ≤ 1 / 2)
{m : ℕ}
(hgood_upper : hP.barSigmaAtScale hStruct 0 ≤ (1 + delta) * hP.barSigmaAtScale hStruct ↑m)
(hgood_lower : (hP.barSigmaStarAtScale hStruct 0)⁻¹ ≤ (1 + delta) * (hP.barSigmaStarAtScale hStruct ↑m)⁻¹)
(e : Vec d)
(he : Ch02.vecNorm e = 1)
:
The scalar weight multiplying the tau sum is bounded by a harmless
constant times sqrt(Theta_0) at a good scale.
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.one_le_thetaAtScale_zero_of_P4
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
:
At scale zero, (P4) implies Theta_0 >= 1.
theorem
HCPolySupport.Book.Ch05.Section54.OneStepContraction.sqrt_thetaAtScale_zero_le_thetaAtScale_zero_of_P4
{d : ℕ}
[NeZero d]
{P : Ch04.RestrictionCoeffLaw d}
(hP : Ch04.RestrictionLawCarrier P)
(hStruct : Ch04.RestrictionStructuralLaw P)
(hP4 : QuantitativeCoarseGrainedEllipticity P)
:
At scale zero, sqrt(Theta_0) <= Theta_0.