Coarse-graining support: Support.Sobolev.Fractional.ContinuousInterpolation.RootScaleControl

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

Root-scale control for the sampled continuous K energy

The continuum scale integral omits the endpoint t = 1. This module controls that missing triadic sample directly with the zero H¹ competitor and separates it exactly from the shifted sampled energy.

theorem HCPolySupport.triadicContinuousKSampleTerm_zero_le_sq_normalizedEuclideanLpENorm {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : triadicContinuousKSampleTerm s F 0 ≤ (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 F.toField ^ 2

The endpoint sample at t = 1 is controlled by the square of the exact normalized Euclidean extended L² norm. This is valid in every dimension without extra assumptions.

theorem HCPolySupport.triadicContinuousKSampleEnergy_eq_root_add_shifted {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : triadicContinuousKSampleEnergy s F = triadicContinuousKSampleTerm s F 0 + triadicContinuousKShiftedSampleEnergy s F

The sampled energy is exactly its root sample plus the shifted sampled energy.

theorem HCPolySupport.triadicContinuousKSampleEnergy_le_sq_normalizedEuclideanLpENorm_add_shifted {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : triadicContinuousKSampleEnergy s F ≤ (unitCenteredCubeDomain d).normalizedEuclideanLpENorm 2 F.toField ^ 2 + triadicContinuousKShiftedSampleEnergy s F

The full sampled energy is bounded by the normalized Euclidean L² square plus the shifted sampled energy.