Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ContinuousInterpolation.EuclideanGagliardoCoordinateBridge

Coarse-graining support: #

Support.Sobolev.Fractional.ContinuousInterpolation.EuclideanGagliardoCoordinateBridge

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

Euclidean-to-coordinate Gagliardo bridge #

This module fixes the exact product measure and the finite-coordinate numerator decomposition needed to compare the Euclidean H^s energy with the scalar ambient-distance Gagliardo energies.

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

The finite-coordinate family of scalar ambient-distance Gagliardo seminorms at exponent two, squared before summation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.euclideanHsProductMeasure_eq_gagliardoCubeMeasure_originCube_zero (d : ℕ) :
    euclideanHsProductMeasure d = Gagliardo.gagliardoCubeMeasure (originCube d 0)

    The exact Euclidean product measure is the scalar Gagliardo product measure on the origin unit cube.

    source
    theorem HCPolySupport.euclideanHs_numerator_eq_sum_coordinates {d : ℕ} (F : UnitCubeEuclideanL2Field d) (z : Vec d × Vec d) :
    ‖HilbertVec.ofVec (F.toField z.1 - F.toField z.2)‖ ^ 2 = ∑ i : Fin d, (F.toField z.1 i - F.toField z.2 i) ^ 2

    The squared Euclidean target magnitude is the finite sum of squared coordinate differences.

    source
    theorem HCPolySupport.euclideanHsEnergy_zero_dim (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field 0) :
    euclideanHsEnergy s F = 0

    At zero dimension both the exact Euclidean energy and the finite coordinate family vanish, with no positive-dimension instance.

    source
    theorem HCPolySupport.coordinateGagliardoEnergy_zero_dim (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field 0) :
    coordinateGagliardoEnergy s F = 0
    source
    theorem HCPolySupport.coordinateGagliardoEnergy_eq_lintegral_sum {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (hF : Measurable F.toField) :
    coordinateGagliardoEnergy s F = ∫⁻ (z : Vec d × Vec d), ∑ i : Fin d, ‖Gagliardo.gagliardoKernel (↑s) 2 (fun (x : Vec d) => F.toField x i) z‖ₑ ^ 2 ∂Gagliardo.gagliardoCubeMeasure (originCube d 0)

    The coordinate energy is one product-measure lintegral of the finite sum of scalar ambient-distance kernels when the chosen representative is measurable.

    source
    theorem HCPolySupport.coordinateGagliardoEnergy_euclideanHsConstant_lt_top (d : ℕ) (s : ↑FractionalOrder) :
    ENNReal.ofReal (↑d ^ (↑d + 2 * ↑s)) < ⊤

    The explicit metric-comparison constant is finite in every dimension and fractional order.

    source
    theorem HCPolySupport.euclideanHsEnergy_le_coordinateGagliardoEnergy {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (hF : Measurable F.toField) :
    euclideanHsEnergy s F ≤ coordinateGagliardoEnergy s F

    Proof-internal positive-dimensional producer: the exact Euclidean energy is bounded by the finite family of scalar ambient-distance Gagliardo energies.

    source
    theorem HCPolySupport.coordinateGagliardoEnergy_le_mul_euclideanHsEnergy {d : ℕ} [NeZero d] (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (hF : Measurable F.toField) :
    coordinateGagliardoEnergy s F ≤ ENNReal.ofReal (↑d ^ (↑d + 2 * ↑s)) * euclideanHsEnergy s F

    Proof-internal positive-dimensional producer: the coordinate Gagliardo energy is bounded by the exact Euclidean energy with an explicit metric-comparison factor.