Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ExactOverlapFinitePDepthTriangle

Coarse-graining support: Support.Sobolev.Fractional.ExactOverlapFinitePDepthTriangle #

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

Finite-p exact-overlap depth triangle inequality #

At one overlap depth, the powered direct Euclidean energy is stable under addition with the usual two-term finite-p constant. The proof keeps the average identity and the local Minkowski step on each overlap cube, before summing, so no center-cardinality loss is introduced.

source
noncomputable def HCPolySupport.exactOverlapDepthTriangleConstant (p : FiniteLpExponent) :
ENNReal

The finite-p two-term constant after raising the Minkowski inequality to the p-th power.

Equations
Instances For
    source
    theorem HCPolySupport.cubeEuclideanPositiveBesovOverlapDepthENorm_add_rpow_le {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) (F G : Vec d → Vec d) (j : ℕ) (hF : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (F x)) p.exponent (normalizedCubeMeasure Q)) (hG : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (G x)) p.exponent (normalizedCubeMeasure Q)) :
    cubeEuclideanPositiveBesovOverlapDepthENorm Q p (fun (x : Vec d) => F x + G x) j ^ p.exponent.toReal ≤ exactOverlapDepthTriangleConstant p * (cubeEuclideanPositiveBesovOverlapDepthENorm Q p F j ^ p.exponent.toReal + cubeEuclideanPositiveBesovOverlapDepthENorm Q p G j ^ p.exponent.toReal)

    The powered direct exact-overlap energy at one depth obeys a triangle inequality with a constant depending only on the finite exponent.

    source
    theorem HCPolySupport.cubeEuclideanPositiveBesovOverlapDepthENorm_sub_add_rpow_le {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) (F G : Vec d → Vec d) (j : ℕ) (hF : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (F x)) p.exponent (normalizedCubeMeasure Q)) (hG : MeasureTheory.MemLp (fun (x : Vec d) => HilbertVec.ofVec (G x)) p.exponent (normalizedCubeMeasure Q)) :
    cubeEuclideanPositiveBesovOverlapDepthENorm Q p F j ^ p.exponent.toReal ≤ exactOverlapDepthTriangleConstant p * (cubeEuclideanPositiveBesovOverlapDepthENorm Q p (fun (x : Vec d) => F x - G x) j ^ p.exponent.toReal + cubeEuclideanPositiveBesovOverlapDepthENorm Q p G j ^ p.exponent.toReal)

    The one-depth decomposition form of the finite-p triangle inequality.