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

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

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

Averaged squared q = 2 weak-flux seminorm at descendant depth j.

Equations

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

@[simp]

theorem HCPolySupport.weakFluxRHSAveragedSeminormSq_zero {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) : weakFluxRHSAveragedSeminormSq Q a s u 0 = (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2

theorem HCPolySupport.weakFluxRHSAveragedSeminormSq_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) : 0 ≤ weakFluxRHSAveragedSeminormSq Q a s u j

noncomputable def HCPolySupport.weakFluxRHSAveragedErrorSum {d : ℕ} (Q : TriadicCube d) (s : ℝ) (E : TriadicCube d → ℝ) (m N : ℕ) : ℝ

Finite weighted error sum produced by iterating the weak-flux recurrence.

Equations

• HCPolySupport.weakFluxRHSAveragedErrorSum Q s E m N = ∑ k ∈ Finset.range N, Real.rpow 3 (-2 * s) ^ k * HCPolySupport.descendantsAverage Q (m + k) E

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

Manuscript T_n-style scaled averaged weak-flux quantity.

Equations

• HCPolySupport.weakFluxRHSScaledAveragedSeminormSq Q a s u j = HCPolySupport.coarsePoincareRHSDepthWeight s j * HCPolySupport.weakFluxRHSAveragedSeminormSq Q a s u j

@[simp]

theorem HCPolySupport.weakFluxRHSScaledAveragedSeminormSq_zero {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) : weakFluxRHSScaledAveragedSeminormSq Q a s u 0 = (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2

theorem HCPolySupport.weakFluxRHSScaledAveragedSeminormSq_nonneg {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) : 0 ≤ weakFluxRHSScaledAveragedSeminormSq Q a s u j

noncomputable def HCPolySupport.weakFluxRHSScaledAveragedErrorSum {d : ℕ} (Q : TriadicCube d) (s θ : ℝ) (E : TriadicCube d → ℝ) (m N : ℕ) : ℝ

Finite weighted error sum for the scaled weak-flux recurrence.

Equations

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

theorem HCPolySupport.weakFluxRHSScaledStepCoeff_eq (s : ℝ) : coarsePoincareRHSScaledStepCoeff s (Real.rpow 3 (-2 * s)) = Real.rpow 3 (-s)

theorem HCPolySupport.weakFluxRHSScaledAveragedErrorSum_le_base_mul_inv_one_sub {d : ℕ} (Q : TriadicCube d) (s θ : ℝ) (E : TriadicCube d → ℝ) (m N : ℕ) {B : ℝ} (hr_nonneg : 0 ≤ coarsePoincareRHSScaledStepCoeff s θ) (hr_lt_one : coarsePoincareRHSScaledStepCoeff s θ < 1) (hB_nonneg : 0 ≤ B) (hterm : ∀ k ∈ Finset.range N, coarsePoincareRHSDepthWeight s (m + k) * descendantsAverage Q (m + k) E ≤ B) : weakFluxRHSScaledAveragedErrorSum Q s θ E m N ≤ B * (1 - coarsePoincareRHSScaledStepCoeff s θ)⁻¹

A uniform base bound on the weighted averaged error terms controls the finite scaled weak-flux error sum by a geometric tail.

theorem HCPolySupport.weakFluxRHSScaledAveragedErrorSum_le_base_mul_inv_one_sub_weakFlux {d : ℕ} (Q : TriadicCube d) (s : ℝ) (E : TriadicCube d → ℝ) (m N : ℕ) {B : ℝ} (hs : 0 < s) (hB_nonneg : 0 ≤ B) (hterm : ∀ k ∈ Finset.range N, coarsePoincareRHSDepthWeight s (m + k) * descendantsAverage Q (m + k) E ≤ B) : weakFluxRHSScaledAveragedErrorSum Q s (Real.rpow 3 (-2 * s)) E m N ≤ B * (1 - Real.rpow 3 (-s))⁻¹

Note-facing form of the scaled weak-flux error summation: after the natural T_n scaling the one-step ratio is 3^{-s}.

@[simp]

theorem HCPolySupport.localizedFluxDefectNegativeBesovAverageTwo_matVecMul_eq_sqrt_weakFluxRHSAveragedSeminormSq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) : localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) j = √(weakFluxRHSAveragedSeminormSq Q a s u j)

The localized ℓ² flux-defect average used by the Section 3.3 black boxes is the square root of the averaged squared weak-flux quantity.

theorem HCPolySupport.localizedFluxDefectNegativeBesovAverageTwo_matVecMul_le_sqrt_of_weakFluxRHSAveragedSeminormSq_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) {B : ℝ} (hB : weakFluxRHSAveragedSeminormSq Q a s u j ≤ B) : localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) j ≤ √B

