Coarse-graining support: Support.Besov.Negative

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

Finite-depth concrete negative/circ cube Besov seminorms.

This file freezes the first block-average-facing negative Besov layer used later in testing and coarse-graining arguments. As on the positive side, the scale parameter is encoded by a depth j : ℕ relative to a fixed parent cube Q, and the outer aggregation is truncated at a finite depth.

At this checkpoint we only record the concrete circ quantities. The genuine duality-based negative Besov seminorms and their comparison theorems belong in Duality.lean.

@[simp]

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

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

The average over depth-j descendants of absolute cube means raised to p.toReal.

Equations

• HCPolySupport.cubeBesovCircDepthAverage Q p u j = HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => ‖HCPolySupport.cubeAverage R u‖ ^ p.toReal

noncomputable def HCPolySupport.cubeBesovCircDepthWeight {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) : ℝ

The side length at depth j raised to the order s.

Equations

• HCPolySupport.cubeBesovCircDepthWeight Q s j = (HCPolySupport.cubeScaleFactor Q / 3 ^ j) ^ s

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

The p-power mean of descendant cube means multiplied by the depth weight.

Equations

• HCPolySupport.cubeBesovCircDepthSeminorm Q s p u j = HCPolySupport.cubeBesovCircDepthWeight Q s j * HCPolySupport.cubeBesovCircDepthAverage Q p u j ^ (1 / p.toReal)

noncomputable def HCPolySupport.cubeBesovCircPartialSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) : ℝ

The q-power sum of weighted circ quantities at depths zero through N, to power 1/q.

Equations

• HCPolySupport.cubeBesovCircPartialSeminorm Q s p q N u = (∑ j ∈ Finset.range (N + 1), HCPolySupport.cubeBesovCircDepthSeminorm Q s p u j ^ q.toReal) ^ (1 / q.toReal)

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

The maximum of the weighted circ quantities at depths zero through N.

Equations

• HCPolySupport.cubeBesovCircPartialSeminormTop Q s p N u = (Finset.range (N + 1)).sup' ⋯ fun (j : ℕ) => HCPolySupport.cubeBesovCircDepthSeminorm Q s p u j

noncomputable def HCPolySupport.cubeBesovCircPartialNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) : ℝ

The finite circ norm, defined to equal its circ seminorm.

Equations

• HCPolySupport.cubeBesovCircPartialNorm Q s p q N u = HCPolySupport.cubeBesovCircPartialSeminorm Q s p q N u

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

The finite circ norm for the maximum aggregation, equal to its circ seminorm.

Equations

• HCPolySupport.cubeBesovCircPartialNormTop Q s p N u = HCPolySupport.cubeBesovCircPartialSeminormTop Q s p N u

@[simp]

theorem HCPolySupport.cubeBesovCircDepthAverage_depth_zero {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) : cubeBesovCircDepthAverage Q p u 0 = ‖cubeAverage Q u‖ ^ p.toReal

@[simp]

theorem HCPolySupport.cubeBesovCircDepthWeight_depth_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) : cubeBesovCircDepthWeight Q s 0 = cubeBesovScaleWeight (-s) Q

theorem HCPolySupport.cubeBesovCircDepthAverage_nonneg {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) : 0 ≤ cubeBesovCircDepthAverage Q p u j

theorem HCPolySupport.cubeBesovCircDepthWeight_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) : 0 ≤ cubeBesovCircDepthWeight Q s j

theorem HCPolySupport.cubeBesovCircDepthSeminorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) : 0 ≤ cubeBesovCircDepthSeminorm Q s p u j

theorem HCPolySupport.cubeBesovCircPartialSeminorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) : 0 ≤ cubeBesovCircPartialSeminorm Q s p q N u

theorem HCPolySupport.cubeBesovCircPartialSeminormTop_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (u : Vec d → ℝ) : 0 ≤ cubeBesovCircPartialSeminormTop Q s p N u

theorem HCPolySupport.cubeBesovCircPartialNorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (u : Vec d → ℝ) : 0 ≤ cubeBesovCircPartialNorm Q s p q N u

theorem HCPolySupport.cubeBesovCircPartialNormTop_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (u : Vec d → ℝ) : 0 ≤ cubeBesovCircPartialNormTop Q s p N u

theorem HCPolySupport.cubeBesovCircDepthAverage_eq_descendantsAverage_projection {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) (j : ℕ) (hp : p ≠ 0) : cubeBesovCircDepthAverage Q p u j = descendantsAverage Q j fun (R : TriadicCube d) => cubeLpNorm R p (cubeProjection Q j u) ^ p.toReal

@[simp]

theorem HCPolySupport.cubeBesovCircDepthAverage_const {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (c : ℝ) (j : ℕ) : cubeBesovCircDepthAverage Q p (fun (x : Vec d) => c) j = ‖c‖ ^ p.toReal

theorem HCPolySupport.cubeBesovCircDepthAverage_zero {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (j : ℕ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) : cubeBesovCircDepthAverage Q p (fun (x : Vec d) => 0) j = 0

@[simp]

theorem HCPolySupport.cubeBesovCircDepthSeminorm_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (j : ℕ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) : cubeBesovCircDepthSeminorm Q s p (fun (x : Vec d) => 0) j = 0

@[simp]

theorem HCPolySupport.cubeBesovCircPartialSeminorm_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) (hq0 : q ≠ 0) (hqTop : q ≠ ⊤) : (cubeBesovCircPartialSeminorm Q s p q N fun (x : Vec d) => 0) = 0

@[simp]

theorem HCPolySupport.cubeBesovCircPartialSeminormTop_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) : (cubeBesovCircPartialSeminormTop Q s p N fun (x : Vec d) => 0) = 0

@[simp]

theorem HCPolySupport.cubeBesovCircPartialNorm_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p q : ENNReal) (N : ℕ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) (hq0 : q ≠ 0) (hqTop : q ≠ ⊤) : (cubeBesovCircPartialNorm Q s p q N fun (x : Vec d) => 0) = 0

@[simp]

theorem HCPolySupport.cubeBesovCircPartialNormTop_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (hp0 : p ≠ 0) (hpTop : p ≠ ⊤) : (cubeBesovCircPartialNormTop Q s p N fun (x : Vec d) => 0) = 0