Coarse-graining support:

Support.Sobolev.Fractional.ContinuousInterpolation.ContinuousDiscreteKSeriesBridge

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

Triadic continuous/discrete K-series bridge

This module compares the canonical continuous triadic K-sample energy with the extended internal discrete K-functional energy.

theorem HCPolySupport.ofReal_sq_continuousDiscreteKBridgeConstant_ne_top (d : ℕ) : ENNReal.ofReal (continuousDiscreteKBridgeConstant d ^ 2) ≠ ⊤

The squared continuous/discrete bridge factor is finite as an extended nonnegative real.

theorem HCPolySupport.ofReal_sq_cubeKPartialSeminorm_eq_sum_depthTerms {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (N : ℕ) : ENNReal.ofReal (cubeKBesovVectorPartialSeminormTwo (originCube d 0) (↑s) N F.toField ^ 2) = ∑ j ∈ Finset.range (N + 1), ENNReal.ofReal (cubeKBesovVectorDepthSeminorm (originCube d 0) (↑s) F.toField j ^ 2)

The squared discrete partial seminorm is exactly its finite ENNReal sum of depth energies.

theorem HCPolySupport.triadicContinuousKSampleEnergy_le_mul_extendedDiscreteKFunctionalEnergy {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : triadicContinuousKSampleEnergy s F ≤ ENNReal.ofReal (continuousDiscreteKBridgeConstant d ^ 2) * extendedDiscreteKFunctionalEnergy s F

The canonical continuous triadic sample energy is bounded by the extended internal discrete K-functional energy, with the squared bridge constant.

theorem HCPolySupport.extendedDiscreteKFunctionalEnergy_le_mul_triadicContinuousKSampleEnergy {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : extendedDiscreteKFunctionalEnergy s F ≤ ENNReal.ofReal (continuousDiscreteKBridgeConstant d ^ 2) * triadicContinuousKSampleEnergy s F

The extended internal discrete K-functional energy is bounded by the canonical continuous triadic sample energy, with the same squared constant.

theorem HCPolySupport.triadicContinuousKSampleEnergy_ne_top_of_extendedDiscreteKFunctionalEnergy_ne_top {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (hF : extendedDiscreteKFunctionalEnergy s F ≠ ⊤) : triadicContinuousKSampleEnergy s F ≠ ⊤

Finiteness of the extended discrete energy transfers to the continuous triadic sampled energy.

theorem HCPolySupport.extendedDiscreteKFunctionalEnergy_ne_top_of_triadicContinuousKSampleEnergy_ne_top {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) (hF : triadicContinuousKSampleEnergy s F ≠ ⊤) : extendedDiscreteKFunctionalEnergy s F ≠ ⊤

Finiteness of the continuous triadic sampled energy transfers to the extended discrete K-functional energy.

theorem HCPolySupport.triadicContinuousKShiftedSampleEnergy_le_triadicContinuousKSampleEnergy {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : triadicContinuousKShiftedSampleEnergy s F ≤ triadicContinuousKSampleEnergy s F

Discarding the endpoint sample cannot increase the nonnegative triadic sample energy.