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

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

Basic definitions for the weak-norm maximizer lemma

Named right-hand-side terms for manuscript Lemma l.weak.norms.maximizer.homogenization.scale.

noncomputable def HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.gradientAverageTermAtScale {d : ℕ} (m k : ℤ) (s : ℝ) (p q p0 : Vec d) (a : RegCoeffField d) : ℝ

The high-scale averaged-gradient term in the weak-norm maximizer estimate.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.fluxAverageTermAtScale {d : ℕ} (m k : ℤ) (t : ℝ) (p q q0 : Vec d) (a : RegCoeffField d) : ℝ

The high-scale averaged-flux term in the weak-norm maximizer estimate.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.responseDefectAverageAtScale {d : ℕ} (m n : ℤ) (p q : Vec d) (a : RegCoeffField d) : ℝ

The parent-child response defect at a child scale.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.gradientMismatchTermAtScale {d : ℕ} (m k : ℤ) (s s' : ℝ) (p q : Vec d) (a : RegCoeffField d) : ℝ

The high-scale gradient mismatch term controlled by the lower ellipticity quantity on the parent cube. The dimensional constant is inserted by the final RHS.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.fluxMismatchTermAtScale {d : ℕ} (m k : ℤ) (t t' : ℝ) (p q : Vec d) (a : RegCoeffField d) : ℝ

The high-scale flux mismatch term controlled by the upper ellipticity quantity on the parent cube. The dimensional constant is inserted by the final RHS.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.gradientLowScaleTailAtScale {d : ℕ} (m k : ℤ) (s s' : ℝ) (p q : Vec d) (a : RegCoeffField d) : ℝ

The low-scale gradient tail in the weak-norm maximizer estimate.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.fluxLowScaleTailAtScale {d : ℕ} (m k : ℤ) (t t' : ℝ) (p q : Vec d) (a : RegCoeffField d) : ℝ

The low-scale flux tail in the weak-norm maximizer estimate.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.gradientConstantTailAtScale {d : ℕ} (m k : ℤ) (s : ℝ) (p0 : Vec d) : ℝ

The affine-gradient constant tail in the gradient weak-norm estimate.

Equations

• HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.gradientConstantTailAtScale m k s p0 = s⁻¹ * Real.rpow 3 (-s * ↑(m - k).toNat) * ‖p0‖

noncomputable def HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.fluxConstantTailAtScale {d : ℕ} (m k : ℤ) (t : ℝ) (q0 : Vec d) : ℝ

The affine-flux constant tail in the flux weak-norm estimate.

Equations

• HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.fluxConstantTailAtScale m k t q0 = t⁻¹ * Real.rpow 3 (-t * ↑(m - k).toNat) * ‖q0‖

noncomputable def HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.gradientRHSAtScale {d : ℕ} (C : ℝ) (m k : ℤ) (s s' : ℝ) (p q p0 : Vec d) (a : RegCoeffField d) : ℝ

Manuscript right-hand side for the gradient estimate in l.weak.norms.maximizer.homogenization.scale.

Equations

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

noncomputable def HCPolySupport.Book.Ch05.Section53.WeakNormsMaximizer.fluxRHSAtScale {d : ℕ} (C : ℝ) (m k : ℤ) (t t' : ℝ) (p q q0 : Vec d) (a : RegCoeffField d) : ℝ

Manuscript right-hand side for the flux estimate in l.weak.norms.maximizer.homogenization.scale.

Equations

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