Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ContinuousInterpolation.ContinuumSampleClosure

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

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

Closure of the continuum and sampled continuous K energies #

This module reinserts the root triadic sample into the lower continuum-series comparison, without applying any real-valued totalization to the energies.

source
theorem HCPolySupport.triadicContinuousKLowerSeriesConstant_pos (s : ↑FractionalOrder) :
0 < triadicContinuousKLowerSeriesConstant s

The lower triadic-series factor is strictly positive.

source
theorem HCPolySupport.triadicContinuousKLowerSeriesConstant_ne_zero (s : ↑FractionalOrder) :
triadicContinuousKLowerSeriesConstant s ≠ 0

The lower triadic-series factor is nonzero.

source
theorem HCPolySupport.triadicContinuousKLowerSeriesConstant_ne_top (s : ↑FractionalOrder) :
triadicContinuousKLowerSeriesConstant s ≠ ⊤

The lower triadic-series factor is finite.

source
theorem HCPolySupport.triadicContinuousKLowerSeriesConstant_inv_ne_top (s : ↑FractionalOrder) :
(triadicContinuousKLowerSeriesConstant s)⁻¹ ≠ ⊤

The inverse lower triadic-series factor is finite.

source
theorem HCPolySupport.triadicContinuousKShiftedSampleEnergy_le_lowerSeriesConstant_inv_mul_continuumEnergy {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
triadicContinuousKShiftedSampleEnergy s F ≤ (triadicContinuousKLowerSeriesConstant s)⁻¹ * ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand (↑s) F t

The shifted sampled energy is controlled by the continuum K energy after dividing through by the strictly positive finite lower series factor.

source
theorem HCPolySupport.triadicSampleEnergy_le_sq_LpNorm_add_inverseSeriesConstant_mul_continuumEnergy {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) :
triadicContinuousKSampleEnergy s F ≤ (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 F.toField ^ 2 + (triadicContinuousKLowerSeriesConstant s)⁻¹ * ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand (↑s) F t

The full sampled continuous K energy is controlled by the normalized Euclidean L² energy and the continuum K energy.