Coarse-graining support: Support.Deterministic.WeakNormInterfacesPositiveQTwo

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

Note-normalized positive q = 2 vector weak norms

This file packages the minimal positive-order vector Besov surface needed on the right-hand-side branch of the deterministic Chapter-3 argument. The normalization is the note-facing one: when Q has scale m, the quantity here corresponds to 3^(s m) [u]_{\underline{B}^{s}_{2,2}(Q)}.

theorem HCPolySupport.cubeLpNorm_congr_on_cubeSet_generic {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (p : ENNReal) {u v : Vec d → E} (h : ∀ x ∈ cubeSet Q, u x = v x) : cubeLpNorm Q p u = cubeLpNorm Q p v

@[simp]

theorem HCPolySupport.cubeAverageVec_const {d : ℕ} (Q : TriadicCube d) (c : Vec d) : (cubeAverageVec Q fun (x : Vec d) => c) = c

theorem HCPolySupport.cubeAverageVec_sub_const {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (c : Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : (cubeAverageVec Q fun (x : Vec d) => u x - c) = cubeAverageVec Q u - c

theorem HCPolySupport.cubeAverageVec_sub_memLp {d : ℕ} (Q : TriadicCube d) (u v : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hv : MeasureTheory.MemLp v 2 (normalizedCubeMeasure Q)) : (cubeAverageVec Q fun (x : Vec d) => u x - v x) = cubeAverageVec Q u - cubeAverageVec Q v

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

Vector-valued fluctuation on a cube.

Equations

• HCPolySupport.cubeFluctuationVec Q u x = u x - HCPolySupport.cubeAverageVec Q u

@[simp]

theorem HCPolySupport.cubeFluctuationVec_apply {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (x : Vec d) : cubeFluctuationVec Q u x = u x - cubeAverageVec Q u

@[simp]

theorem HCPolySupport.cubeFluctuationVec_zero {d : ℕ} (Q : TriadicCube d) : cubeFluctuationVec Q 0 = 0

@[simp]

theorem HCPolySupport.cubeFluctuationVec_sub_const {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (c : Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : (cubeFluctuationVec Q fun (x : Vec d) => u x - c) = cubeFluctuationVec Q u

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

The depth-j positive q = 2 square average 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.cubeBesovPositiveVectorDepthSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) : ℝ

Note-normalized positive depth seminorm. For a parent cube of scale m, this is the depth-j contribution to 3^(s m) [u]_{\underline{B}^{s}_{2,2}(Q)}.

Equations

• HCPolySupport.cubeBesovPositiveVectorDepthSeminorm Q s u j = Real.rpow 3 (s * ↑j) * √(HCPolySupport.cubeBesovPositiveVectorDepthAverage Q u j)

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

Finite-depth note-normalized positive q = 2 seminorm for vector fields.

Equations

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

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

Full note-normalized positive q = 2 seminorm for vector fields.

Equations

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

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

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

theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) : 0 ≤ cubeBesovPositiveVectorPartialSeminormTwo Q s N u

@[simp]

theorem HCPolySupport.cubeBesovPositiveVectorDepthAverage_zero {d : ℕ} (Q : TriadicCube d) (j : ℕ) : cubeBesovPositiveVectorDepthAverage Q 0 j = 0

@[simp]

theorem HCPolySupport.cubeBesovPositiveVectorDepthSeminorm_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) : cubeBesovPositiveVectorDepthSeminorm Q s 0 j = 0

@[simp]

theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) : cubeBesovPositiveVectorPartialSeminormTwo Q s N 0 = 0

theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_zero_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N 0)

@[simp]

theorem HCPolySupport.cubeBesovPositiveVectorSeminormTwo_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) : cubeBesovPositiveVectorSeminormTwo Q s 0 = 0

@[simp]

theorem HCPolySupport.cubeBesovPositiveVectorDepthAverage_depth_zero {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) : cubeBesovPositiveVectorDepthAverage Q u 0 = cubeLpNorm Q 2 (cubeFluctuationVec Q u) ^ 2

theorem HCPolySupport.sq_cubeBesovPositiveVectorDepthSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) : cubeBesovPositiveVectorDepthSeminorm Q s u j ^ 2 = Real.rpow 3 (s * ↑j) ^ 2 * cubeBesovPositiveVectorDepthAverage Q u j

theorem HCPolySupport.sq_cubeBesovPositiveVectorPartialSeminormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) : cubeBesovPositiveVectorPartialSeminormTwo Q s N u ^ 2 = ∑ j ∈ Finset.range (N + 1), cubeBesovPositiveVectorDepthSeminorm Q s u j ^ 2

