Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.Constants

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

noncomputable def HCPolySupport.coarsePoincareRHSLocalCoeff {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) : ℝ

Coefficient prefactor in the local absorbed RHS error.

Equations

• HCPolySupport.coarsePoincareRHSLocalCoeff Q a s = (HCPolySupport.geometricDiscount s 2)⁻¹ * (HCPolySupport.lambdaSq Q s (HCPolySupport.MultiscaleExponent.finite 2) a)⁻¹

noncomputable def HCPolySupport.coarsePoincareRHSIntrinsicLocalEnergyError {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) (s : ℝ) : ℝ

Intrinsic local energy piece in the absorbed RHS error.

Equations

• HCPolySupport.coarsePoincareRHSIntrinsicLocalEnergyError Q a u s = 2 * HCPolySupport.coarsePoincareRHSLocalCoeff Q a s * HCPolySupport.cubeAverage Q (HCPolySupport.coefficientEnergyDensity a u)

noncomputable def HCPolySupport.coarsePoincareRHSIntrinsicLocalForceMultiplier {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) : ℝ

Intrinsic local forcing multiplier in the absorbed RHS error.

The uniform ellipticity lower bound is intentionally absent: quantitative dependence runs through lambdaSq, while IsEllipticFieldOn only supplies well-posedness and nonnegativity hypotheses.

Equations

• HCPolySupport.coarsePoincareRHSIntrinsicLocalForceMultiplier Q a s = HCPolySupport.coarsePoincareRHSLocalCoeff Q a s * (↑d * (3 ^ (↑d + s) * √2))

noncomputable def HCPolySupport.coarsePoincareRHSLocalCenteredForceSeminorm {d : ℕ} (Q : TriadicCube d) (g : Vec d → Vec d) (s : ℝ) : ℝ

Centered local forcing seminorm in the absorbed RHS error.

Equations

• HCPolySupport.coarsePoincareRHSLocalCenteredForceSeminorm Q g s = HCPolySupport.cubeBesovPositiveVectorSeminormTwo Q s fun (x : HCPolySupport.Vec d) => g x - HCPolySupport.cubeAverageVec Q g

noncomputable def HCPolySupport.coarsePoincareRHSGlobalForceBound {d : ℕ} (Q : TriadicCube d) (g : Vec d → Vec d) (s : ℝ) (n : ℕ) : ℝ

The global positive-Besov forcing bound localized to descendants of depth n.

Equations

• HCPolySupport.coarsePoincareRHSGlobalForceBound Q g s n = (Real.rpow 3 (s * ↑n) ^ 2)⁻¹ * HCPolySupport.cubeBesovPositiveVectorSeminormTwo Q s g ^ 2

noncomputable def HCPolySupport.coarsePoincareRHSIntrinsicLocalForceError {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s : ℝ) : ℝ

Intrinsic local forcing piece in the absorbed RHS error.

Equations

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

noncomputable def HCPolySupport.coarsePoincareRHSIntrinsicAbsorbedLocalError {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g u : Vec d → Vec d) (s η : ℝ) : ℝ

Intrinsic local non-child error produced by the absorbed RHS one-cube recurrence.

Equations

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

