Coarse-graining support: Support.Deterministic.WeakNormInterfaces.Definitions

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

Deterministic vector-valued weak norm interfaces

This file isolates the Chapter-3 negative-seminorm surface we need for coarse-grained estimates without touching the active scalar Besov files.

The definitions are the note-normalized q = 1, p = 2 vector-field quantities corresponding to

3^{-s m} [F]_{B^{-s}_{2,1}(Q)}

when Q has scale m.

noncomputable def HCPolySupport.cubeBesovNegativeVectorDepthAverage {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j : ℕ) : ℝ

The depth-j block-average square for a vector field on a parent cube Q.

Equations

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

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

The note-normalized negative depth seminorm. For a parent cube of scale m, this is the depth-j contribution with weight 3^{-s j}.

Equations

• HCPolySupport.cubeBesovNegativeVectorDepthSeminorm Q s u j = Real.rpow 3 (-s * ↑j) * √(HCPolySupport.cubeBesovNegativeVectorDepthAverage Q u j)

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

The finite-depth q = 1 negative seminorm for vector fields.

Equations

• HCPolySupport.cubeBesovNegativeVectorPartialSeminorm Q s N u = ∑ j ∈ Finset.range (N + 1), HCPolySupport.cubeBesovNegativeVectorDepthSeminorm Q s u j

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

The finite-depth q = 2 negative seminorm for vector fields.

Equations

• HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N u = √(∑ j ∈ Finset.range (N + 1), HCPolySupport.cubeBesovNegativeVectorDepthSeminorm Q s u j ^ 2)

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

The full note-normalized q = 1 negative seminorm for vector fields.

Equations

• HCPolySupport.cubeBesovNegativeVectorSeminorm Q s u = sSup (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminorm Q s N u)

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

The full note-normalized q = 2 negative seminorm for vector fields.

Equations

• HCPolySupport.cubeBesovNegativeVectorSeminormTwo Q s u = sSup (Set.range fun (N : ℕ) => HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo Q s N u)

theorem HCPolySupport.cubeBesovNegativeVectorDepthAverage_nonneg {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j : ℕ) : 0 ≤ cubeBesovNegativeVectorDepthAverage Q u j