Square-root extraction from a bound on the averaged squared weak-flux quantity.

theorem HCPolySupport.localizedFluxDefectNegativeBesovAverageTwo_matVecMul_le_of_weakFluxRHSAveragedSeminormSq_le_sq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) {B : ℝ} (hB_nonneg : 0 ≤ B) (hB : weakFluxRHSAveragedSeminormSq Q a s u j ≤ B ^ 2) : localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) j ≤ B

Square-root extraction from a square bound on the averaged weak-flux quantity.

theorem HCPolySupport.weakFluxRHSAveragedSeminormSq_iterate_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (E : TriadicCube d → ℝ) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + E R) (m N : ℕ) : weakFluxRHSAveragedSeminormSq Q a s u m ≤ Real.rpow 3 (-2 * s) ^ N * weakFluxRHSAveragedSeminormSq Q a s u (m + N) + weakFluxRHSAveragedErrorSum Q s E m N

Finite-scale iteration of the averaged weak-flux recurrence. This is the direct Lean form of manuscript Section 3.2.3, Step 4, before the error terms are localized and summed with the final constants.

theorem HCPolySupport.weakFluxRHSScaledAveragedSeminormSq_iterate_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (E : TriadicCube d → ℝ) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + E R) (m N : ℕ) : weakFluxRHSScaledAveragedSeminormSq Q a s u m ≤ coarsePoincareRHSScaledStepCoeff s (Real.rpow 3 (-2 * s)) ^ N * weakFluxRHSScaledAveragedSeminormSq Q a s u (m + N) + weakFluxRHSScaledAveragedErrorSum Q s (Real.rpow 3 (-2 * s)) E m N

Finite-scale iteration of the manuscript T_n-scaled averaged weak-flux recurrence. The one-step coefficient becomes 3^{-s} after multiplying by the natural depth weight.

theorem HCPolySupport.weakFluxRHSScaledAveragedSeminormSq_terminal_tendsto_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (m : ℕ) (hs : 0 < s) (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u n)) : Filter.Tendsto (fun (N : ℕ) => coarsePoincareRHSScaledStepCoeff s (Real.rpow 3 (-2 * s)) ^ N * weakFluxRHSScaledAveragedSeminormSq Q a s u (m + N)) Filter.atTop (nhds 0)

The scaled weak-flux terminal term vanishes under boundedness and s > 0.

theorem HCPolySupport.weakFluxRHSScaledAveragedSeminormSq_le_of_terminal_tendsto {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (E : TriadicCube d → ℝ) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + E R) (m : ℕ) {B : ℝ} (hterminal : Filter.Tendsto (fun (N : ℕ) => coarsePoincareRHSScaledStepCoeff s (Real.rpow 3 (-2 * s)) ^ N * weakFluxRHSScaledAveragedSeminormSq Q a s u (m + N)) Filter.atTop (nhds 0)) (hError : ∀ (N : ℕ), weakFluxRHSScaledAveragedErrorSum Q s (Real.rpow 3 (-2 * s)) E m N ≤ B) : weakFluxRHSScaledAveragedSeminormSq Q a s u m ≤ B

Infinite-depth terminal passage for the scaled weak-flux recurrence.

theorem HCPolySupport.weakFluxRHSScaledAveragedSeminormSq_le_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (E : TriadicCube d → ℝ) (hs : 0 < s) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + E R) (m : ℕ) {B : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u n)) (hError : ∀ (N : ℕ), weakFluxRHSScaledAveragedErrorSum Q s (Real.rpow 3 (-2 * s)) E m N ≤ B) : weakFluxRHSScaledAveragedSeminormSq Q a s u m ≤ B

Infinite-depth scaled weak-flux bound using boundedness to discharge the terminal term.

theorem HCPolySupport.weakFluxRHSScaledAveragedSeminormSq_le_base_mul_inv_one_sub_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (E : TriadicCube d → ℝ) (hs : 0 < s) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + E R) (m : ℕ) {B : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u n)) (hB_nonneg : 0 ≤ B) (hterm : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s (m + k) * descendantsAverage Q (m + k) E ≤ B) : weakFluxRHSScaledAveragedSeminormSq Q a s u m ≤ B * (1 - Real.rpow 3 (-s))⁻¹

Bounded-tail scaled weak-flux iteration with the finite error sums closed by a uniform geometric base bound.

