Documentation

LeanPool.HighContrastHomogenization.Support.Besov.Positive.ExactOverlapEuclideanLp

Coarse-graining support: Support.Besov.Positive.ExactOverlapEuclideanLp #

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

Exact finite-p Euclidean overlap Besov seminorm #

The canonical positive overlap seminorm for vector fields uses Euclidean local oscillations about ScalarOverlap.cubeAverageVec, with a single outer 1 / p root after summing all physical scales.

source
noncomputable def HCPolySupport.cubeEuclideanPositiveBesovOverlapESeminorm {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (g : Vec d → Vec d) :
ENNReal

The canonical positive Euclidean overlap Besov seminorm at finite p. At running depth j, the physical scale is Q.scale - j; the outer root is taken only after the complete weighted scale sum.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.cubeEuclideanPositiveBesovOverlapESeminorm_eq {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (g : Vec d → Vec d) :
    cubeEuclideanPositiveBesovOverlapESeminorm Q s p g = (∑' (j : ℕ), ENNReal.ofReal (Real.rpow 3 (-(↑s * p.exponent.toReal * ↑(Q.scale - ↑j)))) * (↑(ScalarOverlap.centersAtDepth Q j).card)⁻¹ * ∑ S ∈ (ScalarOverlap.centersAtDepth Q j).attach, MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertVec.ofVec (g x - ScalarOverlap.cubeAverageVec (↑S) g)) p.exponent (ScalarOverlap.normalizedCubeMeasure ↑S) ^ p.exponent.toReal) ^ (1 / p.exponent.toReal)

    Formula accessor for the canonical finite-p Euclidean overlap seminorm.

    source
    theorem HCPolySupport.cubeEuclideanPositiveBesovOverlapESeminorm_nonneg {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (g : Vec d → Vec d) :
    0 ≤ cubeEuclideanPositiveBesovOverlapESeminorm Q s p g