Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ContinuousInterpolation.OverlapGagliardoBridge

Coarse-graining support: Support.Sobolev.Fractional.ContinuousInterpolation.OverlapGagliardoBridge #

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

Extended overlap-Besov and coordinate Gagliardo energies #

This module compares the corrected vector overlap-Besov truncations on the centered unit cube with the finite family of scalar coordinate Gagliardo energies. The overlap energy is defined in ℝ≥0∞ as the supremum of the finite squared truncations; in particular, it never passes through the legacy real-valued sSup seminorm.

The positive-dimensional comparison lemmas below are proof-internal producers. Their explicit measurability, MemLp, and [NeZero d] hypotheses are intended to be discharged later by the measurable-representative and zero-dimensional wrappers, rather than exposed in the final source-facing theorem.

source
noncomputable def HCPolySupport.extendedVectorOverlapBesovEnergy {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
ENNReal

The extended corrected-vector overlap-Besov energy on the centered unit cube.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.overlapBesovEnergy_gagliardoConstant_lt_top (d : ℕ) :
    ↑d * (2 * 3 ^ d) < ⊤

    The explicit dimension factor in the overlap-to-Gagliardo estimate is finite.

    source
    theorem HCPolySupport.coordinateGagliardoEnergy_overlapBesovConstant_lt_top (d : ℕ) :
    ↑d * Gagliardo.gagliardoBesovLowerConstant d ^ 2 < ⊤

    The explicit dimension factor in the Gagliardo-to-overlap estimate is finite.

    source
    @[simp]
    theorem HCPolySupport.cubeBesovScaleWeight_originCube_zero {d : ℕ} (s : ℝ) :
    cubeBesovScaleWeight s (originCube d 0) = 1

    The root-scale correction is exactly one on the centered unit cube.

    source
    theorem HCPolySupport.ofReal_sq_vectorPartialSeminorm_le_extendedVectorOverlapBesovEnergy {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (N : ℕ) :
    ENNReal.ofReal (cubeBesovOverlappingPositiveVectorPartialSeminormTwo (originCube d 0) (↑s) N F.toField ^ 2) ≤ extendedVectorOverlapBesovEnergy s F

    Every squared finite truncation is bounded by the extended overlap-Besov energy.

    source
    theorem HCPolySupport.extendedVectorOverlapBesovEnergy_zero_dim (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field 0) :
    extendedVectorOverlapBesovEnergy s F = 0

    The extended corrected-vector overlap energy vanishes in dimension zero.

    source
    theorem HCPolySupport.coordinateGagliardoEnergy_le_mul_extendedVectorOverlapBesovEnergy {d : ℕ} [NeZero d] (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (hFmeas : Measurable F.toField) (hF : MeasureTheory.MemLp F.toField 2 (normalizedCubeMeasure (originCube d 0))) :
    coordinateGagliardoEnergy s F ≤ ↑d * Gagliardo.gagliardoBesovLowerConstant d ^ 2 * extendedVectorOverlapBesovEnergy s F

    Proof-internal positive-dimensional producer: the coordinate Gagliardo energy is bounded by the extended corrected-vector overlap energy.

    source
    theorem HCPolySupport.extendedVectorOverlapBesovEnergy_le_mul_coordinateGagliardoEnergy {d : ℕ} [NeZero d] (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (hFmeas : Measurable F.toField) (hF : MeasureTheory.MemLp F.toField 2 (normalizedCubeMeasure (originCube d 0))) :
    extendedVectorOverlapBesovEnergy s F ≤ ↑d * (2 * 3 ^ d) * coordinateGagliardoEnergy s F

    Proof-internal positive-dimensional producer: the extended corrected-vector overlap energy is bounded by the coordinate Gagliardo energy.