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

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

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

Depth-weighted parent-localized weak-flux coefficient-energy base.

Equations

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

theorem HCPolySupport.weakFluxRHSWeightedCoefficientEnergyBase_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) {s : ℝ} (hs : 0 < s) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a u)) : 0 ≤ weakFluxRHSWeightedCoefficientEnergyBase Q a u s

The depth-weighted parent-localized weak-flux coefficient-energy base is nonnegative when the parent energy average is nonnegative.

theorem HCPolySupport.weakFluxRHSWeightedCoefficientEnergyBase_mul_inv_one_sub_step_le_noteEnergySquare {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) {s : ℝ} (hs : 0 < s) (hs_le : s ≤ 1) (havg_nonneg : 0 ≤ cubeAverage Q (coefficientEnergyDensity a u)) : weakFluxRHSWeightedCoefficientEnergyBase Q a u s * (1 - Real.rpow 3 (-s))⁻¹ ≤ 50 * s⁻¹ ^ 2 * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a u)

Note-constant square-envelope for the coefficient-energy part of the localized weak-flux RHS. This is the manuscript s^{-2} Lambda * energy piece before taking the final square root.

noncomputable def HCPolySupport.weakFluxRHSAbsorbedLocalizedNoteBase {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u g : Vec d → Vec d) (s : ℝ) (m : ℕ) (BU BV : ℝ) : ℝ

Note-eta specialization of the localized absorbed weak-flux component base.

Equations

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

theorem HCPolySupport.weakFluxRHSAbsorbedLocalizedNoteBase_mul_inv_one_sub_step_le_of_components {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u g : Vec d → Vec d) (s : ℝ) (m : ℕ) (BU BV Bcoeff Bu Bv Bforce : ℝ) (hcoeff : weakFluxRHSWeightedCoefficientEnergyBase Q a u s * (1 - Real.rpow 3 (-s))⁻¹ ≤ Bcoeff) (hu : coarsePoincareRHSNoteEta s * BU * (1 - Real.rpow 3 (-s))⁻¹ ≤ Bu) (hv : coarsePoincareRHSNoteEta s * BV * (1 - Real.rpow 3 (-s))⁻¹ ≤ 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))⁻¹ ≤ Bcoeff + Bu + Bv + Bforce

Componentwise upper-bound interface for the full note-eta localized base after multiplying by the weak-flux geometric tail.

theorem HCPolySupport.weakFluxRHSLocalCoefficientEnergyErrorAverage_le_parentHalfLambda_globalAverage {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) {s lam Lam : ℝ} (n : ℕ) (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum_half : Summable fun (m : ℕ) => geometricWeight (s / 2) 2 m * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑m) a).rpow 1) (havg_nonneg : ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (cubeSet Q) MeasureTheory.volume) : weakFluxRHSLocalCoefficientEnergyErrorAverage Q a u s n ≤ 2 * ((geometricDiscount s 2)⁻¹ * (Real.rpow 3 (s * ↑n) * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)) * cubeAverage Q (coefficientEnergyDensity a u)

Descendant-averaged coefficient-energy component localized to the parent half-scale upper multiscale coefficient and the parent energy average.

theorem HCPolySupport.weakFluxRHSDepthWeight_mul_coefficientEnergyErrorAverage_le_parentHalfLambda_globalAverage {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) {s lam Lam : ℝ} (n : ℕ) (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum_half : Summable fun (m : ℕ) => geometricWeight (s / 2) 2 m * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑m) a).rpow 1) (havg_nonneg : ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (cubeSet Q) MeasureTheory.volume) : coarsePoincareRHSDepthWeight s n * weakFluxRHSLocalCoefficientEnergyErrorAverage Q a u s n ≤ 2 * (geometricDiscount s 2)⁻¹ * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a * cubeAverage Q (coefficientEnergyDensity a u)

The depth weight cancels the half-scale coefficient growth in the averaged u coefficient-energy component.

