Coarse-graining support:

Support.Sobolev.Fractional.ContinuousInterpolation.PositiveDimensionalComposition

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

Positive-dimensional composition of exact finite-energy bridges

This module composes the finite-energy arrows in the positive-dimensional, measurable-representative lane. It does not introduce a source-facing full norm comparison.

noncomputable def HCPolySupport.positiveDimensionalDiscreteToHsTailConstant (s : ↑FractionalOrder) (d : ℕ) : ENNReal

The finite constant for the sample-energy to Euclidean-energy direction, apart from the continuous/discrete series bridge factor.

Equations

• HCPolySupport.positiveDimensionalDiscreteToHsTailConstant s d = ENNReal.ofReal (HCPolySupport.discreteKOverlapAveragingConstant d ^ 2) * (↑d * (2 * 3 ^ d)) * ENNReal.ofReal (↑d ^ (↑d + 2 * ↑s))

noncomputable def HCPolySupport.positiveDimensionalHsToDiscreteTailConstant (d : ℕ) : ENNReal

The finite constant for the Euclidean-energy to discrete-energy direction, apart from the continuous/discrete series bridge factor.

Equations

• HCPolySupport.positiveDimensionalHsToDiscreteTailConstant d = ↑d * HCPolySupport.Gagliardo.gagliardoBesovLowerConstant d ^ 2 * ENNReal.ofReal (HCPolySupport.overlapDiscreteKConstant d ^ 2)

theorem HCPolySupport.positiveDimensionalDiscreteToHsTailConstant_lt_top (s : ↑FractionalOrder) (d : ℕ) : positiveDimensionalDiscreteToHsTailConstant s d < ⊤

theorem HCPolySupport.positiveDimensionalHsToDiscreteTailConstant_lt_top (d : ℕ) : positiveDimensionalHsToDiscreteTailConstant d < ⊤

noncomputable def HCPolySupport.positiveDimensionalSampleToHsConstant (s : ↑FractionalOrder) (d : ℕ) : ENNReal

The full finite sample-energy to Euclidean-energy composition constant.

Equations

• HCPolySupport.positiveDimensionalSampleToHsConstant s d = ENNReal.ofReal (HCPolySupport.continuousDiscreteKBridgeConstant d ^ 2) * HCPolySupport.positiveDimensionalDiscreteToHsTailConstant s d

noncomputable def HCPolySupport.positiveDimensionalHsToSampleConstant (d : ℕ) : ENNReal

The full finite Euclidean-energy to sample-energy composition constant.

Equations

• HCPolySupport.positiveDimensionalHsToSampleConstant d = HCPolySupport.positiveDimensionalHsToDiscreteTailConstant d * ENNReal.ofReal (HCPolySupport.continuousDiscreteKBridgeConstant d ^ 2)

theorem HCPolySupport.positiveDimensionalSampleToHsConstant_lt_top (s : ↑FractionalOrder) (d : ℕ) : positiveDimensionalSampleToHsConstant s d < ⊤

theorem HCPolySupport.positiveDimensionalHsToSampleConstant_lt_top (d : ℕ) : positiveDimensionalHsToSampleConstant d < ⊤

theorem HCPolySupport.euclideanHsEnergy_le_mul_triadicContinuousKSampleEnergy {d : ℕ} [NeZero d] (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (hFmeas : Measurable F.toField) : euclideanHsEnergy s F ≤ positiveDimensionalHsToSampleConstant d * triadicContinuousKSampleEnergy s F

In positive dimension, the exact sampled continuous K-energy controls the exact Euclidean H^s energy through the four finite bridge layers.

theorem HCPolySupport.triadicContinuousKSampleEnergy_le_mul_euclideanHsEnergy {d : ℕ} [NeZero d] (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (hFmeas : Measurable F.toField) : triadicContinuousKSampleEnergy s F ≤ positiveDimensionalSampleToHsConstant s d * euclideanHsEnergy s F

In positive dimension, the exact Euclidean H^s energy controls the exact sampled continuous K-energy through the same finite bridge layers.