theorem HCPolySupport.cubeBesovPositiveVectorDepthAverage_add_eq_descendantsAverage {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j n : ℕ) : cubeBesovPositiveVectorDepthAverage Q u (j + n) = descendantsAverage Q j fun (R : TriadicCube d) => cubeBesovPositiveVectorDepthAverage R u n

theorem HCPolySupport.descendantsAverage_sq_cubeBesovPositiveVectorDepthSeminorm_eq_shifted {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j n : ℕ) : (Real.rpow 3 (s * ↑j) ^ 2 * descendantsAverage Q j fun (R : TriadicCube d) => cubeBesovPositiveVectorDepthSeminorm R s u n ^ 2) = cubeBesovPositiveVectorDepthSeminorm Q s u (j + n) ^ 2

theorem HCPolySupport.descendantsAverage_sq_scaled_cubeBesovPositiveVectorPartialSeminormTwo_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j N : ℕ) : (descendantsAverage Q j fun (R : TriadicCube d) => (Real.rpow 3 (s * ↑j) * cubeBesovPositiveVectorPartialSeminormTwo R s N u) ^ 2) ≤ cubeBesovPositiveVectorPartialSeminormTwo Q s (j + N) u ^ 2

theorem HCPolySupport.descendantsAverage_scaled_cubeBesovPositiveVectorPartialSeminormTwo_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j N : ℕ) : (descendantsAverage Q j fun (R : TriadicCube d) => (Real.rpow 3 (s * ↑j) * cubeBesovPositiveVectorPartialSeminormTwo R s N u) ^ 2) ^ (1 / 2) ≤ cubeBesovPositiveVectorPartialSeminormTwo Q s (j + N) u

theorem HCPolySupport.cubeBesovPositiveVectorSeminormTwo_le_of_partialBound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) {B : ℝ} (hB : ∀ (N : ℕ), cubeBesovPositiveVectorPartialSeminormTwo Q s N u ≤ B) : cubeBesovPositiveVectorSeminormTwo Q s u ≤ B

theorem HCPolySupport.cubeBesovPositiveVectorDepthSeminorm_le_of_exponent_le {d : ℕ} (Q : TriadicCube d) {s t : ℝ} (u : Vec d → Vec d) (j : ℕ) (hst : s ≤ t) : cubeBesovPositiveVectorDepthSeminorm Q s u j ≤ cubeBesovPositiveVectorDepthSeminorm Q t u j

theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_le_of_exponent_le {d : ℕ} (Q : TriadicCube d) {s t : ℝ} (u : Vec d → Vec d) (N : ℕ) (hst : s ≤ t) : cubeBesovPositiveVectorPartialSeminormTwo Q s N u ≤ cubeBesovPositiveVectorPartialSeminormTwo Q t N u

theorem HCPolySupport.cubeBesovPositiveVectorSeminormTwo_le_of_exponent_le_of_bddAbove {d : ℕ} (Q : TriadicCube d) {s t : ℝ} (u : Vec d → Vec d) (hst : s ≤ t) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q t N u)) : cubeBesovPositiveVectorSeminormTwo Q s u ≤ cubeBesovPositiveVectorSeminormTwo Q t u

theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_bddAbove_of_exponent_le {d : ℕ} (Q : TriadicCube d) {s t : ℝ} (u : Vec d → Vec d) (hst : s ≤ t) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q t N u)) : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N u)

theorem HCPolySupport.cubeBesovPositiveVectorDepthAverage_sub_const {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (c : Vec d) (j : ℕ) (hmem : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) : cubeBesovPositiveVectorDepthAverage Q (fun (x : Vec d) => u x - c) j = cubeBesovPositiveVectorDepthAverage Q u j

theorem HCPolySupport.cubeBesovPositiveVectorDepthSeminorm_sub_const {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (c : Vec d) (j : ℕ) (hmem : ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) : cubeBesovPositiveVectorDepthSeminorm Q s (fun (x : Vec d) => u x - c) j = cubeBesovPositiveVectorDepthSeminorm Q s u j

theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_sub_const {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) (c : Vec d) (hmem : ∀ j ∈ Finset.range (N + 1), ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) : (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => u x - c) = cubeBesovPositiveVectorPartialSeminormTwo Q s N u

theorem HCPolySupport.cubeBesovPositiveVectorSeminormTwo_sub_const {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (c : Vec d) (hmem : ∀ (j : ℕ), ∀ R ∈ descendantsAtDepth Q j, MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) : (cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => u x - c) = cubeBesovPositiveVectorSeminormTwo Q s u