SandwichNondegeneracyAttainment

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

Attainment of the affine minimum on the §4.3 consumption class

AffineMinimizerExistence.lean proves attainment of ℓ(u,W) = argmin_{ℓ ∈ 𝕃} ‖u − ℓ‖_{L²(W)} on every window carrying the two-sided parameter-space nondegeneracy

c₀ ‖(c,g)‖ ≤ ‖c + g·x‖_{L²(W)} ≤ K ‖(c,g)‖        (hlb / hub),      c₀ > 0 ,

It also records the residual: the §4.3 consumption sites are the truncated windows U_j = (x + □_j) ∩ □_m, whose only stated geometry is the sandwich `x

• □_{j-2} ⊆ U_j ⊆ y + □_j, and on such a window hlb/hub` are theorems --- reachable only through the exact cube second moment.

This module closes that residual. hub is the crude sup bound on the outer cube; hlb combines

• the exact cube second moment on the inner cube (CubeMoments.lean), which gives both |c + g·x| ≤ ‖c + g·x‖_{L²(□in)} and (Lin/(2√3))|g| ≤ ‖c + g·x‖_{L²(□in)},
• the volume-ratio transfer normalizedL2On_le_of_subset from □in to W, and
• the recentring |c| ≤ |c + g·x| + |x||g|, which converts the two cube bounds into a bound on the parameter norm ‖(c,g)‖ = max(|c|, ‖g‖_∞).

The outcome is exists_isAffineMinimizer_of_cubeSandwich: attainment is unconditional on the consumption class, with the explicit constants lbConst and ubConst.

Scope, honestly

Attainment needs only that W is sandwiched between some two axis-parallel (resp. triadic) cubes of positive side; the scale relation Lin = 3^{-2} Lout of the paper's sandwich is not used here and is therefore not a hypothesis. It is used by SandwichNondegeneracy.lean, whose constants must be scale-free across the window family. Note also that lbConst and ubConst are not scale invariant: they involve the position of the window (‖zout‖, |x|), because the parameter norm ‖(c,g)‖ adds an intercept to a slope. That is intrinsic to the direct method's coercivity hypothesis, not a defect; the scale-invariant form is hnd.

References

• ABK26, e.excess.def (the min/argmin).

Euclidean versus sup norm on Vec d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.norm_le_slopeMagnitude {d : ℕ} (g : HCPolySupport.Vec d) : ‖g‖ ≤ Support.slopeMagnitude g

The ambient (sup) norm of a slope is dominated by its Euclidean norm.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.abs_vecDot_le_slopeMagnitude_mul {d : ℕ} (x y : HCPolySupport.Vec d) : |HCPolySupport.vecDot x y| ≤ Support.slopeMagnitude x * Support.slopeMagnitude y

Cauchy--Schwarz in the Euclidean norm of Vec d.

A pointwise bound bounds the normalized seminorm

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_le_of_abs_le {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hWm : MeasurableSet W) (hW : 0 < (MeasureTheory.volume W).toReal) (hfin : MeasureTheory.volume W ≠ ⊤) {f : HCPolySupport.Vec d → ℝ} {M : ℝ} (hM : 0 ≤ M) (hf2 : MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => f x ^ 2) W MeasureTheory.volume) (hle : ∀ x ∈ W, |f x| ≤ M) : Support.normalizedL2On W f ≤ M

If |f| ≤ M on W then ‖f‖_{L²(W)} ≤ M.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.abs_affineEval_le_of_mem_axisCube {d : ℕ} {zout : HCPolySupport.Vec d} {Lout : ℝ} (hLout : 0 < Lout) (c : ℝ) (g : HCPolySupport.Vec d) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.axisCube zout Lout) : |Support.affineEval c g x| ≤ |c| + ↑d * (‖g‖ * (‖zout‖ + Lout))

An affine function is bounded on an axis-parallel cube, with an explicit bound.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memLp_affineEval_of_sandwich {d : ℕ} {W : Set (HCPolySupport.Vec d)} {zout : HCPolySupport.Vec d} {Lout : ℝ} (hLout : 0 < Lout) (hWm : MeasurableSet W) (hout : W ⊆ HCPolySupport.axisCube zout Lout) (c : ℝ) (g : HCPolySupport.Vec d) : MeasureTheory.MemLp (Support.affineEval c g) 2 (MeasureTheory.volume.restrict W)