theorem HCPolySupport.sqrt_add_le_add_sqrt_of_nonneg {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : √(a + b) ≤ √a + √b

Scalar square-root subadditivity in the two-term form used below.

theorem HCPolySupport.sqrt_four_mul_sum_le_two_mul_sum_sqrt {a b c d : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hd : 0 ≤ d) : √(4 * (a + b + c + d)) ≤ 2 * (√a + √b + √c + √d)

Four-term scalar square-root subadditivity with the Cauchy factor 2.

theorem HCPolySupport.weighted_sqrt_sum_le_const_mul_weighted_sqrt_sum_of_le_const_sq_mul {ι : Type u_1} (I : Finset ι) (weight value bound : ι → ℝ) {C : ℝ} (hC : 0 ≤ C) (hweight : ∀ i ∈ I, 0 ≤ weight i) (hvalue : ∀ i ∈ I, value i ≤ C ^ 2 * bound i) : ∑ i ∈ I, weight i * √(value i) ≤ C * ∑ i ∈ I, weight i * √(bound i)

theorem HCPolySupport.weighted_sqrt_sum_le_weighted_coeff_sqrt_sum_of_le_sq_mul {ι : Type u_1} (I : Finset ι) (weight value bound coeff : ι → ℝ) (hcoeff : ∀ i ∈ I, 0 ≤ coeff i) (hweight : ∀ i ∈ I, 0 ≤ weight i) (hvalue : ∀ i ∈ I, value i ≤ coeff i ^ 2 * bound i) : ∑ i ∈ I, weight i * √(value i) ≤ ∑ i ∈ I, weight i * (coeff i * √(bound i))

theorem HCPolySupport.triadicDepthWeight_eq_pow (s : ℝ) (j : ℕ) : Real.rpow 3 (-(s * ↑j)) = Real.rpow 3 (-s) ^ j

theorem HCPolySupport.triadicDepthWeight_nonneg (s : ℝ) (j : ℕ) : 0 ≤ Real.rpow 3 (-s * ↑j)

theorem HCPolySupport.triadicDepthWeight_mul_growth_eq (s s' : ℝ) (j : ℕ) : Real.rpow 3 (-s * ↑j) * Real.rpow 3 (s' * ↑j) = Real.rpow 3 (-(s - s') * ↑j)

theorem HCPolySupport.triadicDepthWeight_mul_const_growth_eq (C s s' : ℝ) (j : ℕ) : Real.rpow 3 (-s * ↑j) * (C * Real.rpow 3 (s' * ↑j)) = C * Real.rpow 3 (-(s - s') * ↑j)

theorem HCPolySupport.filteredTriadicWeight_sqrtDescendantNorm_le_constantWeightedSqrt {d : ℕ} (Q : TriadicCube d) (s s' C : ℝ) (N : ℕ) (high : ℕ → Prop) [DecidablePred high] (component : ℕ → TriadicCube d → Vec d) (gap : ℕ → ℝ) (hC : 0 ≤ C) (hbound : ∀ j ∈ Finset.filter high (Finset.range (N + 1)), (descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (component j R)) ≤ (C * Real.rpow 3 (s' * ↑j)) ^ 2 * gap j) : ∑ j ∈ Finset.range (N + 1) with high j, Real.rpow 3 (-s * ↑j) * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (component j R)) ≤ C * ∑ j ∈ Finset.range (N + 1) with high j, Real.rpow 3 (-(s - s') * ↑j) * √(gap j)

If a cube-indexed contribution has a depthwise squared bound with growth C^2 * 3^{2s'j}, then its B^{-s} weighted square-root sum is controlled by the shifted B^{-(s-s')} weighted square-root sum of the controlling gap.

This is the deterministic algebraic core behind the Section 5.3 mismatch and additivity-gap estimates: the analytic input is only the depthwise squared bound, and the conclusion performs the 3^{-sj} 3^{s'j} = 3^{-(s-s')j} weight shift.

theorem HCPolySupport.sum_filter_triadicDepthWeight_le_geometric_inv (s : ℝ) (N : ℕ) (low : ℕ → Prop) [DecidablePred low] (hs : 0 < s) : ∑ j ∈ Finset.range (N + 1) with low j, Real.rpow 3 (-s * ↑j) ≤ (1 - Real.rpow 3 (-s))⁻¹

theorem HCPolySupport.sum_range_filter_ge_triadicDepthWeight_le_geometric_tail (s : ℝ) (N L : ℕ) (hs : 0 < s) : ∑ j ∈ Finset.range (N + 1) with L ≤ j, Real.rpow 3 (-s * ↑j) ≤ Real.rpow 3 (-s * ↑L) * (1 - Real.rpow 3 (-s))⁻¹

theorem HCPolySupport.sum_range_filter_not_lt_triadicDepthWeight_le_geometric_tail (s : ℝ) (N L : ℕ) (hs : 0 < s) : ∑ j ∈ Finset.range (N + 1) with ¬j < L, Real.rpow 3 (-s * ↑j) ≤ Real.rpow 3 (-s * ↑L) * (1 - Real.rpow 3 (-s))⁻¹

theorem HCPolySupport.cubeBesovNegativeVectorDepthAverage_le_four_mul_sum_of_cubeAverageVec_eq {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j : ℕ) (predictor additivity lowScale tail : TriadicCube d → Vec d) (hdecomp : ∀ R ∈ descendantsAtDepth Q j, cubeAverageVec R u = predictor R + additivity R + lowScale R + tail R) : cubeBesovNegativeVectorDepthAverage Q u j ≤ descendantsAverage Q j fun (R : TriadicCube d) => 4 * (vecNormSq (predictor R) + vecNormSq (additivity R) + vecNormSq (lowScale R) + vecNormSq (tail R))

Depthwise four-term Cauchy split for the negative weak-norm block average. If each descendant cube average decomposes into four vector terms, then the depth average is controlled by the average of the four squared sizes.

theorem HCPolySupport.cubeBesovNegativeVectorDepthSeminorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) : 0 ≤ cubeBesovNegativeVectorDepthSeminorm Q s u j

theorem HCPolySupport.cubeBesovNegativeVectorDepthSeminorm_anti_mono_exponent {d : ℕ} (Q : TriadicCube d) {a b : ℝ} (hab : a ≤ b) (u : Vec d → Vec d) (j : ℕ) : cubeBesovNegativeVectorDepthSeminorm Q b u j ≤ cubeBesovNegativeVectorDepthSeminorm Q a u j

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_anti_mono_exponent {d : ℕ} (Q : TriadicCube d) {a b : ℝ} (hab : a ≤ b) (N : ℕ) (u : Vec d → Vec d) : cubeBesovNegativeVectorPartialSeminorm Q b N u ≤ cubeBesovNegativeVectorPartialSeminorm Q a N u

