Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.PairedWeakNormSquares

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

Paired weak-norm square conversion

This proof-internal file converts the actual paired weak-norm square expectations from the first Section 5.3 lemma into the coarse-fluctuation manuscript terms. The component expectation estimates live in the preceding files; this file owns the final square algebra.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.paired_constantTail_special_le_lowScaleTail {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier 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 θ := thetaAtScale hP hStruct ↑m; σ * WeakNormsMaximizer.gradientConstantTailAtScale (↑m) (↑k) s p0_e ^ 2 + σ⁻¹ * WeakNormsMaximizer.fluxConstantTailAtScale (↑m) (↑k) t q0_e ^ 2 ≤ 2 * ((β ^ 2)⁻¹ * Real.rpow 3 (-2 * β * ↑(m - k)) * coarseFluctuationScalarWeightAtScale hP hStruct m * (θ - 1))

The constant affine tails in the weak-norm maximizer RHS are absorbed by the low-scale scalar tail of the final manuscript RHS.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.paired_weakNormSquares_special_le_componentIntegrals {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) (hGradSq : have β := section53CoarseFluctuationBeta hP4; have s := hP4.sLower + 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; MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.canonicalScalarResponseGradientWeakNormCubeSet (originCube d ↑m) s p_e q_e p0_e a.toFun ^ 2) P) (hFluxSq : have β := section53CoarseFluctuationBeta hP4; have t := hP4.sUpper + 2 * β; 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; MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.canonicalScalarResponseFluxWeakNormCubeSet (originCube d ↑m) t p_e q_e q0_e a.toFun ^ 2) P) : have β := section53CoarseFluctuationBeta hP4; have s := hP4.sLower + 2 * β; have s' := hP4.sLower + β; have t := hP4.sUpper + 2 * β; have t' := hP4.sUpper + β; have Q := originCube d ↑m; 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 K := WeakNormsMaximizer.section53WeakNormMaximizerConst d; have gradWeak := Ch04.canonicalScalarResponseGradientWeakNormCubeSet Q s p_e q_e p0_e; have fluxWeak := Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q t p_e q_e q0_e; σ * ∫ (a : RegCoeffField d), gradWeak a.toFun ^ 2 ∂P + σ⁻¹ * ∫ (a : RegCoeffField d), fluxWeak a.toFun ^ 2 ∂P ≤ 16 * (∫ (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 + K ^ 2 * ∫ (a : RegCoeffField d), σ * WeakNormsMaximizer.gradientMismatchTermAtScale (↑m) (↑k) s s' p_e q_e a ^ 2 + σ⁻¹ * WeakNormsMaximizer.fluxMismatchTermAtScale (↑m) (↑k) t t' p_e q_e a ^ 2 ∂P + K ^ 2 * ∫ (a : RegCoeffField d), σ * WeakNormsMaximizer.gradientLowScaleTailAtScale (↑m) (↑k) s s' p_e q_e a ^ 2 + σ⁻¹ * WeakNormsMaximizer.fluxLowScaleTailAtScale (↑m) (↑k) t t' p_e q_e a ^ 2 ∂P + K ^ 2 * (σ * WeakNormsMaximizer.gradientConstantTailAtScale (↑m) (↑k) s p0_e ^ 2 + σ⁻¹ * WeakNormsMaximizer.fluxConstantTailAtScale (↑m) (↑k) t q0_e ^ 2))

The paired special-vector weak-norm square expectation is bounded by the four component square expectations coming from the weak-norm maximizer RHS. This is the expectation-level square algebra; later lemmas convert the component integrals into the manuscript coarse-fluctuation terms.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.paired_weakNormSquares_special_le_coarseFluctuationTerms {d : ℕ} [NeZero d] (params : QuantitativeCoarseGrainedEllipticityParams d) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P), Ch04.RestrictionStationaryLaw P → ∀ (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P), hP4.params = params → ∀ {k m : ℕ}, k < m → ∀ (e : Vec d), vecNormSq e = 1 → (have β := section53CoarseFluctuationBeta hP4; have s := hP4.sLower + 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; MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.canonicalScalarResponseGradientWeakNormCubeSet (originCube d ↑m) s p_e q_e p0_e a.toFun ^ 2) P) → (have β := section53CoarseFluctuationBeta hP4; have t := hP4.sUpper + 2 * β; 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; MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.canonicalScalarResponseFluxWeakNormCubeSet (originCube d ↑m) t p_e q_e q0_e a.toFun ^ 2) P) → have β := section53CoarseFluctuationBeta hP4; have s := hP4.sLower + 2 * β; have t := hP4.sUpper + 2 * β; have Q := originCube d ↑m; 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 θ := thetaAtScale hP hStruct ↑m; have gradWeak := Ch04.canonicalScalarResponseGradientWeakNormCubeSet Q s p_e q_e p0_e; have fluxWeak := Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q t p_e q_e q0_e; σ * ∫ (a : RegCoeffField d), gradWeak a.toFun ^ 2 ∂P + σ⁻¹ * ∫ (a : RegCoeffField d), fluxWeak a.toFun ^ 2 ∂P ≤ C * (β⁻¹ * θ * coarseFluctuationFullBlockSumAtScale hP hStruct hP4 k m + (β ^ 2)⁻¹ * coarseFluctuationScalarWeightAtScale hP hStruct m * coarseFluctuationTauSumAtScale hP hStruct hP4 k m e + ↑hP4.xi * (β ^ 3)⁻¹ * Real.rpow 3 (-β * ↑m) * coarseFluctuationUnitMomentWeightAtScale hP hStruct hP4 m * coarseFluctuationResponseMomentAtScale hP hStruct hP4 k m e + (β ^ 2)⁻¹ * Real.rpow 3 (-2 * β * ↑(m - k)) * coarseFluctuationScalarWeightAtScale hP hStruct m * (θ - 1))

The paired special-vector weak-norm square expectations are bounded by the four square-conversion terms of the manuscript coarse-fluctuation RHS.