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

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

Approximate competitors for the continuous K-functional

This file records convention-neutral consequences of the definition of the continuous K-functional as a real infimum. The infimum need not be attained: every positive error admits a genuine ContinuousKCompetitor whose value lies within that error of the infimum.

theorem HCPolySupport.exists_continuousKCompetitor_value_lt_add {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) {ε : ℝ} (hε : 0 < ε) : ∃ (G : ContinuousKCompetitor d), continuousKFunctionalCompetitorValue t F G < continuousKFunctional t F + ε

Every positive error admits a genuine competitor whose value is strictly less than the continuous K-functional plus that error. This does not assert that the infimum is attained.

theorem HCPolySupport.exists_continuousKCompetitor_value_le_add {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) {ε : ℝ} (hε : 0 < ε) : ∃ (G : ContinuousKCompetitor d), continuousKFunctionalCompetitorValue t F G ≤ continuousKFunctional t F + ε

Non-strict version of exists_continuousKCompetitor_value_lt_add.

theorem HCPolySupport.exists_continuousKCompetitor_value_lt_of_continuousKFunctional_lt {d : ℕ} (t : ↑ContinuousKScale) (F : UnitCubeEuclideanL2Field d) {a : ℝ} (h : continuousKFunctional t F < a) : ∃ (G : ContinuousKCompetitor d), continuousKFunctionalCompetitorValue t F G < a

A strict upper bound on the continuous K-functional contains the value of a genuine competitor.