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

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

noncomputable def HCPolySupport.coarsePoincareRHSDepthWeight (s : ℝ) (n : ℕ) : ℝ

The natural-depth scale weight used to pass from R_n to S_n.

Equations

• HCPolySupport.coarsePoincareRHSDepthWeight s n = Real.rpow 3 (-s * ↑n)

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

Natural-depth version of the note's averaged R_n quantity.

Equations

• HCPolySupport.coarsePoincareRHSRn Q s u n = HCPolySupport.descendantsAverage Q n fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.cubeBesovNegativeVectorSeminormTwo R s u ^ 2

@[simp]

theorem HCPolySupport.coarsePoincareRHSRn_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) : coarsePoincareRHSRn Q s u 0 = cubeBesovNegativeVectorSeminormTwo Q s u ^ 2

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

Natural-depth version of the note's scaled S_n quantity.

Equations

• HCPolySupport.coarsePoincareRHSSn Q s u n = HCPolySupport.coarsePoincareRHSDepthWeight s n * HCPolySupport.coarsePoincareRHSRn Q s u n

@[simp]

theorem HCPolySupport.coarsePoincareRHSDepthWeight_zero (s : ℝ) : coarsePoincareRHSDepthWeight s 0 = 1

@[simp]

theorem HCPolySupport.coarsePoincareRHSSn_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) : coarsePoincareRHSSn Q s u 0 = cubeBesovNegativeVectorSeminormTwo Q s u ^ 2

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

Averaged intrinsic local error appearing in the absorbed R_n recurrence.

Equations

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

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

Averaged intrinsic local energy piece in the absorbed R_n recurrence.

Equations

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

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

Averaged intrinsic local forcing piece in the absorbed R_n recurrence.

Equations

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

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

Intrinsic localized one-step error after absorption and parent coefficient localization.

Equations

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

noncomputable def HCPolySupport.coarsePoincareRHSIntrinsicWeightedLocalizedEnergyForceErrorSum {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) (s θ CE CF : ℝ) (B : ℕ → ℝ) (m N : ℕ) : ℝ

Finite weighted intrinsic localized-error sum produced by iterating the localized recurrence.

Equations

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

noncomputable def HCPolySupport.coarsePoincareRHSSIntrinsicWeightedLocalizedEnergyForceErrorSum {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) (s θ CE CF : ℝ) (B : ℕ → ℝ) (m N : ℕ) : ℝ

Scaled intrinsic localized-error sum produced by the localized S_n recurrence.

Equations

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

noncomputable def HCPolySupport.coarsePoincareRHSSIntrinsicWeightedGlobalEnergyErrorSum {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (u : Vec d → Vec d) (s θ CE : ℝ) (m N : ℕ) : ℝ

Intrinsic energy part of the scaled localized global-force error sum.

Equations

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

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

The k = 0 intrinsic energy coefficient for the scaled global-force finite sum.

Equations

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

noncomputable def HCPolySupport.coarsePoincareRHSSIntrinsicWeightedGlobalForceErrorSum {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (s θ CF : ℝ) (m N : ℕ) : ℝ

Intrinsic force part of the scaled localized global-force error sum.

Equations

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

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

The k = 0 intrinsic force coefficient for the scaled global-force finite sum.

Equations

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

theorem HCPolySupport.coarsePoincareRHSSIntrinsicWeightedLocalizedEnergyForceErrorSum_global_eq_energy_add_force {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g u : Vec d → Vec d) (s θ CE CF : ℝ) (m N : ℕ) : coarsePoincareRHSSIntrinsicWeightedLocalizedEnergyForceErrorSum Q a u s θ CE CF (fun (n : ℕ) => coarsePoincareRHSGlobalForceBound Q g s n) m N = coarsePoincareRHSSIntrinsicWeightedGlobalEnergyErrorSum Q a u s θ CE m N + coarsePoincareRHSSIntrinsicWeightedGlobalForceErrorSum Q a g s θ CF m N