Coarse-graining support:

Support.Deterministic.CoarseCaccioppoli.CutoffProduct.PositiveSeminorms.Definitions

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

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

The uniform average of squared cube L² norms of v over descendants at depth j.

Equations

• HCPolySupport.cubeL2ScalarDepthAverage Q v j = HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.cubeLpNorm R 2 v ^ 2

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

The square root of the depth-j average of squared L² norms, weighted by 3^(s j).

Equations

• HCPolySupport.cubeL2ScalarDepthSeminorm Q s v j = Real.rpow 3 (s * ↑j) * √(HCPolySupport.cubeL2ScalarDepthAverage Q v j)

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

The ℓ² aggregation of the weighted L² depth quantities from depth zero through N.

Equations

• HCPolySupport.cubeL2ScalarPartialSeminormTwo Q s N v = √(∑ j ∈ Finset.range (N + 1), HCPolySupport.cubeL2ScalarDepthSeminorm Q s v j ^ 2)

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

The uniform average of squared L² oscillations of v over descendants at depth j.

Equations

• HCPolySupport.cubeBesovPositiveScalarDepthAverage Q v j = HCPolySupport.descendantsAverage Q j fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.cubeBesovOscillation R 2 v ^ 2

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

The square root of the depth-j average of squared oscillations, weighted by 3^(s j).

Equations

• HCPolySupport.cubeBesovPositiveScalarDepthSeminorm Q s v j = Real.rpow 3 (s * ↑j) * √(HCPolySupport.cubeBesovPositiveScalarDepthAverage Q v j)

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

The ℓ² aggregation of the weighted positive Besov depth quantities from depth zero through N.

Equations

• HCPolySupport.cubeBesovPositiveScalarPartialSeminormTwo Q s N v = √(∑ j ∈ Finset.range (N + 1), HCPolySupport.cubeBesovPositiveScalarDepthSeminorm Q s v j ^ 2)

theorem HCPolySupport.cubeL2ScalarDepthAverage_nonneg {d : ℕ} (Q : TriadicCube d) (v : Vec d → ℝ) (j : ℕ) : 0 ≤ cubeL2ScalarDepthAverage Q v j

theorem HCPolySupport.cubeL2ScalarDepthSeminorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (v : Vec d → ℝ) (j : ℕ) : 0 ≤ cubeL2ScalarDepthSeminorm Q s v j

theorem HCPolySupport.cubeBesovPositiveScalarDepthAverage_nonneg {d : ℕ} (Q : TriadicCube d) (v : Vec d → ℝ) (j : ℕ) : 0 ≤ cubeBesovPositiveScalarDepthAverage Q v j

theorem HCPolySupport.cubeBesovPositiveScalarDepthSeminorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (v : Vec d → ℝ) (j : ℕ) : 0 ≤ cubeBesovPositiveScalarDepthSeminorm Q s v j

theorem HCPolySupport.sq_cubeL2ScalarDepthSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (v : Vec d → ℝ) (j : ℕ) : cubeL2ScalarDepthSeminorm Q s v j ^ 2 = Real.rpow 3 (s * ↑j) ^ 2 * cubeL2ScalarDepthAverage Q v j

theorem HCPolySupport.sq_cubeL2ScalarPartialSeminormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (v : Vec d → ℝ) : cubeL2ScalarPartialSeminormTwo Q s N v ^ 2 = ∑ j ∈ Finset.range (N + 1), cubeL2ScalarDepthSeminorm Q s v j ^ 2

theorem HCPolySupport.sq_cubeBesovPositiveScalarDepthSeminorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (v : Vec d → ℝ) (j : ℕ) : cubeBesovPositiveScalarDepthSeminorm Q s v j ^ 2 = Real.rpow 3 (s * ↑j) ^ 2 * cubeBesovPositiveScalarDepthAverage Q v j

