AffineMinimizerExistence

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Attainment of the affine minimum ℓ(u,W) (the min/argmin)

e.excess.def writes the excess with a min over the affine functions and names the minimizer ℓ(u,W) = argmin. AffineExcess.lean defines the excess as the sInf of the same competitor set. This module supplies the attainment statement --- the assertion that the sInf is a min --- by the direct method in the (d+1)-dimensional affine parameter space ℝ × Vec d.

What is proved, and on which class

exists_isAffineMinimizer_of_nondegenerate proves attainment on every window W for which

• u ∈ L²(W) and every affine function is in L²(W) (haff), and
• the affine evaluation map is two-sidedly nondegenerate on W: c₀‖(c,g)‖ ≤ ‖c + g·x‖_{L²(W)} ≤ K‖(c,g)‖ with c₀ > 0 (hlb, hub).

That is exactly the hypothesis set the direct method needs: hub gives that the competitor function is K-Lipschitz, hence continuous; hlb gives coercivity; ℝ × Vec d is finite-dimensional, hence proper, so a continuous coercive function attains a global minimum, and a global minimizer of the competitor function realizes the sInf.

Note also that hlb forces 0 < |W|.

The residual, stated precisely (attainment on the consumption class)

The §4.3 consumption sites are not the source's "bounded domains": they are the truncated windows U_j = (x + □_j) ∩ □_m and the abstract nested family of l.iteration.lemma, whose only stated geometry is the sandwich x + □_{j-2} ⊆ U_j ⊆ y + □_j (hypothesis (iii), scoped to j ≤ m per the binding). On such a window hlb/hub are theorems, not assumptions, and the route is fixed and known:

• hub follows from W ⊆ y + □_j and the crude bound |c + g·x| ≤ |c| + |g| · diam, since ‖·‖_{L²(W)} of a bounded function is at most its sup;

Until it is proved, every §4.3 statement in this tree is phrased so that a chosen minimizer's data (c_j, g_j) is quantified, never obtained from a choose on an unavailable attainment: see IterationLemma.lean, whose slope sequence p is a parameter and whose hypotheses are properties of the given minimizers.

References

• ABK26, e.excess.def.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_isAffineMinimizer_of_nondegenerate {d : ℕ} {W : Set (HCPolySupport.Vec d)} {c₀ K : ℝ} (hc₀ : 0 < c₀) (haff : ∀ (c : ℝ) (g : HCPolySupport.Vec d), MeasureTheory.MemLp (Support.affineEval c g) 2 (MeasureTheory.volume.restrict W)) (hlb : ∀ (c : ℝ) (g : HCPolySupport.Vec d), c₀ * ‖(c, g)‖ ≤ Support.normalizedL2On W (Support.affineEval c g)) (hub : ∀ (c : ℝ) (g : HCPolySupport.Vec d), Support.normalizedL2On W (Support.affineEval c g) ≤ K * ‖(c, g)‖) (u : HCPolySupport.Vec d → ℝ) (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict W)) : ∃ (c : ℝ) (g : HCPolySupport.Vec d), Support.IsAffineMinimizer W u c g

Attainment of the affine minimum, on a nondegenerate window.

On a window carrying the two-sided affine nondegeneracy hlb/hub and on which u is square-integrable, the infimum defining affineExcessRaw is attained: some affine parameter pair (c, g) is an IsAffineMinimizer. This is the source's min/argmin, with the hypotheses the statement needs made visible. See the module docstring for the (false) hypothesis-free reading and for the residual on the truncated consumption windows.