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

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

Triadic sample series for the continuous K-energy

This module assembles the disjoint triadic scale intervals into an ENNReal series. The lower comparison is deliberately indexed from j + 1: the continuous scale integral alone cannot recover the endpoint sample at t = 1.

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

The canonical weighted triadic sample at t_j = 3^{-j}.

Equations

• One or more equations did not get rendered due to their size.

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

The canonical ENNReal triadic sampled energy. Its weights are the scale form of 3^(2 s j) K(3^{-j},F)^2.

Equations

• HCPolySupport.triadicContinuousKSampleEnergy s F = ∑' (j : ℕ), HCPolySupport.triadicContinuousKSampleTerm s F j

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

The shifted sampled energy, excluding only the endpoint sample at t=1.

Equations

• HCPolySupport.triadicContinuousKShiftedSampleEnergy s F = ∑' (j : ℕ), HCPolySupport.triadicContinuousKSampleTerm s F (j + 1)

noncomputable def HCPolySupport.triadicContinuousKLowerSeriesConstant (s : ↑FractionalOrder) : ENNReal

The explicit lower comparison constant for base-three intervals.

Equations

• HCPolySupport.triadicContinuousKLowerSeriesConstant s = ENNReal.ofReal (2 / 3) * ENNReal.ofReal (Real.rpow 3 (-2 * ↑s))

noncomputable def HCPolySupport.triadicContinuousKUpperSeriesConstant (s : ↑FractionalOrder) : ENNReal

The explicit upper comparison constant for base-three intervals.

Equations

• HCPolySupport.triadicContinuousKUpperSeriesConstant s = ENNReal.ofReal 2 * ENNReal.ofReal (Real.rpow 3 (2 * ↑s))

theorem HCPolySupport.continuousKSeminorm_lintegral_eq_tsum_triadicIntervals {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand (↑s) F t = ∑' (j : ℕ), ∫⁻ (t : ℝ) in triadicContinuousKInterval j, continuousKSeminormIntegrand (↑s) F t

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

The continuum K energy dominates the shifted canonical triadic energy.

theorem HCPolySupport.triadicContinuousKUpperSeriesComparison {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : ∫⁻ (t : ℝ) in Set.Ioo 0 1, continuousKSeminormIntegrand (↑s) F t ≤ triadicContinuousKUpperSeriesConstant s * triadicContinuousKSampleEnergy s F

The continuum K energy is controlled by the canonical triadic sampled energy with an explicit base-three constant.

theorem HCPolySupport.triadicContinuousKLowerSeriesComparison_rpow {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : (triadicContinuousKLowerSeriesConstant s * triadicContinuousKShiftedSampleEnergy s F) ^ (1 / 2) ≤ continuousKSeminorm s F

Square-root form of the shifted lower series comparison.

theorem HCPolySupport.triadicContinuousKUpperSeriesComparison_rpow {d : ℕ} (s : ↑FractionalOrder) (F : UnitCubeEuclideanL2Field d) : continuousKSeminorm s F ≤ (triadicContinuousKUpperSeriesConstant s * triadicContinuousKSampleEnergy s F) ^ (1 / 2)

Square-root form of the upper series comparison.