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

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

Basic

Basic right-hand-side definitions for the first Section 5.3 lemma.

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffProductBridgeRHS {d : ℕ} (Q : TriadicCube d) (s : ℝ) (cutoffGradient : Vec d → Vec d) (fluxWeakOne fluxWeakS fluxAverage cutoffCircOne poincareConst cutoffConstant centeredCutoffConstant : ℝ) : ℝ

Private right-hand side for the cutoff-product estimate used in the first Section 5.3 lemma. This is just the active deterministic cutoff-product bound, renamed with the roles used in the manuscript proof.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffProductScaledWeakNormCoeff {d : ℕ} (Q : TriadicCube d) (s t B : ℝ) (cutoffGradient : Vec d → Vec d) : ℝ

Private coefficient in the manuscript product estimate after centering the potential and applying Ch01's legacy disjoint-Besov cutoff-product bound.

Equations

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