theorem HCPolySupport.weakFluxRHSDepthWeight_mul_coefficientEnergyErrorAverage_le_weightedCoefficientEnergyBase {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) {s lam Lam : ℝ} (n : ℕ) (hs : 0 < s) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum_half : Summable fun (m : ℕ) => geometricWeight (s / 2) 2 m * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑m) a).rpow 1) (havg_nonneg : ∀ R ∈ descendantsAtDepth Q n, 0 ≤ cubeAverage R (coefficientEnergyDensity a u)) (hint : MeasureTheory.IntegrableOn (coefficientEnergyDensity a u) (cubeSet Q) MeasureTheory.volume) : coarsePoincareRHSDepthWeight s n * weakFluxRHSLocalCoefficientEnergyErrorAverage Q a u s n ≤ weakFluxRHSWeightedCoefficientEnergyBase Q a u s

The localized coefficient-energy average supplies the uniform component-base input needed by the weak-flux global wrappers.

theorem HCPolySupport.weakFluxRHSCorrectorEnergyErrorAverage_eq_components {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) (z : TriadicCube d → Vec d → Vec d) (s : ℝ) (n : ℕ) : weakFluxRHSCorrectorEnergyErrorAverage Q a u z s n = weakFluxRHSLocalCoefficientEnergyErrorAverage Q a u s n + weakFluxRHSLocalCorrectorEnergyErrorAverage Q a z s n

Averaging preserves the corrector-energy component split.

theorem HCPolySupport.weakFluxRHSAbsorbedErrorAverage_eq_components {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g u : Vec d → Vec d) (v : TriadicCube d → Vec d → Vec d) (s η : ℝ) (n : ℕ) : weakFluxRHSAbsorbedErrorAverage Q a g u v s η n = weakFluxRHSLocalCoefficientEnergyErrorAverage Q a u s n + weakFluxRHSLocalUSeminormErrorAverage Q u s η n + weakFluxRHSLocalHarmonicSeminormErrorAverage Q v s η n + weakFluxRHSLocalForceErrorAverage Q a g s η n

Averaging preserves the absorbed component split.

theorem HCPolySupport.weakFluxRHSCorrectorEnergyErrorAverage_weighted_le_add_of_components {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) (z : TriadicCube d → Vec d → Vec d) (s : ℝ) (n : ℕ) {Bcoeff Bcorr : ℝ} (hcoeff : coarsePoincareRHSDepthWeight s n * weakFluxRHSLocalCoefficientEnergyErrorAverage Q a u s n ≤ Bcoeff) (hcorr : coarsePoincareRHSDepthWeight s n * weakFluxRHSLocalCorrectorEnergyErrorAverage Q a z s n ≤ Bcorr) : (coarsePoincareRHSDepthWeight s n * descendantsAverage Q n fun (R : TriadicCube d) => weakFluxRHSCorrectorEnergyLocalError R a u (z R) s) ≤ Bcoeff + Bcorr

Weighted component bounds imply a weighted bound for the corrector-energy local-error envelope.

theorem HCPolySupport.weakFluxRHSAbsorbedErrorAverage_weighted_le_add_of_components {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g u : Vec d → Vec d) (v : TriadicCube d → Vec d → Vec d) (s η : ℝ) (n : ℕ) {Bcoeff Bu Bv Bforce : ℝ} (hcoeff : coarsePoincareRHSDepthWeight s n * weakFluxRHSLocalCoefficientEnergyErrorAverage Q a u s n ≤ Bcoeff) (hu : coarsePoincareRHSDepthWeight s n * weakFluxRHSLocalUSeminormErrorAverage Q u s η n ≤ Bu) (hv : coarsePoincareRHSDepthWeight s n * weakFluxRHSLocalHarmonicSeminormErrorAverage Q v s η n ≤ Bv) (hforce : coarsePoincareRHSDepthWeight s n * weakFluxRHSLocalForceErrorAverage Q a g s η n ≤ Bforce) : (coarsePoincareRHSDepthWeight s n * descendantsAverage Q n fun (R : TriadicCube d) => weakFluxRHSAbsorbedLocalError R a g u (v R) s η) ≤ Bcoeff + Bu + Bv + Bforce

Weighted component bounds imply a weighted bound for the absorbed local-error envelope.