theorem HCPolySupport.cubeBesovNegativeVectorDepthSeminorm_eq_gap_mul {d : ℕ} (Q : TriadicCube d) (a b : ℝ) (u : Vec d → Vec d) (j : ℕ) : cubeBesovNegativeVectorDepthSeminorm Q a u j = Real.rpow 3 (-(a - b) * ↑j) * cubeBesovNegativeVectorDepthSeminorm Q b u j

Exact depthwise conversion between two negative-Besov exponents.

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_le_gap_sqrt_mul_partialSeminormTwo {d : ℕ} (Q : TriadicCube d) (a b : ℝ) (N : ℕ) (u : Vec d → Vec d) : cubeBesovNegativeVectorPartialSeminorm Q a N u ≤ √(∑ j ∈ Finset.range (N + 1), Real.rpow 3 (-(a - b) * ↑j) ^ 2) * cubeBesovNegativeVectorPartialSeminormTwo Q b N u

Finite-depth Cauchy conversion from the q = 1 negative seminorm at a larger exponent to the q = 2 negative seminorm at a smaller exponent.

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_le_gap_geometric_mul_partialSeminormTwo {d : ℕ} (Q : TriadicCube d) {a b : ℝ} (hgap : 0 < a - b) (N : ℕ) (u : Vec d → Vec d) : cubeBesovNegativeVectorPartialSeminorm Q a N u ≤ √(1 - Real.rpow 3 (-2 * (a - b)))⁻¹ * cubeBesovNegativeVectorPartialSeminormTwo Q b N u

Geometric-loss version of the finite-depth q = 1 to q = 2 conversion.

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_scale_compare_of_le {d : ℕ} (Q : TriadicCube d) {r t : ℝ} (ht : t ≤ r) (N : ℕ) (F : Vec d → Vec d) : cubeBesovScaleWeight (-r) Q * cubeBesovNegativeVectorPartialSeminorm Q r N F ≤ cubeBesovScaleWeight (-(r - t)) Q * (cubeBesovScaleWeight (-t) Q * cubeBesovNegativeVectorPartialSeminorm Q t N F)

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_flux_scale_compare {d : ℕ} (Q : TriadicCube d) {s t : ℝ} (hst : s + t ≤ 1) (N : ℕ) (F : Vec d → Vec d) : cubeBesovScaleWeight (-(1 - s)) Q * cubeBesovNegativeVectorPartialSeminorm Q (1 - s) N F ≤ cubeBesovScaleWeight (-(1 - s - t)) Q * (cubeBesovScaleWeight (-t) Q * cubeBesovNegativeVectorPartialSeminorm Q t N F)

theorem HCPolySupport.cubeBesovNegativeVectorDepthSeminorm_le_of_depthAverage_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) {A : ℝ} (hA : cubeBesovNegativeVectorDepthAverage Q u j ≤ A) : cubeBesovNegativeVectorDepthSeminorm Q s u j ≤ Real.rpow 3 (-s * ↑j) * √A

Turn a bound for one descendant-average block into the corresponding weighted negative-Besov depth bound. This is the analytic insertion point used by the Section 5.3 weak-norm estimates after the local Caccioppoli/Besov argument has produced depthwise controls.

theorem HCPolySupport.descendantsAverage_vecNormSq_nonneg {d : ℕ} (Q : TriadicCube d) (j : ℕ) (v : TriadicCube d → Vec d) : 0 ≤ descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (v R)

theorem HCPolySupport.sqrt_descendantsAverage_vecNormSq_const_smul_eq {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) (V : TriadicCube d → Vec d) (hc : 0 ≤ c) : √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (c • V R)) = c * √(descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (V R))

theorem HCPolySupport.descendantsAverage_const_eq {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) : (descendantsAverage Q j fun (x : TriadicCube d) => c) = c

theorem HCPolySupport.descendantsAverage_four_mul_sum_vecNormSq_eq {d : ℕ} (Q : TriadicCube d) (j : ℕ) (v₁ v₂ v₃ v₄ : TriadicCube d → Vec d) : (descendantsAverage Q j fun (R : TriadicCube d) => 4 * (vecNormSq (v₁ R) + vecNormSq (v₂ R) + vecNormSq (v₃ R) + vecNormSq (v₄ R))) = 4 * ((((descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (v₁ R)) + descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (v₂ R)) + descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (v₃ R)) + descendantsAverage Q j fun (R : TriadicCube d) => vecNormSq (v₄ R))