theorem HCPolySupport.weakFluxRHSAveragedSeminormSq_le_inv_depthWeight_mul_of_scaled_le {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (m : ℕ) {B : ℝ} (hB : weakFluxRHSScaledAveragedSeminormSq Q a s u m ≤ B) : weakFluxRHSAveragedSeminormSq Q a s u m ≤ (coarsePoincareRHSDepthWeight s m)⁻¹ * B

Convert a scaled T_m bound back to the unscaled averaged weak-flux quantity.

theorem HCPolySupport.negativeBesovFluxAverage_of_weakFluxRHSScaledAveragedSeminormSq {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (m : ℕ) {B : ℝ} (hB : weakFluxRHSScaledAveragedSeminormSq Q a s u m ≤ B) : localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * B)

Localized flux-defect handoff from a scaled averaged weak-flux bound.

theorem HCPolySupport.localizedFluxDefectNegativeBesovAverageTwo_matVecMul_le_sqrt_of_scaled_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (E : TriadicCube d → ℝ) (hs : 0 < s) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + E R) (m : ℕ) {B : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u n)) (hError : ∀ (N : ℕ), weakFluxRHSScaledAveragedErrorSum Q s (Real.rpow 3 (-2 * s)) E m N ≤ B) : localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * B)

Localized flux-defect form of the scaled bounded-tail weak-flux iteration.

theorem HCPolySupport.localizedFluxDefect_negativeBesovAverage_le_sqrt_baseError {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (E : TriadicCube d → ℝ) (hs : 0 < s) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + E R) (m : ℕ) {B : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSScaledAveragedSeminormSq Q a s u n)) (hB_nonneg : 0 ≤ B) (hterm : ∀ (k : ℕ), coarsePoincareRHSDepthWeight s (m + k) * descendantsAverage Q (m + k) E ≤ B) : localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) m ≤ √((coarsePoincareRHSDepthWeight s m)⁻¹ * (B * (1 - Real.rpow 3 (-s))⁻¹))

Localized flux-defect form of the scaled bounded-tail weak-flux iteration after closing the finite error sums by a uniform geometric base bound.

theorem HCPolySupport.weakFluxRHSAveragedSeminormSq_terminal_tendsto_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (m : ℕ) (hs : 0 < s) (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSAveragedSeminormSq Q a s u n)) : Filter.Tendsto (fun (N : ℕ) => Real.rpow 3 (-2 * s) ^ N * weakFluxRHSAveragedSeminormSq Q a s u (m + N)) Filter.atTop (nhds 0)

The discounted terminal term vanishes if the averaged weak-flux seminorms are bounded above and s > 0.

theorem HCPolySupport.weakFluxRHSAveragedSeminormSq_le_of_terminal_tendsto {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (E : TriadicCube d → ℝ) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + E R) (m : ℕ) {B : ℝ} (hterminal : Filter.Tendsto (fun (N : ℕ) => Real.rpow 3 (-2 * s) ^ N * weakFluxRHSAveragedSeminormSq Q a s u (m + N)) Filter.atTop (nhds 0)) (hError : ∀ (N : ℕ), weakFluxRHSAveragedErrorSum Q s E m N ≤ B) : weakFluxRHSAveragedSeminormSq Q a s u m ≤ B

Infinite-depth terminal passage for the averaged weak-flux recurrence. Once the terminal term tends to zero, any uniform bound on the finite weighted error sums bounds the initial averaged seminorm.

theorem HCPolySupport.weakFluxRHSAveragedSeminormSq_le_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (E : TriadicCube d → ℝ) (hs : 0 < s) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + E R) (m : ℕ) {B : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSAveragedSeminormSq Q a s u n)) (hError : ∀ (N : ℕ), weakFluxRHSAveragedErrorSum Q s E m N ≤ B) : weakFluxRHSAveragedSeminormSq Q a s u m ≤ B

Infinite-depth weak-flux bound using boundedness of the averaged seminorm sequence to discharge the terminal term.

theorem HCPolySupport.localizedFluxDefectNegativeBesovAverageTwo_matVecMul_le_sqrt_of_bddAbove {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s : ℝ) (u : Vec d → Vec d) (E : TriadicCube d → ℝ) (hs : 0 < s) (hlocal : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, (cubeBesovNegativeVectorSeminormTwo R s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage R 1 fun (S : TriadicCube d) => (cubeBesovNegativeVectorSeminormTwo S s fun (x : Vec d) => matVecMul (a x) (u x)) ^ 2) + E R) (m : ℕ) {B : ℝ} (hBdd : BddAbove (Set.range fun (n : ℕ) => weakFluxRHSAveragedSeminormSq Q a s u n)) (hError : ∀ (N : ℕ), weakFluxRHSAveragedErrorSum Q s E m N ≤ B) : localizedFluxDefectNegativeBesovAverageTwo Q s (fun (x : Vec d) => matVecMul (a x) (u x)) m ≤ √B

Localized flux-defect form of the bounded-tail weak-flux iteration.