Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ContinuousInterpolation.UnitCubeGeometry

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

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

Geometry of the unit centered cube for continuous interpolation #

This module gathers convention-neutral domain, measure, and metric facts for the exact continuous interpolation theorem. The analytic domain is the open centered unit cube; the normalized measure retains the canonical half-open cube carrier.

source
@[reducible, inline]
abbrev HCPolySupport.unitCenteredOpenCubeSet (d : ℕ) :
Set (Vec d)

The source-facing open realization of the centered unit cube.

Equations
Instances For
    source
    theorem HCPolySupport.isOpenBoundedConvexDomain_unitCenteredOpenCubeSet (d : ℕ) :
    IsOpenBoundedConvexDomain (unitCenteredOpenCubeSet d)

    The analytic unit cube is open, bounded, and convex in every dimension.

    source
    @[simp]
    theorem HCPolySupport.cubeVolume_originCube_zero (d : ℕ) :
    cubeVolume (originCube d 0) = 1

    The centered unit triadic cube has literal volume one.

    source
    @[simp]
    theorem HCPolySupport.volume_cubeSet_originCube_zero (d : ℕ) :
    MeasureTheory.volume (cubeSet (originCube d 0)) = 1

    The half-open centered unit cube has Lebesgue volume one.

    source
    @[simp]
    theorem HCPolySupport.volume_openCubeSet_originCube_zero (d : ℕ) :
    MeasureTheory.volume (unitCenteredOpenCubeSet d) = 1

    The source-facing open centered unit cube has Lebesgue volume one.

    source
    theorem HCPolySupport.unitCenteredCubeDomain_restrictedVolume_eq_cubeMeasure (d : ℕ) :
    (unitCenteredCubeDomain d).restrictedVolume = cubeMeasure (originCube d 0)

    The exact unit-cube domain's restricted volume is the canonical cube measure.

    source
    theorem HCPolySupport.unitCenteredCubeDomain_normalizedVolume_eq_normalizedCubeMeasure (d : ℕ) :
    (unitCenteredCubeDomain d).normalizedVolume = normalizedCubeMeasure (originCube d 0)

    The exact unit-cube normalized volume is the canonical normalized cube measure.

    source
    theorem HCPolySupport.unitCenteredCubeDomain_restrictedVolume_eq_restrict_openCubeSet (d : ℕ) :
    (unitCenteredCubeDomain d).restrictedVolume = MeasureTheory.volume.restrict (unitCenteredOpenCubeSet d)

    The exact unit-cube restricted volume can equivalently be read on the source-facing open cube.

    source
    theorem HCPolySupport.cubeSet_originCube_zero_ae_eq_unitCenteredOpenCubeSet (d : ℕ) :
    cubeSet (originCube d 0) =ᵐ[MeasureTheory.volume] unitCenteredOpenCubeSet d

    The half-open and open centered unit cubes agree almost everywhere.

    source
    theorem HCPolySupport.norm_le_euclideanNorm {d : ℕ} (x : Vec d) :
    ‖x‖ ≤ euclideanNorm x

    The project ambient (sup) norm is bounded by the explicit Euclidean magnitude.

    source
    theorem HCPolySupport.euclideanNorm_le_dimension_mul_norm {d : ℕ} (x : Vec d) :
    euclideanNorm x ≤ ↑d * ‖x‖

    The Euclidean magnitude is bounded by a dimension-only multiple of the project ambient (sup) norm. This formulation remains valid at d = 0.

    source
    theorem HCPolySupport.dist_le_euclideanDist {d : ℕ} (x y : Vec d) :
    dist x y ≤ euclideanDist x y

    The project ambient distance is bounded by the explicit Euclidean distance.

    source
    theorem HCPolySupport.euclideanDist_le_dimension_mul_dist {d : ℕ} (x y : Vec d) :
    euclideanDist x y ≤ ↑d * dist x y

    The Euclidean distance is bounded by a dimension-only multiple of the project ambient distance. This formulation remains valid at d = 0.