noncomputable def HCPolySupport.coarsePoincareRHSParentHalfCoeff {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (n : ℕ) : ℝ

Parent half-scale coefficient used after localizing lambda_{s,2}^{-1}.

Equations

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

noncomputable def HCPolySupport.coarsePoincareRHSIntrinsicParentHalfForceMultiplier {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (n : ℕ) : ℝ

Intrinsic parent half-scale forcing multiplier used after localizing lambda_{s,2}^{-1}.

Equations

• HCPolySupport.coarsePoincareRHSIntrinsicParentHalfForceMultiplier Q a s n = HCPolySupport.coarsePoincareRHSParentHalfCoeff Q a s n * (↑d * (3 ^ (↑d + s) * √2))

noncomputable def HCPolySupport.coarsePoincareRHSAbsorbedEnergyCoeff (η : ℝ) : ℝ

Coefficient of the local energy average after expanding the absorbed error.

Equations

• HCPolySupport.coarsePoincareRHSAbsorbedEnergyCoeff η = 1 + η * (1 - η)⁻¹

noncomputable def HCPolySupport.coarsePoincareRHSAbsorbedRnCoeff (η : ℝ) : ℝ

Coefficient of the current R_n term after expanding the absorbed error.

Equations

• HCPolySupport.coarsePoincareRHSAbsorbedRnCoeff η = η + η ^ 2 * (1 - η)⁻¹

noncomputable def HCPolySupport.coarsePoincareRHSAbsorbedForceCoeff (η : ℝ) : ℝ

Coefficient of the local forcing average after expanding the absorbed error.

Equations

• HCPolySupport.coarsePoincareRHSAbsorbedForceCoeff η = 2 * η * (1 - η)⁻¹ * η⁻¹ + 2 * η⁻¹

noncomputable def HCPolySupport.coarsePoincareRHSNoteEta (s : ℝ) : ℝ

Absorption parameter that makes the scaled recurrence use the note-step ratio exactly.

Equations

• HCPolySupport.coarsePoincareRHSNoteEta s = (1 - Real.rpow 3 (-s / 2)) / (2 - Real.rpow 3 (-s / 2))

noncomputable def HCPolySupport.coarsePoincareRHSNoteEnergyEnvelope (s : ℝ) : ℝ

Exact energy envelope after inserting coarsePoincareRHSNoteEta.

Equations

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

noncomputable def HCPolySupport.coarsePoincareRHSNoteForceEnvelope (s : ℝ) : ℝ

Exact forcing envelope after inserting coarsePoincareRHSNoteEta.

Equations

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

noncomputable def HCPolySupport.coarsePoincareRHSDiscount (s : ℝ) : ℝ

The fixed one-step discount in the current natural-depth R_n recurrence.

Equations

• HCPolySupport.coarsePoincareRHSDiscount s = Real.rpow 3 (-2 * s)

noncomputable def HCPolySupport.coarsePoincareRHSStepDiscount (s : ℝ) : ℝ

The one-step discount after the note-style scaling from R_n to S_n.

Equations

• HCPolySupport.coarsePoincareRHSStepDiscount s = Real.rpow 3 (-s)

noncomputable def HCPolySupport.coarsePoincareRHSScaledStepCoeff (s θ : ℝ) : ℝ

Abstract one-step coefficient after passing from R_n to the scaled S_n.

Equations

• HCPolySupport.coarsePoincareRHSScaledStepCoeff s θ = θ * Real.rpow 3 s

noncomputable def HCPolySupport.coarsePoincareRHSNoteStepCoeff (s : ℝ) : ℝ

The note-facing one-step coefficient 3^{-3s/2} for the R_n recurrence.

Equations

• HCPolySupport.coarsePoincareRHSNoteStepCoeff s = Real.rpow 3 (-(3 * s / 2))

noncomputable def HCPolySupport.coarsePoincareRHSFiniteSumRatio (s θ : ℝ) : ℝ

Ratio governing the localized energy coefficient sums after inserting parent q = 2 bounds.

Equations

• HCPolySupport.coarsePoincareRHSFiniteSumRatio s θ = HCPolySupport.coarsePoincareRHSScaledStepCoeff s θ

noncomputable def HCPolySupport.coarsePoincareRHSForceFiniteSumRatio (s θ : ℝ) : ℝ

Ratio governing the localized force coefficient sums after inserting parent q = 2 bounds.

Equations

• HCPolySupport.coarsePoincareRHSForceFiniteSumRatio s θ = HCPolySupport.coarsePoincareRHSScaledStepCoeff s θ * Real.rpow 3 (-s)