Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.RHSConversion

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

RHS conversion for the coarse-fluctuation lemma

This file is proof-internal to the third Section 5.3 lemma. It owns the scalar/nonnegativity bookkeeping and the expectation-level conversion from the first-lemma weak-norm RHS to the manuscript coarse-fluctuation RHS.

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

Nonnegativity of the scalar ellipticity weight in the final RHS.

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

The scalar weight in the coarse-fluctuation RHS is uniformly bounded below. This is just AM-GM applied to \widehat\sigma_m \bar\sigma_{*,0}^{-1} and \widehat\sigma_m^{-1} \bar\sigma_0, whose product is Theta_0 ≥ 1.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.coarseFluctuationFullBlockSumAtScale_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (k m : ℕ) : 0 ≤ coarseFluctuationFullBlockSumAtScale hP hStruct hP4 k m

Nonnegativity of the full-block fluctuation sum. The fluctuation term is the squared Euclidean operator norm (Matrix.toEuclideanCLM), not a Frobenius norm.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.coarseFluctuationTauSumAtScale_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (k m : ℕ) (e : Vec d) : 0 ≤ coarseFluctuationTauSumAtScale hP hStruct hP4 k m e

Nonnegativity of the tau sum in the final RHS.

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

Nonnegativity of the unit-scale ellipticity moment weight.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.coarseFluctuationResponseMomentAtScale_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (k m : ℕ) (e : Vec d) : 0 ≤ coarseFluctuationResponseMomentAtScale hP hStruct hP4 k m e

Nonnegativity of the response moment term.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integral_paired_highScaleAverageTerms_special_le_fullBlockSumAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k m : ℕ} (_hkm : k < m) (e : Vec d) (he : vecNormSq e = 1) : have β := section53CoarseFluctuationBeta hP4; have s := hP4.sLower + 2 * β; have t := hP4.sUpper + 2 * β; 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; have σ := sigmaHatAtScale hP hStruct ↑m; have S := Finset.Icc (↑k + 1) ↑m; have w := fun (n : ℤ) => Real.rpow 3 (-β * ↑(↑m - n).toNat); MeasureTheory.Integrable (fun (a : RegCoeffField d) => σ * WeakNormsMaximizer.gradientAverageTermAtScale (↑m) (↑k) s p_e q_e p0_e a ^ 2 + σ⁻¹ * WeakNormsMaximizer.fluxAverageTermAtScale (↑m) (↑k) t p_e q_e q0_e a ^ 2) P ∧ ∫ (a : RegCoeffField d), σ * WeakNormsMaximizer.gradientAverageTermAtScale (↑m) (↑k) s p_e q_e p0_e a ^ 2 + σ⁻¹ * WeakNormsMaximizer.fluxAverageTermAtScale (↑m) (↑k) t p_e q_e q0_e a ^ 2 ∂P ≤ (∑ n ∈ S, w n) * (2 * thetaAtScale hP hStruct ↑m * coarseFluctuationFullBlockSumAtScale hP hStruct hP4 k m)

Expectation-level conversion for the paired high-scale average terms in the weak-norm maximizer RHS. This is the full-block fluctuation part of the paired square estimate; the fluctuation observable is the squared Euclidean operator norm (Matrix.toEuclideanCLM), not a Frobenius norm.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integral_paired_highScaleAverageTerms_special_le_beta_inv_fullBlockSumAtScale {d : ℕ} [NeZero d] : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P), Ch04.RestrictionStationaryLaw P → ∀ (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k m : ℕ}, k < m → ∀ (e : Vec d), vecNormSq e = 1 → have β := section53CoarseFluctuationBeta hP4; have s := hP4.sLower + 2 * β; have t := hP4.sUpper + 2 * β; 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; have σ := sigmaHatAtScale hP hStruct ↑m; ∫ (a : RegCoeffField d), σ * WeakNormsMaximizer.gradientAverageTermAtScale (↑m) (↑k) s p_e q_e p0_e a ^ 2 + σ⁻¹ * WeakNormsMaximizer.fluxAverageTermAtScale (↑m) (↑k) t p_e q_e q0_e a ^ 2 ∂P ≤ C * β⁻¹ * thetaAtScale hP hStruct ↑m * coarseFluctuationFullBlockSumAtScale hP hStruct hP4 k m

The paired high-scale average part of the weak-norm maximizer RHS has the manuscript beta^{-1} * theta * full-block fluctuation form. The fluctuation observable is the squared Euclidean operator norm (Matrix.toEuclideanCLM), not a Frobenius norm.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integral_sq_beta_weighted_sqrt_responseDefectAverageAtScale_special_le_tauSum {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k m : ℕ} (hkm : k < m) (e : Vec d) : have β := section53CoarseFluctuationBeta hP4; have p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; ∫ (a : RegCoeffField d), (∑ n ∈ Finset.Icc (↑k + 1) ↑m, Real.rpow 3 (-β * ↑(↑m - n).toNat) * √(WeakNormsMaximizer.responseDefectAverageAtScale (↑m) n p_e q_e a)) ^ 2 ∂P ≤ 5 * β⁻¹ * coarseFluctuationTauSumAtScale hP hStruct hP4 k m e

The beta-weighted response-defect square-root sum at the Section 5.3 special vectors is controlled by the manuscript weighted tau sum. All response integrability inputs are discharged from (P4) and the Ch4 law-facing integrability surface.