haff: the affine functions are square-integrable on a bounded window. On a window contained in a bounded cube every affine function is bounded, hence in L². This discharges the haff hypothesis of exists_isAffineMinimizer_of_nondegenerate.

The two parameter-space constants

def Algsuperdiff.Section4.Provider.ExcessDecay.ubConst (d : ℕ) (zout : HCPolySupport.Vec d) (Lout : ℝ) : ℝ

The hub constant of a sandwich: K = 1 + d(‖y‖ + Lout) for the outer cube y + □(Lout).

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.ubConst d zout Lout = 1 + ↑d * (‖zout‖ + Lout)

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.lbConst (d : ℕ) (zin : HCPolySupport.Vec d) (Lin Lout : ℝ) : ℝ

The hlb constant of a sandwich: c₀ = √((Lin/Lout)^d) · min(1, Lin/(2√3)) / (2(1 + |xin|)), with xin the centre of the inner cube. Every factor is explicit: the volume ratio of the sandwich, the sharp cube constant 1/(2√3) from the second moment, and the recentring loss 1 + |xin|.

Equations

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

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ubConst_nonneg {d : ℕ} {zout : HCPolySupport.Vec d} {Lout : ℝ} (hLout : 0 ≤ Lout) : 0 ≤ ubConst d zout Lout

theorem Algsuperdiff.Section4.Provider.ExcessDecay.lbConst_pos {d : ℕ} {zin : HCPolySupport.Vec d} {Lin Lout : ℝ} (hLin : 0 < Lin) (hLout : 0 < Lout) : 0 < lbConst d zin Lin Lout

hub: the affine evaluation map is bounded

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_affineEval_le_of_sandwich {d : ℕ} {W : Set (HCPolySupport.Vec d)} {zin zout : HCPolySupport.Vec d} {Lin Lout : ℝ} (hLin : 0 < Lin) (hLout : 0 < Lout) (hWm : MeasurableSet W) (hin : HCPolySupport.axisCube zin Lin ⊆ W) (hout : W ⊆ HCPolySupport.axisCube zout Lout) (c : ℝ) (g : HCPolySupport.Vec d) : Support.normalizedL2On W (Support.affineEval c g) ≤ ubConst d zout Lout * ‖(c, g)‖

hub. ‖c + g·x‖_{L²(W)} ≤ (1 + d(‖y‖ + Lout))·‖(c,g)‖ on a window contained in the cube y + □(Lout) and containing a cube of positive side.

hlb: the affine evaluation map is bounded below

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2On_affineEval_ge_norm_of_sandwich {d : ℕ} {W : Set (HCPolySupport.Vec d)} {zin zout : HCPolySupport.Vec d} {Lin Lout : ℝ} (hLin : 0 < Lin) (hLout : 0 < Lout) (hin : HCPolySupport.axisCube zin Lin ⊆ W) (hout : W ⊆ HCPolySupport.axisCube zout Lout) (c : ℝ) (g : HCPolySupport.Vec d) : lbConst d zin Lin Lout * ‖(c, g)‖ ≤ Support.normalizedL2On W (Support.affineEval c g)

hlb. c₀ ‖(c,g)‖ ≤ ‖c + g·x‖_{L²(W)} on a sandwiched window, with c₀ = lbConst d zin Lin Lout > 0. Together with hub this says the affine evaluation map is a linear isomorphism onto its image --- the nondegeneracy the direct method needs.

Both cube inputs come from the exact second moment: |c + g·x| ≤ ‖c + g·x‖_{L²(□in)} and (Lin/(2√3))|g| ≤ ‖c + g·x‖_{L²(□in)}.

Attainment on the consumption class

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_isAffineMinimizer_of_axisCubeSandwich {d : ℕ} {W : Set (HCPolySupport.Vec d)} {zin zout : HCPolySupport.Vec d} {Lin Lout : ℝ} (hLin : 0 < Lin) (hLout : 0 < Lout) (hWm : MeasurableSet W) (hin : HCPolySupport.axisCube zin Lin ⊆ W) (hout : W ⊆ HCPolySupport.axisCube zout Lout) (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 on a window sandwiched between two axis-parallel cubes. The infimum defining affineExcessRaw W u is a minimum: some affine parameter pair is an IsAffineMinimizer.

This is exists_isAffineMinimizer_of_nondegenerate with all three of its analytic inputs discharged from the sandwich geometry, at the explicit constants lbConst and ubConst.