Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.SpecialVectors

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

Special vectors for the third Section 5.3 lemma

This file contains the scalar algebra for the manuscript choices p_e = \widehat\sigma_m^{-1/2} e and q_e = \widehat\sigma_m^{1/2} e.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.expectedResponseJCubeSet_sub_half_vecDot_specialCentering_eq_expectedCenteredResponseJAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) : 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; have q0_e := q_e - hP.barSigmaAtScale hStruct ↑m • p_e; Ch04.expectedResponseJCubeSet P (originCube d ↑m) p_e q_e - 1 / 2 * vecDot p0_e q0_e = expectedCenteredResponseJAtScale hP hStruct (↑m) p_e q_e

The centered-response expectation is the raw response expectation with the manuscript scalar centering subtracted, specialized to the Section 5.3 special vectors.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.one_le_thetaAtScale_of_P4 {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : 1 ≤ thetaAtScale hP hStruct ↑m

Under (P4), the scalar condition number at every origin scale is at least one.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.expectedResponseJCubeSet_special_eq_sqrtTheta_sub_one_mul_vecNormSq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) : have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; Ch04.expectedResponseJCubeSet P (originCube d ↑m) p_e q_e = (√(thetaAtScale hP hStruct ↑m) - 1) * vecNormSq e

At the Section 5.3 special vectors, the raw annealed scalar response is the scalar gap sqrt(Theta_m) - 1, times the Euclidean square of the chosen direction.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.expectedResponseJCubeSet_special_le_thetaAtScale_sub_one_mul_vecNormSq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) : have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; Ch04.expectedResponseJCubeSet P (originCube d ↑m) p_e q_e ≤ (thetaAtScale hP hStruct ↑m - 1) * vecNormSq e

At the special vectors, the raw annealed scalar response is bounded by the condition-number excess, with the Euclidean square of the chosen direction.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.expectedResponseJCubeSet_special_le_thetaAtScale_sub_one_of_vecNormSq_eq_one {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) (he : vecNormSq e = 1) : have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; Ch04.expectedResponseJCubeSet P (originCube d ↑m) p_e q_e ≤ thetaAtScale hP hStruct ↑m - 1

Euclidean-unit specialization of expectedResponseJCubeSet_special_le_thetaAtScale_sub_one_mul_vecNormSq.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sigmaHatAtScale_mul_norm_specialPCentering_sq_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) (he : ‖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; sigmaHatAtScale hP hStruct ↑m * ‖p0_e‖ ^ 2 = (√(thetaAtScale hP hStruct ↑m) - 1) ^ 2

The manuscript special vector p_e has the exact centered size.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.sigmaHatAtScale_mul_vecNormSq_specialPCentering_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) : 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; sigmaHatAtScale hP hStruct ↑m * vecNormSq p0_e = (√(thetaAtScale hP hStruct ↑m) - 1) ^ 2 * vecNormSq e

Euclidean-squared form of the manuscript special-vector centered size for p_e. This is the robust form used by the coarse-fluctuation argument; the direction size is left explicit and can later be specialized by vecNormSq e = 1.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.inv_sigmaHatAtScale_mul_norm_specialQCentering_sq_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) (he : ‖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; (sigmaHatAtScale hP hStruct ↑m)⁻¹ * ‖q0_e‖ ^ 2 = (√(thetaAtScale hP hStruct ↑m) - 1) ^ 2

The manuscript special vector q_e has the exact centered size.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.inv_sigmaHatAtScale_mul_vecNormSq_specialQCentering_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) (e : Vec d) : 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; (sigmaHatAtScale hP hStruct ↑m)⁻¹ * vecNormSq q0_e = (√(thetaAtScale hP hStruct ↑m) - 1) ^ 2 * vecNormSq e

Euclidean-squared form of the manuscript special-vector centered size for q_e.