theorem HCPolySupport.sq_cubeBesovPositiveScalarPartialSeminormTwo {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (v : Vec d → ℝ) : cubeBesovPositiveScalarPartialSeminormTwo Q s N v ^ 2 = ∑ j ∈ Finset.range (N + 1), cubeBesovPositiveScalarDepthSeminorm Q s v j ^ 2

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

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

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

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

theorem HCPolySupport.sqrt_sum_sq_add_le {ι : Type u_1} (s : Finset ι) (A B : ι → ℝ) (hA : ∀ i ∈ s, 0 ≤ A i) (hB : ∀ i ∈ s, 0 ≤ B i) : (∑ i ∈ s, (A i + B i) ^ 2) ^ (1 / 2) ≤ (∑ i ∈ s, A i ^ 2) ^ (1 / 2) + (∑ i ∈ s, B i ^ 2) ^ (1 / 2)

theorem HCPolySupport.descendantsAverage_L2_add_le {d : ℕ} (Q : TriadicCube d) (j : ℕ) (A B : TriadicCube d → ℝ) (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) ^ 2) ^ (1 / 2) ≤ (descendantsAverage Q j fun (R : TriadicCube d) => A R ^ 2) ^ (1 / 2) + (descendantsAverage Q j fun (R : TriadicCube d) => B R ^ 2) ^ (1 / 2)

theorem HCPolySupport.descendantsAverage_L2_const_mul_eq {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) (F : TriadicCube d → ℝ) (hc : 0 ≤ c) : (descendantsAverage Q j fun (R : TriadicCube d) => (c * F R) ^ 2) ^ (1 / 2) = c * (descendantsAverage Q j fun (R : TriadicCube d) => F R ^ 2) ^ (1 / 2)

theorem HCPolySupport.sqrt_sum_sq_const_mul_eq {ι : Type u_1} (s : Finset ι) (c : ℝ) (F : ι → ℝ) (hc : 0 ≤ c) : √(∑ i ∈ s, (c * F i) ^ 2) = c * √(∑ i ∈ s, F i ^ 2)

theorem HCPolySupport.descendantsAverage_sqrt_const_mul_eq {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) (F : TriadicCube d → ℝ) (hc : 0 ≤ c) : √(descendantsAverage Q j fun (R : TriadicCube d) => (c * F R) ^ 2) = c * √(descendantsAverage Q j fun (R : TriadicCube d) => F R ^ 2)

theorem HCPolySupport.descendantsAverage_sqrt_add_le {d : ℕ} (Q : TriadicCube d) (j : ℕ) (A B : TriadicCube d → ℝ) (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) ^ 2) ≤ √(descendantsAverage Q j fun (R : TriadicCube d) => A R ^ 2) + √(descendantsAverage Q j fun (R : TriadicCube d) => B R ^ 2)

theorem HCPolySupport.sqrt_sum_sq_add_le_sqrt {ι : Type u_1} (s : Finset ι) (A B : ι → ℝ) (hA : ∀ i ∈ s, 0 ≤ A i) (hB : ∀ i ∈ s, 0 ≤ B i) : √(∑ i ∈ s, (A i + B i) ^ 2) ≤ √(∑ i ∈ s, A i ^ 2) + √(∑ i ∈ s, B i ^ 2)

theorem HCPolySupport.sqrt_sum_sq_le_sum {ι : Type u_1} (s : Finset ι) (A : ι → ℝ) (hA : ∀ i ∈ s, 0 ≤ A i) : √(∑ i ∈ s, A i ^ 2) ≤ ∑ i ∈ s, A i

theorem HCPolySupport.sqrt_sum_sq_sum_le_sum_sqrt_sum_sq {ι : Type u_1} {κ : Type u_2} (s : Finset ι) (t : Finset κ) (A : ι → κ → ℝ) (hA : ∀ i ∈ s, ∀ k ∈ t, 0 ≤ A i k) : √(∑ i ∈ s, (∑ k ∈ t, A i k) ^ 2) ≤ ∑ k ∈ t, √(∑ i ∈ s, A i k ^ 2)

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