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

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

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

Explicit non-child error envelope in the absorbed weak-flux RHS recurrence.

This is the local Section 3.2.3 error produced after absorbing the short corrector product into the u, harmonic-remainder, and centered-forcing quadratic terms.

Equations

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

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

Explicit non-child error envelope in the corrector-energy weak-flux RHS recurrence, before the corrector energy is converted into Besov forcing terms.

Equations

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

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

Local coefficient multiplying the weak-flux RHS error terms.

Equations

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

theorem HCPolySupport.weakFluxRHSLocalCoeff_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {s : ℝ} (hs : 0 < s) : 0 ≤ weakFluxRHSLocalCoeff Q a s

The weak-flux local coefficient is nonnegative for positive regularity.

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

Parent half-scale coefficient used after localizing Lambda_{s,2}.

Equations

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

theorem HCPolySupport.weakFluxRHSParentHalfCoeff_succ {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (n : ℕ) : weakFluxRHSParentHalfCoeff Q a s (n + 1) = Real.rpow 3 s * weakFluxRHSParentHalfCoeff Q a s n

Parent half-scale weak-flux coefficient grows by 3^s when the descendant depth is incremented.

theorem HCPolySupport.weakFluxRHSLocalCoeff_le_parentHalfLambda_of_mem_descendantsAtDepth {d : ℕ} [NeZero d] {Q R : TriadicCube d} (a : CoeffField d) {n : ℕ} {s lam Lam : ℝ} (hs : 0 < s) (hR : R ∈ descendantsAtDepth Q n) (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) : weakFluxRHSLocalCoeff R a s ≤ (geometricDiscount s 2)⁻¹ * (Real.rpow 3 (s * ↑n) * LambdaSq Q (s / 2) (MultiscaleExponent.finite 2) a)

Half-scale localization of the local coefficient multiplying the weak-flux RHS error terms.

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

Parent half-scale forcing multiplier used after localizing Lambda_{s,2}.

Equations

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

theorem HCPolySupport.weakFluxRHSParentHalfForceMultiplier_succ {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (n : ℕ) : weakFluxRHSParentHalfForceMultiplier Q a s (n + 1) = Real.rpow 3 s * weakFluxRHSParentHalfForceMultiplier Q a s n

Parent half-scale weak-flux forcing multiplier grows by 3^s when the descendant depth is incremented.

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

The geometric multiplier attached to the centered forcing seminorm in the absorbed weak-flux RHS error.

Equations

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

theorem HCPolySupport.weakFluxRHSLocalForceMultiplier_sq_le_of_localCoeffBound {d : ℕ} (R : TriadicCube d) (a : CoeffField d) {s C : ℝ} (hs : 0 < s) (hcoeff : weakFluxRHSLocalCoeff R a s ≤ C) : weakFluxRHSLocalForceMultiplier R a s ^ 2 ≤ (C * (↑d * (3 ^ (↑d + s) * √2))) ^ 2

Local forcing multipliers are controlled by any upper bound on the local weak-flux coefficient.

theorem HCPolySupport.weakFluxRHSLocalForceMultiplier_sq_le_parentHalfLambda_of_mem_descendantsAtDepth {d : ℕ} [NeZero d] {Q R : TriadicCube d} (a : CoeffField d) {s lam Lam : ℝ} (n : ℕ) (hs : 0 < s) (hR : R ∈ descendantsAtDepth Q n) (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) : weakFluxRHSLocalForceMultiplier R a s ^ 2 ≤ weakFluxRHSParentHalfForceMultiplier Q a s n ^ 2

Half-scale localization of the weak-flux forcing multiplier on descendants.

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

Centered positive Besov forcing seminorm used by the absorbed weak-flux RHS error.

Equations

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

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

The u coefficient-energy contribution to the local weak-flux RHS error.

Equations

• HCPolySupport.weakFluxRHSLocalCoefficientEnergyError Q a u s = 2 * HCPolySupport.weakFluxRHSLocalCoeff Q a s * HCPolySupport.cubeAverage Q (HCPolySupport.coefficientEnergyDensity a u)

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

The corrector coefficient-energy contribution to the local weak-flux RHS error.

Equations

• HCPolySupport.weakFluxRHSLocalCorrectorEnergyError Q a z s = 2 * HCPolySupport.weakFluxRHSLocalCoeff Q a s * HCPolySupport.cubeAverage Q (HCPolySupport.coefficientEnergyDensity a z)

noncomputable def HCPolySupport.weakFluxRHSLocalUSeminormError {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (s η : ℝ) : ℝ

The absorbed u negative-Besov contribution to the local weak-flux RHS error.

Equations

• HCPolySupport.weakFluxRHSLocalUSeminormError Q u s η = η * HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q s u ^ 2

noncomputable def HCPolySupport.weakFluxRHSLocalHarmonicSeminormError {d : ℕ} (Q : TriadicCube d) (v : Vec d → Vec d) (s η : ℝ) : ℝ

The absorbed harmonic-remainder negative-Besov contribution to the local weak-flux RHS error.

Equations

• HCPolySupport.weakFluxRHSLocalHarmonicSeminormError Q v s η = η * HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q s v ^ 2

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

The absorbed centered-forcing contribution to the local weak-flux RHS error.

Equations

• HCPolySupport.weakFluxRHSLocalForceError Q a g s η = 2 * η⁻¹ * (HCPolySupport.weakFluxRHSLocalForceMultiplier Q a s * HCPolySupport.weakFluxRHSLocalCenteredForceSeminorm Q g s) ^ 2

theorem HCPolySupport.weakFluxRHSCorrectorEnergyLocalError_eq_components {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u z : Vec d → Vec d) (s : ℝ) : weakFluxRHSCorrectorEnergyLocalError Q a u z s = weakFluxRHSLocalCoefficientEnergyError Q a u s + weakFluxRHSLocalCorrectorEnergyError Q a z s

The corrector-energy local weak-flux RHS error is exactly the sum of its two coefficient-energy components.

theorem HCPolySupport.weakFluxRHSAbsorbedLocalError_eq_components {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g u v : Vec d → Vec d) (s η : ℝ) : weakFluxRHSAbsorbedLocalError Q a g u v s η = weakFluxRHSLocalCoefficientEnergyError Q a u s + weakFluxRHSLocalUSeminormError Q u s η + weakFluxRHSLocalHarmonicSeminormError Q v s η + weakFluxRHSLocalForceError Q a g s η

The absorbed local weak-flux RHS error is exactly the sum of its named coefficient-energy, absorbed seminorm, and centered-forcing components.

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

Descendant average of the corrector-energy weak-flux RHS error.

Equations

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

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

Descendant average of the absorbed weak-flux RHS error.

Equations

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

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

Descendant average of the u coefficient-energy component.

Equations

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

noncomputable def HCPolySupport.weakFluxRHSLocalCorrectorEnergyErrorAverage {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (z : TriadicCube d → Vec d → Vec d) (s : ℝ) (n : ℕ) : ℝ

Descendant average of the corrector coefficient-energy component.

Equations

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

noncomputable def HCPolySupport.weakFluxRHSLocalUSeminormErrorAverage {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (s η : ℝ) (n : ℕ) : ℝ

Descendant average of the absorbed u negative-Besov component.

Equations

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

noncomputable def HCPolySupport.weakFluxRHSLocalHarmonicSeminormErrorAverage {d : ℕ} (Q : TriadicCube d) (v : TriadicCube d → Vec d → Vec d) (s η : ℝ) (n : ℕ) : ℝ

Descendant average of the absorbed harmonic-remainder negative-Besov component.

Equations

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

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

Averaged negative-Besov size of a depth-dependent harmonic remainder.

Equations

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

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

Scaled averaged negative-Besov size of a depth-dependent harmonic remainder.

Equations

• HCPolySupport.weakFluxRHSHarmonicRemainderScaledAveragedSeminormSq Q s v n = HCPolySupport.coarsePoincareRHSDepthWeight s n * HCPolySupport.weakFluxRHSHarmonicRemainderAveragedSeminormSq Q s v n

theorem HCPolySupport.weakFluxRHSHarmonicRemainderAveragedSeminormSq_le_of_descendant_sq_bound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (v : TriadicCube d → Vec d → Vec d) (n : ℕ) {B : ℝ} (hbound : ∀ R ∈ descendantsAtDepth Q n, cubeBesovNegativeVectorSeminormTwo R s (v R) ^ 2 ≤ B) : weakFluxRHSHarmonicRemainderAveragedSeminormSq Q s v n ≤ B

Descendantwise squared bounds control the averaged varying-cube harmonic remainder size.

theorem HCPolySupport.weakFluxRHSHarmonicRemainderScaledAveragedSeminormSq_le_of_descendant_scaled_sq_bound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (v : TriadicCube d → Vec d → Vec d) (n : ℕ) {B : ℝ} (hbound : ∀ R ∈ descendantsAtDepth Q n, cubeBesovNegativeVectorSeminormTwo R s (v R) ^ 2 ≤ (coarsePoincareRHSDepthWeight s n)⁻¹ * B) : weakFluxRHSHarmonicRemainderScaledAveragedSeminormSq Q s v n ≤ B

Descendantwise squared bounds at the reciprocal depth-weight scale control the scaled varying-cube harmonic remainder size.

theorem HCPolySupport.weakFluxRHSHarmonicRemainderScaledAveragedSeminormSq_tail_le_of_descendant_scaled_sq_bound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (v : TriadicCube d → Vec d → Vec d) (m : ℕ) {B : ℝ} (hbound : ∀ (k : ℕ), ∀ R ∈ descendantsAtDepth Q (m + k), cubeBesovNegativeVectorSeminormTwo R s (v R) ^ 2 ≤ (coarsePoincareRHSDepthWeight s (m + k))⁻¹ * B) (k : ℕ) : weakFluxRHSHarmonicRemainderScaledAveragedSeminormSq Q s v (m + k) ≤ B

Tail form of weakFluxRHSHarmonicRemainderScaledAveragedSeminormSq_le_of_descendant_scaled_sq_bound.

theorem HCPolySupport.weakFluxRHSLocalUSeminormErrorAverage_eq_eta_mul_coarsePoincareRHSRn {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (s η : ℝ) (n : ℕ) : weakFluxRHSLocalUSeminormErrorAverage Q u s η n = η * coarsePoincareRHSRn Q s u n

The averaged absorbed u seminorm component is exactly η R_n.

theorem HCPolySupport.weakFluxRHSDepthWeight_mul_uSeminormErrorAverage_eq_eta_mul_coarsePoincareRHSSn {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (s η : ℝ) (n : ℕ) : coarsePoincareRHSDepthWeight s n * weakFluxRHSLocalUSeminormErrorAverage Q u s η n = η * coarsePoincareRHSSn Q s u n

The depth-weighted absorbed u seminorm component is exactly η S_n.

theorem HCPolySupport.weakFluxRHSLocalHarmonicSeminormErrorAverage_eq_eta_mul_harmonicRemainder {d : ℕ} (Q : TriadicCube d) (v : TriadicCube d → Vec d → Vec d) (s η : ℝ) (n : ℕ) : weakFluxRHSLocalHarmonicSeminormErrorAverage Q v s η n = η * weakFluxRHSHarmonicRemainderAveragedSeminormSq Q s v n

The averaged absorbed harmonic-remainder seminorm component is exactly η times its varying-cube averaged seminorm.

theorem HCPolySupport.weakFluxRHSDepthWeight_mul_harmonicSeminormErrorAverage_eq_eta_mul_harmonicRemainderScaled {d : ℕ} (Q : TriadicCube d) (v : TriadicCube d → Vec d → Vec d) (s η : ℝ) (n : ℕ) : coarsePoincareRHSDepthWeight s n * weakFluxRHSLocalHarmonicSeminormErrorAverage Q v s η n = η * weakFluxRHSHarmonicRemainderScaledAveragedSeminormSq Q s v n

The depth-weighted absorbed harmonic-remainder seminorm component is exactly η times its scaled varying-cube averaged seminorm.

theorem HCPolySupport.weakFluxRHSDepthWeight_mul_uSeminormErrorAverage_le_eta_mul_base {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (s : ℝ) {η B : ℝ} (n : ℕ) (hη_nonneg : 0 ≤ η) (hbase : coarsePoincareRHSSn Q s u n ≤ B) : coarsePoincareRHSDepthWeight s n * weakFluxRHSLocalUSeminormErrorAverage Q u s η n ≤ η * B

Any bound on S_n gives the corresponding weighted absorbed u component bound after multiplying by η.

theorem HCPolySupport.weakFluxRHSDepthWeight_mul_uSeminormErrorAverage_le_eta_mul_base_of_tail {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (s : ℝ) {η B : ℝ} (m k : ℕ) (hη_nonneg : 0 ≤ η) (hbase : ∀ (l : ℕ), coarsePoincareRHSSn Q s u (m + l) ≤ B) : coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalUSeminormErrorAverage Q u s η (m + k) ≤ η * B

Uniform tail bounds on S_{m+k} give the corresponding absorbed u component bounds along the iteration tail.

theorem HCPolySupport.weakFluxRHSDepthWeight_mul_harmonicSeminormErrorAverage_le_eta_mul_base {d : ℕ} (Q : TriadicCube d) (v : TriadicCube d → Vec d → Vec d) (s : ℝ) {η B : ℝ} (n : ℕ) (hη_nonneg : 0 ≤ η) (hbase : weakFluxRHSHarmonicRemainderScaledAveragedSeminormSq Q s v n ≤ B) : coarsePoincareRHSDepthWeight s n * weakFluxRHSLocalHarmonicSeminormErrorAverage Q v s η n ≤ η * B

Any scaled varying-cube harmonic-remainder bound gives the corresponding weighted absorbed harmonic component bound after multiplying by η.

theorem HCPolySupport.weakFluxRHSDepthWeight_mul_harmonicSeminormErrorAverage_le_eta_mul_base_of_tail {d : ℕ} (Q : TriadicCube d) (v : TriadicCube d → Vec d → Vec d) (s : ℝ) {η B : ℝ} (m k : ℕ) (hη_nonneg : 0 ≤ η) (hbase : ∀ (l : ℕ), weakFluxRHSHarmonicRemainderScaledAveragedSeminormSq Q s v (m + l) ≤ B) : coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalHarmonicSeminormErrorAverage Q v s η (m + k) ≤ η * B

Uniform tail bounds on the scaled harmonic-remainder seminorm give the corresponding absorbed harmonic component bounds along the iteration tail.

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

Descendant average of the absorbed centered-forcing component.

Equations

• HCPolySupport.weakFluxRHSLocalForceErrorAverage Q a g s η n = HCPolySupport.descendantsAverage Q n fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.weakFluxRHSLocalForceError R a g s η

theorem HCPolySupport.weakFluxRHSLocalForceErrorAverage_le_of_multiplierSqBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s : ℝ) {η : ℝ} (n : ℕ) {K2 : ℝ} (hη : 0 < η) (hmult : ∀ R ∈ descendantsAtDepth Q n, weakFluxRHSLocalForceMultiplier R a s ^ 2 ≤ K2) : weakFluxRHSLocalForceErrorAverage Q a g s η n ≤ 2 * η⁻¹ * (K2 * descendantsAverage Q n fun (R : TriadicCube d) => weakFluxRHSLocalCenteredForceSeminorm R g s ^ 2)

Average forcing component controlled by a uniform multiplier-square bound.

theorem HCPolySupport.weakFluxRHSLocalForceErrorAverage_le_of_multiplierSqBound_of_centeredForceAverageBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s : ℝ) {η : ℝ} (n : ℕ) {K2 B : ℝ} (hη : 0 < η) (hK2 : 0 ≤ K2) (hmult : ∀ R ∈ descendantsAtDepth Q n, weakFluxRHSLocalForceMultiplier R a s ^ 2 ≤ K2) (hforceAvg : (descendantsAverage Q n fun (R : TriadicCube d) => weakFluxRHSLocalCenteredForceSeminorm R g s ^ 2) ≤ B) : weakFluxRHSLocalForceErrorAverage Q a g s η n ≤ 2 * η⁻¹ * (K2 * B)

Average forcing component controlled by a multiplier bound and an averaged centered-force bound.

theorem HCPolySupport.weakFluxRHSLocalForceErrorAverage_le_parentHalfLambda_of_centeredForceAverageBound {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) {s η lam Lam : ℝ} (n : ℕ) {B : ℝ} (hs : 0 < s) (hη : 0 < η) (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) (hforceAvg : (descendantsAverage Q n fun (R : TriadicCube d) => weakFluxRHSLocalCenteredForceSeminorm R g s ^ 2) ≤ B) : weakFluxRHSLocalForceErrorAverage Q a g s η n ≤ 2 * η⁻¹ * (weakFluxRHSParentHalfForceMultiplier Q a s n ^ 2 * B)

Average forcing component localized to the parent half-scale multiplier under an averaged centered-force bound.

theorem HCPolySupport.weakFluxRHSLocalCenteredForceSeminorm_eq_uncentered_of_mem {d : ℕ} {Q R : TriadicCube d} (g : Vec d → Vec d) (s : ℝ) {n : ℕ} (hR : R ∈ descendantsAtDepth Q n) (hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S)) : weakFluxRHSLocalCenteredForceSeminorm R g s = cubeBesovPositiveVectorSeminormTwo R s g

The weak-flux centered forcing seminorm agrees with the uncentered positive Besov seminorm under the standard descendant MemLp assumptions.

theorem HCPolySupport.descendantsAverage_sq_weakFluxRHSLocalCenteredForceSeminorm_eq_of_mem {d : ℕ} (Q : TriadicCube d) (g : Vec d → Vec d) (s : ℝ) (n : ℕ) (hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S)) : (descendantsAverage Q n fun (R : TriadicCube d) => weakFluxRHSLocalCenteredForceSeminorm R g s ^ 2) = descendantsAverage Q n fun (R : TriadicCube d) => cubeBesovPositiveVectorSeminormTwo R s g ^ 2

Descendant averages of weak-flux centered forcing seminorms agree with uncentered positive-Besov averages under the standard MemLp assumptions.

theorem HCPolySupport.weakFluxRHSLocalForceErrorAverage_le_parentHalfLambda_of_forceAverageBound {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) {s η lam Lam : ℝ} (n : ℕ) {B : ℝ} (hs : 0 < s) (hη : 0 < η) (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) (hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S)) (hforceAvg : (descendantsAverage Q n fun (R : TriadicCube d) => cubeBesovPositiveVectorSeminormTwo R s g ^ 2) ≤ B) : weakFluxRHSLocalForceErrorAverage Q a g s η n ≤ 2 * η⁻¹ * (weakFluxRHSParentHalfForceMultiplier Q a s n ^ 2 * B)

Average forcing component localized to the parent half-scale multiplier under an averaged uncentered-force bound.

theorem HCPolySupport.weakFluxRHSLocalForceErrorAverage_le_parentHalfLambda_globalForceBound {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) {s η lam Lam : ℝ} (n : ℕ) (hs : 0 < s) (hη : 0 < η) (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) (hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hLocalBdd : ∀ R ∈ descendantsAtDepth Q n, BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) : weakFluxRHSLocalForceErrorAverage Q a g s η n ≤ 2 * η⁻¹ * (weakFluxRHSParentHalfForceMultiplier Q a s n ^ 2 * coarsePoincareRHSGlobalForceBound Q g s n)

Average forcing component localized to the parent half-scale multiplier and the global positive-Besov forcing bound.

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

Depth-weighted parent-localized weak-flux forcing base.

Equations

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

theorem HCPolySupport.weakFluxRHSWeightedGlobalForceBase_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s : ℝ) {η : ℝ} (hη : 0 < η) (n : ℕ) : 0 ≤ weakFluxRHSWeightedGlobalForceBase Q a g s η n

The depth-weighted parent-localized weak-flux forcing base is nonnegative for positive absorption parameter.

theorem HCPolySupport.weakFluxRHSWeightedGlobalForceBase_succ {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s η : ℝ) (n : ℕ) : weakFluxRHSWeightedGlobalForceBase Q a g s η (n + 1) = Real.rpow 3 (-s) * weakFluxRHSWeightedGlobalForceBase Q a g s η n

The weighted weak-flux forcing base decays by 3^{-s} when the depth is incremented.

theorem HCPolySupport.weakFluxRHSWeightedGlobalForceBase_add_eq_base_mul_ratio_pow {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s η : ℝ) (m k : ℕ) : weakFluxRHSWeightedGlobalForceBase Q a g s η (m + k) = weakFluxRHSWeightedGlobalForceBase Q a g s η m * Real.rpow 3 (-s) ^ k

The weighted weak-flux forcing base at depth m + k is the depth-m base times 3^{-s} to the k.

theorem HCPolySupport.weakFluxRHSWeightedGlobalForceBase_add_le_base {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) {s η : ℝ} (m k : ℕ) (hs : 0 < s) (hη : 0 < η) : weakFluxRHSWeightedGlobalForceBase Q a g s η (m + k) ≤ weakFluxRHSWeightedGlobalForceBase Q a g s η m

The weighted weak-flux forcing base decreases along descendants when s > 0.

theorem HCPolySupport.weakFluxRHSDepthWeight_mul_forceErrorAverage_le_weightedGlobalForceBase {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) {s η lam Lam : ℝ} (m k : ℕ) (hs : 0 < s) (hη : 0 < η) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hsum_half : Summable fun (l : ℕ) => geometricWeight (s / 2) 2 l * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑l) a).rpow 1) (hmem : ∀ (j : ℕ), ∀ S ∈ descendantsAtDepth Q j, MeasureTheory.MemLp g 2 (normalizedCubeMeasure S)) (hGlobalBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N g)) (hLocalBdd : ∀ R ∈ descendantsAtDepth Q (m + k), BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)) : coarsePoincareRHSDepthWeight s (m + k) * weakFluxRHSLocalForceErrorAverage Q a g s η (m + k) ≤ weakFluxRHSWeightedGlobalForceBase Q a g s η m

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