Coarse-graining support: Support.Deterministic.WeakFluxRHS.AbsorbedNoteConstants

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

theorem HCPolySupport.coarsePoincareRHSNoteEta_le_one {s : ℝ} (hs : 0 < s) : coarsePoincareRHSNoteEta s ≤ 1

theorem HCPolySupport.coarsePoincareRHSNoteEta_inv_le_ten_inv {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) : (coarsePoincareRHSNoteEta s)⁻¹ ≤ 10 * s⁻¹

Reciprocal bound for the note absorption parameter used by the weak-flux forcing component.

theorem HCPolySupport.weakFluxRHSNoteEtaComponent_mul_inv_one_sub_step_le_five_inv_mul {s B : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (hB_nonneg : 0 ≤ B) : coarsePoincareRHSNoteEta s * B * (1 - Real.rpow 3 (-s))⁻¹ ≤ 5 * s⁻¹ * B

The note-eta scalar seminorm component is bounded by the weak-flux geometric-tail constant.

theorem HCPolySupport.weakFluxRHSAbsorbedLocalizedNoteBase_mul_inv_one_sub_step_le_noteEnergySeminorms_of_force {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u g : Vec d → Vec d) {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (m : ℕ) {BU BV Bforce : ℝ} (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a u)) (hBU_nonneg : 0 ≤ BU) (hBV_nonneg : 0 ≤ BV) (hforce : weakFluxRHSWeightedGlobalForceBase Q a g s (coarsePoincareRHSNoteEta s) m * (1 - Real.rpow 3 (-s))⁻¹ ≤ Bforce) : weakFluxRHSAbsorbedLocalizedNoteBase Q a u g s m BU BV * (1 - Real.rpow 3 (-s))⁻¹ ≤ 50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a u) + 5 * s⁻¹ * BU + 5 * s⁻¹ * BV + Bforce

Note-constant expansion of the localized weak-flux base with the forcing component left as a separately supplied bound.

theorem HCPolySupport.weakFluxRHSWeightedGlobalForceBase_noteEta_zero_mul_inv_one_sub_step_le_noteForceSquare {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) : weakFluxRHSWeightedGlobalForceBase Q a g s (coarsePoincareRHSNoteEta s) 0 * (1 - Real.rpow 3 (-s))⁻¹ ≤ 2500 * s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2

Note-constant square-envelope for the weighted global forcing component at the parent depth.

theorem HCPolySupport.weakFluxRHSWeightedGlobalForceBase_noteEta_mul_inv_one_sub_step_le_noteForceSquare {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (m : ℕ) : weakFluxRHSWeightedGlobalForceBase Q a g s (coarsePoincareRHSNoteEta s) m * (1 - Real.rpow 3 (-s))⁻¹ ≤ 2500 * s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2

Note-constant square-envelope for the weighted global forcing component at any descendant depth.

theorem HCPolySupport.weakFluxRHSAbsorbedLocalizedNoteBase_mul_inv_one_sub_step_le_noteEnergySeminormsForce {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u g : Vec d → Vec d) {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (m : ℕ) {BU BV : ℝ} (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a u)) (hBU_nonneg : 0 ≤ BU) (hBV_nonneg : 0 ≤ BV) : weakFluxRHSAbsorbedLocalizedNoteBase Q a u g s m BU BV * (1 - Real.rpow 3 (-s))⁻¹ ≤ 50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a u) + 5 * s⁻¹ * BU + 5 * s⁻¹ * BV + 2500 * s⁻¹ ^ 4 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a ^ 2 * (↑d * (3 ^ (↑d + s) * √2)) ^ 2 * cubeBesovPositiveVectorSeminormTwo Q s g ^ 2

Fully expanded note-constant bound for the localized weak-flux base, with the u and harmonic-remainder tails left as caller-supplied square bounds.