Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.CoarseAverages

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

Coarse-average terms in the third Section 5.3 lemma

This file starts the bridge from the high-scale average terms in WeakNormsMaximizer to the manuscript coarse block-matrix fluctuation. The first step is deterministic: on the a.e.-elliptic support, the Ch4 measurable scalar-response average over a cube agrees with the corresponding coarse-block formula from Chapter 2.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.scalarAnnealedBlockMatrixAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) : BlockMat d

Block diagonal annealed matrix with scalar conductivity and inverse dual conductivity at the given scale.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.reflectedBlockFluctuationOperatorNormSqAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (R : TriadicCube d) (a : RegCoeffField d) : ℝ

Squared Euclidean operator norm of the reflected coarse block matrix minus its reflected annealed matrix.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.starInvSqrtDiag {d : ℕ} (b c : ℝ) : BlockCoord d → ℝ

Diagonal weights for reflected normalization: square root of the dual conductivity on the first block and inverse square root of the conductivity on the second.

Equations

• HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.starInvSqrtDiag b c (Sum.inl val) = √c
• HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.starInvSqrtDiag b c (Sum.inr val) = (√b)⁻¹

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.starSqrtDiag {d : ℕ} (b c : ℝ) : BlockCoord d → ℝ

Reciprocal diagonal weights for reflected normalization: inverse square root of the dual conductivity on the first block and square root of the conductivity on the second.

Equations

• HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.starSqrtDiag b c (Sum.inl val) = (√c)⁻¹
• HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.starSqrtDiag b c (Sum.inr val) = √b

def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.blockCoordSwapEquiv (d : ℕ) : BlockCoord d ≃ BlockCoord d

Equivalence interchanging the two coordinate blocks and preserving the index within each block.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.fullBlockInvSqrtDiag {d : ℕ} (b c : ℝ) : BlockCoord d → ℝ

Diagonal weights for full block normalization: inverse square root of the conductivity on the first block and square root of the dual conductivity on the second.

Equations

• HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.fullBlockInvSqrtDiag b c (Sum.inl val) = (√b)⁻¹
• HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.fullBlockInvSqrtDiag b c (Sum.inr val) = √c

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.reflectedNormalizedBlockFluctuationOperatorNormSqAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (R : TriadicCube d) (a : RegCoeffField d) : ℝ

Squared Euclidean operator norm of the reflected fluctuation, multiplied on both sides by its diagonal normalization weights.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.fullBlockNormalizedFluctuationOperatorNormSqAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (m : ℤ) (R : TriadicCube d) (a : RegCoeffField d) : ℝ

Proof-internal manuscript normalized full-block fluctuation, using the Euclidean operator norm of the full block matrix. This is exposed inside the third-lemma proof namespace so the assembly file can state the variance term without introducing a public Ch5 wrapper.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.weighted_special_average_mismatch_le_fullBlockNormalized_fluctuation_mul_vecNormSq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (m : ℕ) (R : TriadicCube d) (e : Vec d) (hb : 0 < hP.barSigmaAtScale hStruct ↑m) (hc : 0 < hP.barSigmaStarAtScale hStruct ↑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; sigmaHatAtScale hP hStruct ↑m * vecNormSq (Ch04.canonicalScalarResponseGradientAverageCubeSet R R p_e q_e a.toFun - p0_e) + (sigmaHatAtScale hP hStruct ↑m)⁻¹ * vecNormSq (Ch04.canonicalScalarResponseFluxAverageCubeSet R R p_e q_e a.toFun - q0_e) ≤ 2 * thetaAtScale hP hStruct ↑m * fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) R a * vecNormSq e

Pointwise special-vector average mismatch controlled by the manuscript normalized full-block fluctuation, with the Euclidean size of the special direction left explicit. This is the robust internal form; the unit-vector corollary below is the one currently consumed by the high-scale assembly.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.weighted_special_average_mismatch_le_fullBlockNormalized_fluctuation {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (m : ℕ) (R : TriadicCube d) (e : Vec d) (hb : 0 < hP.barSigmaAtScale hStruct ↑m) (hc : 0 < hP.barSigmaStarAtScale hStruct ↑m) (he : vecNormSq 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; have q0_e := q_e - hP.barSigmaAtScale hStruct ↑m • p_e; sigmaHatAtScale hP hStruct ↑m * vecNormSq (Ch04.canonicalScalarResponseGradientAverageCubeSet R R p_e q_e a.toFun - p0_e) + (sigmaHatAtScale hP hStruct ↑m)⁻¹ * vecNormSq (Ch04.canonicalScalarResponseFluxAverageCubeSet R R p_e q_e a.toFun - q0_e) ≤ 2 * thetaAtScale hP hStruct ↑m * fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) R a

Pointwise special-vector average mismatch controlled by the manuscript normalized full-block fluctuation for Euclidean-unit directions. This remains a theorem in the coarse-fluctuation proof namespace, not a new public theorem package.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.weightedSpecialAverageMismatch_le_BlockFluctuation_mul_vectorNormSquared {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (m : ℕ) (Q : TriadicCube d) (j : ℕ) (e : Vec d) (hb : 0 < hP.barSigmaAtScale hStruct ↑m) (hc : 0 < hP.barSigmaStarAtScale hStruct ↑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; (descendantsAverage Q j fun (R : TriadicCube d) => sigmaHatAtScale hP hStruct ↑m * vecNormSq (Ch04.canonicalScalarResponseGradientAverageCubeSet R R p_e q_e a.toFun - p0_e) + (sigmaHatAtScale hP hStruct ↑m)⁻¹ * vecNormSq (Ch04.canonicalScalarResponseFluxAverageCubeSet R R p_e q_e a.toFun - q0_e)) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 2 * thetaAtScale hP hStruct ↑m * fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) R a * vecNormSq e

Descendant-averaged special-vector average mismatch controlled by the manuscript normalized full-block fluctuation, with the Euclidean direction size explicit.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.descendantsAverage_weighted_special_average_mismatch_le_fullBlockNormalized_fluctuation {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (m : ℕ) (Q : TriadicCube d) (j : ℕ) (e : Vec d) (hb : 0 < hP.barSigmaAtScale hStruct ↑m) (hc : 0 < hP.barSigmaStarAtScale hStruct ↑m) (he : vecNormSq 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; have q0_e := q_e - hP.barSigmaAtScale hStruct ↑m • p_e; (descendantsAverage Q j fun (R : TriadicCube d) => sigmaHatAtScale hP hStruct ↑m * vecNormSq (Ch04.canonicalScalarResponseGradientAverageCubeSet R R p_e q_e a.toFun - p0_e) + (sigmaHatAtScale hP hStruct ↑m)⁻¹ * vecNormSq (Ch04.canonicalScalarResponseFluxAverageCubeSet R R p_e q_e a.toFun - q0_e)) ≤ descendantsAverage Q j fun (R : TriadicCube d) => 2 * thetaAtScale hP hStruct ↑m * fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) R a

Descendant-averaged special-vector average mismatch controlled by the manuscript normalized full-block fluctuation.