Coarse-graining support:

Support.Book.Ch05.Theorems.Section53.JUpperBoundWeakNorms.Expectation.YoungRHS

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

YoungRHS

An alternative expectation surface for the first Section 5.3 lemma. The standard manuscript RHS collapses the additivity term by Cauchy in probability, giving sqrt tau * sqrt E[J_k]. For the flatness-rules route we keep the estimate base-free by applying Young to that scalar product, producing eta * E[J_k] + eta^{-1} * tau instead.

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

Manuscript expected RHS with the first square-root additivity term replaced by its Young envelope.

Equations

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

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.jUpperWeakNormManuscriptExpectedRHSAtScale_le_youngManuscriptExpectedRHSAtScale {d : ℕ} {P : Ch04.RestrictionCoeffLaw d} {m k : ℤ} {s t C Cosc scaleSep BφS BφT Cprod η : ℝ} (p q p0 q0 : Vec d) (hC : 0 ≤ C) (hη : 0 < η) (htau : 0 ≤ tauAtScale P m k p q) (hresponse : 0 ≤ Ch04.expectedResponseJCubeSet P (originCube d k) p q) : jUpperWeakNormManuscriptExpectedRHSAtScale P m k s t C Cosc scaleSep BφS BφT Cprod p q p0 q0 ≤ jUpperWeakNormYoungManuscriptExpectedRHSAtScale P m k s t C Cosc scaleSep BφS BφT Cprod η p q p0 q0

The standard manuscript RHS is bounded by the Young-envelope RHS for the first additivity term.

theorem HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.expectedResponseJCubeSet_sub_half_dot_le_jUpperWeakNormYoungExpectedRHS {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hstat : Ch04.RestrictionStationaryLaw P) (hStruct : Ch04.RestrictionStructuralLaw P) (hP4 : QuantitativeCoarseGrainedEllipticity P) {k m : ℤ} (hk_nonneg : 0 ≤ k) (hkm : k ≤ m) {s t : ℝ} (hs : 0 < s) (hs_lt_one : s < 1) (ht : 0 < t) (hst : s + t ≤ 1) (p q p0 q0 : Vec d) {η : ℝ} (hη : 0 < η) (hGradSq : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.canonicalScalarResponseGradientWeakNormCubeSet (originCube d m) s p q p0 a.toFun ^ 2) P) (hFluxSq : MeasureTheory.Integrable (fun (a : RegCoeffField d) => Ch04.canonicalScalarResponseFluxWeakNormCubeSet (originCube d m) t p q q0 a.toFun ^ 2) P) : have Q := originCube d m; have j := (m - k).toNat; Ch04.expectedResponseJCubeSet P Q p q - 1 / 2 * vecDot p0 q0 ≤ jUpperWeakNormYoungManuscriptExpectedRHSAtScale P m k s t (1 + section53CutoffBound Q) (section53CutoffOscillationConstant Q) (section53CutoffScaleSep Q j) (section53CutoffDualBound Q s) (section53CutoffDualBound Q t) (section53CutoffProductCoeff Q s t) η p q p0 q0

First Section 5.3 lemma with the Young-envelope additivity term, using the same normalized cutoff and P4 integrability inputs as the standard public surface.