Coarse-graining support: Support.Book.Ch05.Theorems.Section53.JUpperBoundWeakNorms.Expectation.RHS

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

ExpectationRHS

Expected right-hand sides and nonnegativity facts.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.jUpperWeakNormPointwiseRHSAtScale {d : ℕ} (m k : ℤ) (s t : ℝ) (cutoffGradient : Vec d → Vec d) (C Cosc scaleSep BφS BφT cutoffCircOne poincareConst cutoffConstant centeredCutoffConstant : ℝ) (p q p0 q0 : Vec d) : RegCoeffField d → ℝ

Total Ch4-facing pointwise RHS for the first Section 5.3 lemma after the deterministic split has been assembled. The only non-total deterministic objects have been rewritten to Ch4 observables.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.jUpperWeakNormManuscriptPointwiseRHSAtScale {d : ℕ} (m k : ℤ) (s t C Cosc scaleSep BφS BφT Cprod : ℝ) (p q p0 q0 : Vec d) : RegCoeffField d → ℝ

Pointwise RHS with the cutoff-product term already in the manuscript Cauchy product form.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.jUpperWeakNormExpectedRHSAtScale {d : ℕ} (P : Ch04.RestrictionCoeffLaw d) (m k : ℤ) (s t : ℝ) (cutoffGradient : Vec d → Vec d) (C Cosc scaleSep BφS BφT cutoffCircOne poincareConst cutoffConstant centeredCutoffConstant : ℝ) (p q p0 q0 : Vec d) : ℝ

Expected right-hand side after the first stochastic assembly step for Lemma l.J.upper.bound.weak.norms.homogenization.scale. The square-root additivity term has been converted to sqrt tau * sqrt E[J_k]; the remaining weak-norm and cutoff-product terms are still written as expectations of the Ch4 scalar-response observables.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.jUpperWeakNormManuscriptExpectedRHSAtScale {d : ℕ} (P : Ch04.RestrictionCoeffLaw d) (m k : ℤ) (s t C Cosc scaleSep BφS BφT Cprod : ℝ) (p q p0 q0 : Vec d) : ℝ

Manuscript-facing expected RHS for Lemma l.J.upper.bound.weak.norms.homogenization.scale. Compared with jUpperWeakNormExpectedRHSAtScale, the cutoff-product bridge expectation has been replaced by the final Cauchy product of the note-normalized gradient and flux weak-norm square expectations.

Equations

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

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.childResponseJAverageOnDependentFamilyAtScale_eq_ch04 {d : ℕ} [NeZero d] (a : RegCoeffField d) (ha : Ch04.AELocallyUniformlyEllipticField a) (m k : ℤ) (p q : Vec d) : have F := Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha; childResponseJAverageOnFamilyAtDepth F (originCube d m) (m - k).toNat p q = descendantsAverage (originCube d m) (m - k).toNat fun (R : TriadicCube d) => Ch04.restrictionResponseJObservableCubeSet R p q a

At origin scales, the deterministic child response average for the Ch4 dependent family is the total Ch4 descendant response average.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.descendantsAverage_restrictionResponseJObservableCubeSet_nonneg {d : ℕ} (Q : TriadicCube d) (j : ℕ) (p q : Vec d) (a : RegCoeffField d) : 0 ≤ descendantsAverage Q j fun (R : TriadicCube d) => Ch04.restrictionResponseJObservableCubeSet R p q a

The total Ch4 descendant response average is pointwise nonnegative.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integrable_responseJAdditivityDefectAtScale {d : ℕ} {P : Ch04.RestrictionCoeffLaw d} {k m : ℤ} (hkm : k ≤ m) (p q : Vec d) (hParent : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet (originCube d m) p q) P) (hDesc : ∀ R ∈ descendantsAtScale (originCube d m) k, MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet R p q) P) : MeasureTheory.Integrable (responseJAdditivityDefectAtScale m k p q) P

The private additivity-defect observable is integrable when the parent and child response observables are integrable.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.responseJAdditivityDefectAtScale_nonneg_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) {k m : ℤ} (hkm : k ≤ m) (p q : Vec d) : 0 ≤ᵐ[P] responseJAdditivityDefectAtScale m k p q

The additivity-defect observable is nonnegative on the a.s. elliptic support of a Chapter 4 law carrier.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integral_sqrt_responseJAdditivityDefectAtScale_mul_sqrt_childResponseAverage_le {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) {k m : ℤ} (hk_nonneg : 0 ≤ k) (hkm : k ≤ m) (p q : Vec d) (hParent : MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet (originCube d m) p q) P) (hDesc : ∀ R ∈ descendantsAtScale (originCube d m) k, MeasureTheory.Integrable (Ch04.restrictionResponseJObservableCubeSet R p q) P) : ∫ (a : RegCoeffField d), √(responseJAdditivityDefectAtScale m k p q a) * √(descendantsAverage (originCube d m) (m - k).toNat fun (R : TriadicCube d) => Ch04.restrictionResponseJObservableCubeSet R p q a) ∂P ≤ √(tauAtScale P m k p q) * √(Ch04.expectedResponseJCubeSet P (originCube d k) p q)

