Coarse-graining support: Support.Besov.Basic

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

Local building blocks for the cube Besov layer.

This file stays intentionally lightweight: it packages the cube-wise oscillation and scale weights that later positive and negative Besov definitions will assemble across descendants and scales.

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

The cube Lᵖ norm of the fluctuation of u about its cube average.

Equations

• HCPolySupport.cubeBesovOscillation Q p u = HCPolySupport.cubeLpNorm Q p (HCPolySupport.cubeFluctuation Q u)

@[reducible, inline]

noncomputable abbrev HCPolySupport.cubeBesovDisjointOscillation {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) : ℝ

Explicit disjoint-cube spelling of the legacy scalar cube oscillation.

Equations

• HCPolySupport.cubeBesovDisjointOscillation Q p u = HCPolySupport.cubeBesovOscillation Q p u

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

The Besov weight given by the cube scale factor raised to the power -s.

Equations

• HCPolySupport.cubeBesovScaleWeight s Q = HCPolySupport.cubeScaleFactor Q ^ (-s)

noncomputable def HCPolySupport.descendantsAverage {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → ℝ) : ℝ

The uniform arithmetic average of F over all descendants at depth j in Q.

Equations

• HCPolySupport.descendantsAverage Q j F = (↑(HCPolySupport.descendantsAtDepth Q j).card)⁻¹ * (HCPolySupport.descendantsAtDepth Q j).sum F

theorem HCPolySupport.descendantsAverage_nonneg {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → ℝ) (hF : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ F R) : 0 ≤ descendantsAverage Q j F

theorem HCPolySupport.descendantsAverage_mul_left {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) (F : TriadicCube d → ℝ) : (descendantsAverage Q j fun (R : TriadicCube d) => c * F R) = c * descendantsAverage Q j F

theorem HCPolySupport.descendantsAverage_le_descendantsAverage {d : ℕ} (Q : TriadicCube d) (j : ℕ) {F G : TriadicCube d → ℝ} (hFG : ∀ R ∈ descendantsAtDepth Q j, F R ≤ G R) : descendantsAverage Q j F ≤ descendantsAverage Q j G

theorem HCPolySupport.descendantsAverage_sum {d : ℕ} {ι : Type u_1} (Q : TriadicCube d) (j : ℕ) (s : Finset ι) (F : TriadicCube d → ι → ℝ) : (descendantsAverage Q j fun (R : TriadicCube d) => ∑ i ∈ s, F R i) = ∑ i ∈ s, descendantsAverage Q j fun (R : TriadicCube d) => F R i

theorem HCPolySupport.sq_rpow_half_eq_of_nonneg {x : ℝ} (hx : 0 ≤ x) : (x ^ 2) ^ (1 / 2) = x

theorem HCPolySupport.descendantsAverage_succ_eq_descendantsAverage_descendantsAverage {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → ℝ) : descendantsAverage Q (j + 1) F = descendantsAverage Q j fun (R : TriadicCube d) => descendantsAverage R 1 F

theorem HCPolySupport.descendantsAverage_mul_le_Lp_mul_Lq_of_nonneg {d : ℕ} (Q : TriadicCube d) (j : ℕ) (A B : TriadicCube d → ℝ) {p q : ℝ} (hpq : p.HolderConjugate q) (hA : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ A R) (hB : ∀ R ∈ descendantsAtDepth Q j, 0 ≤ B R) : (descendantsAverage Q j fun (R : TriadicCube d) => A R * B R) ≤ (descendantsAverage Q j fun (R : TriadicCube d) => A R ^ p) ^ (1 / p) * (descendantsAverage Q j fun (R : TriadicCube d) => B R ^ q) ^ (1 / q)

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

theorem HCPolySupport.cubeBesovOscillation_cubeFluctuation_eq_of_memLp_two {d : ℕ} (R Q : TriadicCube d) {u : Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure R)) : cubeBesovOscillation R 2 (cubeFluctuation Q u) = cubeBesovOscillation R 2 u

@[simp]

theorem HCPolySupport.cubeBesovOscillation_const {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (c : ℝ) : (cubeBesovOscillation Q p fun (x : Vec d) => c) = 0

theorem HCPolySupport.cubeBesovOscillation_zero {d : ℕ} (Q : TriadicCube d) (p : ENNReal) : (cubeBesovOscillation Q p fun (x : Vec d) => 0) = 0

theorem HCPolySupport.cubeBesovScaleWeight_nonneg {d : ℕ} (s : ℝ) (Q : TriadicCube d) : 0 ≤ cubeBesovScaleWeight s Q

theorem HCPolySupport.cubeBesovScaleWeight_mul_eq_scaleWeight_add {d : ℕ} (r q : ℝ) (Q : TriadicCube d) : cubeBesovScaleWeight r Q * cubeBesovScaleWeight q Q = cubeBesovScaleWeight (r + q) Q