Coarse-graining support: Support.Sobolev.Fractional.EuclideanWspLocalization

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

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

ENNReal average over the finite set of depth-j descendants.

Equations

• HCPolySupport.descendantsENNAverage Q j F = (↑(HCPolySupport.descendantsAtDepth Q j).card)⁻¹ * ∑ R ∈ HCPolySupport.descendantsAtDepth Q j, F R

theorem HCPolySupport.descendantsENNAverage_lintegral_normalizedCubeMeasure_eq {d : ℕ} (Q : TriadicCube d) (j : ℕ) (f : Vec d → ENNReal) : (descendantsENNAverage Q j fun (R : TriadicCube d) => ∫⁻ (x : Vec d), f x ∂normalizedCubeMeasure R) = ∫⁻ (x : Vec d), f x ∂normalizedCubeMeasure Q

Exact descendant partition identity for a first-variable normalized nonnegative integrand.

theorem HCPolySupport.descendantsENNAverage_normalizedEuclideanLpENorm_rpow_eq {d n : ℕ} (Q : TriadicCube d) (j : ℕ) (p : ENNReal) (F : Vec d → Vec n) (hp0 : p ≠ 0) (hpt : p ≠ ⊤) : (descendantsENNAverage Q j fun (R : TriadicCube d) => (cubeBoundedMeasurableDomain R).normalizedEuclideanLpENorm p F ^ p.toReal) = (cubeBoundedMeasurableDomain Q).normalizedEuclideanLpENorm p F ^ p.toReal

The exact finite-exponent Euclidean normalized Lᵖ descendant partition.

theorem HCPolySupport.descendant_scale_weight_algebra {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (s : ℝ) (p : ENNReal) (hs : 0 ≤ s) : ENNReal.ofReal (cubeScaleFactor R) ^ (-s * p.toReal) = ENNReal.ofReal 3 ^ (↑j * s * p.toReal) * ENNReal.ofReal (cubeScaleFactor Q) ^ (-s * p.toReal)

Exact change of the anchored p-power scale weight down j triadic levels. The factor is the manuscript's 3^(j*s*p).

theorem HCPolySupport.descendantsENNAverage_full_power_le_of_partition {d : ℕ} (Q : TriadicCube d) (j : ℕ) (A : ENNReal) (w L S : TriadicCube d → ENNReal) (hA : 1 ≤ A) (hw : ∀ R ∈ descendantsAtDepth Q j, w R = A * w Q) (hL : descendantsENNAverage Q j L = L Q) (hS : descendantsENNAverage Q j S ≤ S Q) : (descendantsENNAverage Q j fun (R : TriadicCube d) => w R * L R + S R) ≤ A * (w Q * L Q + S Q)

Pure ENNReal assembly of the full-norm power localization. The three inputs are exactly: local physical-scale weights, normalized Lᵖ powers, and fractional seminorm powers.

theorem HCPolySupport.descendantsENNAverage_cubeEuclideanWspESeminorm_rpow_le {d : ℕ} (Q : TriadicCube d) (j : ℕ) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) : (descendantsENNAverage Q j fun (R : TriadicCube d) => cubeEuclideanWspESeminorm R s p F ^ p.exponent.toReal) ≤ cubeEuclideanWspESeminorm Q s p F ^ p.exponent.toReal

theorem HCPolySupport.descendantsENNAverage_cubeEuclideanWspFullENorm_rpow_le {d : ℕ} (Q : TriadicCube d) (j : ℕ) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) : (descendantsENNAverage Q j fun (R : TriadicCube d) => cubeEuclideanWspFullENorm R s p F ^ p.exponent.toReal) ≤ ENNReal.ofReal 3 ^ (↑j * ↑s * p.exponent.toReal) * cubeEuclideanWspFullENorm Q s p F ^ p.exponent.toReal

theorem HCPolySupport.descendantsENNAverage_cubeEuclideanWspFullENorm_root_le {d : ℕ} (Q : TriadicCube d) (j : ℕ) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) : (descendantsENNAverage Q j fun (R : TriadicCube d) => cubeEuclideanWspFullENorm R s p F ^ p.exponent.toReal) ^ p.exponent.toReal⁻¹ ≤ ENNReal.ofReal 3 ^ (↑j * ↑s) * cubeEuclideanWspFullENorm Q s p F

Rooted form of positive Euclidean W^{s,p} descendant localization.