The square-root additivity term is controlled in expectation by the geometric mean of the tau defect and the child-scale annealed response.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalScalarResponseGradientWeakNormCubeSet_nonneg_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (p q p0 : Vec d) : 0 ≤ᵐ[P] fun (a : RegCoeffField d) => Ch04.canonicalScalarResponseGradientWeakNormCubeSet Q s p q p0 a.toFun

A.e. nonnegativity of the Ch4 scalar-response gradient weak norm.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalScalarResponseFluxWeakNormCubeSet_nonneg_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (Q : TriadicCube d) {t : ℝ} (ht : 0 < t) (p q q0 : Vec d) : 0 ≤ᵐ[P] fun (a : RegCoeffField d) => Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q t p q q0 a.toFun

A.e. nonnegativity of the Ch4 scalar-response flux weak norm.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.scaledCanonicalScalarResponseGradientWeakNorm_nonneg_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (Q : TriadicCube d) {s : ℝ} (hs : 0 < s) (p q p0 : Vec d) : 0 ≤ᵐ[P] fun (a : RegCoeffField d) => cubeBesovScaleWeight (-s) Q * Ch04.canonicalScalarResponseGradientWeakNormCubeSet Q s p q p0 a.toFun

A.e. nonnegativity of a scaled Ch4 scalar-response gradient weak norm.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.scaledCanonicalScalarResponseFluxWeakNorm_nonneg_ae {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (Q : TriadicCube d) {t : ℝ} (ht : 0 < t) (p q q0 : Vec d) : 0 ≤ᵐ[P] fun (a : RegCoeffField d) => cubeBesovScaleWeight (-t) Q * Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q t p q q0 a.toFun

A.e. nonnegativity of a scaled Ch4 scalar-response flux weak norm.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.integral_cutoffProductBridgeRHS_le_weakNormSquareProduct {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (Q : TriadicCube d) {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (cutoffGradient : Vec d → Vec d) (cutoffCircOne poincareConst cutoffConstant centeredCutoffConstant Cprod : ℝ) (p q p0 q0 : Vec d) (hCprod : 0 ≤ Cprod) (hGradSq : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.canonicalScalarResponseGradientWeakNormCubeSet Q s p q p0 a.toFun ^ 2) P) (hFluxSq : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q t p q q0 a.toFun ^ 2) P) (hProductInt : MeasureTheory.Integrable (fun (a : RegCoeffField d) => cutoffProductBridgeRHS Q s cutoffGradient (Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q 1 p q q0 a.toFun) (Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q s p q q0 a.toFun) ‖Ch04.canonicalScalarResponseFluxAverageCubeSet Q Q p q a.toFun - q0‖ cutoffCircOne poincareConst cutoffConstant centeredCutoffConstant) P) (hProductPoint : ∀ᵐ (a : RegCoeffField d) ∂P, cutoffProductBridgeRHS Q s cutoffGradient (Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q 1 p q q0 a.toFun) (Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q s p q q0 a.toFun) ‖Ch04.canonicalScalarResponseFluxAverageCubeSet Q Q p q a.toFun - q0‖ cutoffCircOne poincareConst cutoffConstant centeredCutoffConstant ≤ Cprod * (Ch04.canonicalScalarResponseGradientWeakNormCubeSet Q s p q p0 a.toFun * Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q t p q q0 a.toFun)) : ∫ (a : RegCoeffField d), cutoffProductBridgeRHS Q s cutoffGradient (Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q 1 p q q0 a.toFun) (Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q s p q q0 a.toFun) ‖Ch04.canonicalScalarResponseFluxAverageCubeSet Q Q p q a.toFun - q0‖ cutoffCircOne poincareConst cutoffConstant centeredCutoffConstant ∂P ≤ Cprod * (√(∫ (a : RegCoeffField d), Ch04.canonicalScalarResponseGradientWeakNormCubeSet Q s p q p0 a.toFun ^ 2 ∂P) * √(∫ (a : RegCoeffField d), Ch04.canonicalScalarResponseFluxWeakNormCubeSet Q t p q q0 a.toFun ^ 2 ∂P))

Expectation of the cutoff-product bridge is bounded by the manuscript square-root product once the deterministic bridge has been pointwise replaced by the note-normalized gradient/flux weak-norm product.