Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundCoarseFluctuations.Assembly

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

Assembly for the coarse-fluctuation lemma

This file is the intended owner of the final proof of JUpperBoundCoarseFluctuations_homogenizationScale. The deterministic high-scale bridge is available from CoarseAverages.lean; the remaining assembly step needs a law-facing stationarity/integrability theorem for the normalized full-block operator-norm-square fluctuation observable.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.specialWeakNormManuscriptRHSAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (k m : ℕ) (e : Vec d) : ℝ

The RHS obtained by applying the first Section 5.3 lemma to the coarse-fluctuation special vectors, before the second and third Section 5.3 lemmas are used to rewrite it into manuscript coarse-fluctuation quantities.

Equations

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

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

Scalar weight multiplying the tau and low-scale tail terms in the final coarse-fluctuation RHS.

Equations

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

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

Weighted sum of normalized full-block operator-norm-square fluctuation expectations appearing in the final coarse-fluctuation RHS.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.coarseFluctuationTauSumAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (k m : ℕ) (e : Vec d) : ℝ

Weighted tau sum appearing in the final coarse-fluctuation RHS.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.coarseFluctuationUnitMomentWeightAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (m : ℕ) : ℝ

Unit-scale moment weight appearing in the final coarse-fluctuation RHS.

Equations

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

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

Response moment appearing in the positive-excess contribution of the final coarse-fluctuation RHS.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.coarseFluctuationManuscriptRHSAtScale {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (C ε : ℝ) (k m : ℕ) (e : Vec d) : ℝ

The six-term manuscript RHS from e.J.upper.bound.coarse.fluctuations.homogenization.scale.

This is the target RHS for the final third Section 5.3 lemma. The matrix fluctuation term uses the Euclidean operator norm via fullBlockNormalizedFluctuationOperatorNormSqAtScale.

Equations

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

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.expectedCenteredResponseJAtScale_le_specialWeakNormManuscriptRHSAtScale {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) (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 p_e := specialPAtScale hP hStruct (↑m) e; have q_e := specialQAtScale hP hStruct (↑m) e; expectedCenteredResponseJAtScale hP hStruct (↑m) p_e q_e ≤ specialWeakNormManuscriptRHSAtScale hP hStruct hP4 k m e

The first Section 5.3 lemma instantiated at the special vectors used in the coarse-fluctuation lemma. The two integrability hypotheses are exactly the finite-RHS side conditions intentionally left on JUpperBoundWeakNorms_homogenizationScale; this theorem does not introduce a new proof package.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundCoarseFluctuations.integral_weighted_descendantsAverage_fullBlockNormalizedFluctuationOperatorNormSqAtScale_eq {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) (k m : ℕ) : have β := section53CoarseFluctuationBeta hP4; have θ := thetaAtScale hP hStruct ↑m; have S := Finset.Icc (↑k + 1) ↑m; have w := fun (n : ℤ) => Real.rpow 3 (-β * ↑(↑m - n).toNat); ∫ (a : RegCoeffField d), ∑ n ∈ S, w n * descendantsAverage (originCube d ↑m) (↑m - n).toNat fun (R : TriadicCube d) => 2 * θ * fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) R a ∂P = ∑ n ∈ S, w n * (2 * θ * ∫ (a : RegCoeffField d), fullBlockNormalizedFluctuationOperatorNormSqAtScale hP hStruct (↑m) (originCube d n) a ∂P)

Expectation-level stationarity conversion for the weighted full-block fluctuation sum generated by the deterministic high-scale bridge.