Attainment and interior-radius bounds for the kernel's infimal-convolution minimizers.

theorem V7.Stage5AboveTwoLowerResume.continuous_lpNorm {p : ℝ} (hp : 1 ≤ p) {d : ℕ} : Continuous fun (z : Point d) => lpNorm p z

Continuity of the literal finite-dimensional ell_p norm in the ambient product topology.

theorem V7.Stage5AboveTwoLowerResume.isCompact_lpNorm_le {p chi : ℝ} (hp : 1 ≤ p) {d : ℕ} : IsCompact {v : Point d | lpNorm p v ≤ chi}

Closed ell_p balls are compact in the actual finite-dimensional ambient topology used by the V7 carriers.

theorem V7.Stage5AboveTwoLowerResume.continuous_of_isOneLipschitz {d : ℕ} {p : ℝ} (hp : 1 ≤ p) {ell : Point d → ℝ} (hlip : IsOneLipschitz p ell) : Continuous ell

A function that is one-Lipschitz for the literal ell_p norm is continuous in the ambient product topology.

theorem V7.Stage5AboveTwoLowerResume.continuous_smoothingCost {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) {chi : ℝ} {ell : Point d → ℝ} (hp : 1 ≤ p) (hlip : IsOneLipschitz p ell) (hphi : Continuous kernel.phi) (x : Point d) : Continuous (Stage5AboveTwoLower.S5ARepair.smoothingCost kernel chi ell x)

Continuity of the concrete infimal cost follows from the frozen one-Lipschitz input and continuity of the selected kernel.

theorem V7.Stage5AboveTwoLowerResume.lpNorm_le_lpNorm_of_exponent_le {r p : ℝ} (hr : 1 ≤ r) (hrp : r ≤ p) {d : ℕ} (x : Point d) : lpNorm p x ≤ lpNorm r x

Monotonicity of the unnormalised finite-dimensional ell_p norms in the exponent, proved in the literal lpNorm representation used by V7.

theorem V7.Stage5AboveTwoLowerResume.lowerKernelPhi_radial_of_lpNorm_le {p r theta : ℝ} (hr : r ≠ 0) (htheta : 1 < theta) {d : ℕ} (hmono : ∀ (u : Point d), lpNorm p u ≤ lpNorm r u) (u : Point d) : 1 ≤ lpNorm p u → lpNorm p u < lowerKernelPhi r theta u

The concrete kernel has the required all-radii barrier once the standard finite-dimensional monotonicity ‖u‖_p ≤ ‖u‖_r for r ≤ p is available.

theorem V7.Stage5AboveTwoLowerResume.lowerKernelPhi_radial {p r theta : ℝ} (hr : 1 ≤ r) (hrp : r ≤ p) (htheta : 1 < theta) {d : ℕ} (u : Point d) : 1 ≤ lpNorm p u → lpNorm p u < lowerKernelPhi r theta u

Concrete all-radii barrier for the current lowerKernelPhi.

theorem V7.Stage5AboveTwoLowerResume.self_lt_two_mul_rpow_of_three_four_lt {t a : ℝ} (ht : 3 / 4 < t) (ht1 : t ≤ 1) (ha : 0 ≤ a) (ha3 : a < 3) : t < 2 * t ^ a

theorem V7.Stage5AboveTwoLowerResume.lowerKernelPhi_dominates_outer_quarter {p r theta : ℝ} (hr : 1 ≤ r) (hrp : r ≤ p) (htheta : 1 < theta) (hthetaUpper : theta < 5 / 4) {d : ℕ} (u : Point d) (huLower : 3 / 4 < lpNorm p u) (huUpper : lpNorm p u ≤ 1) : lpNorm p u < lowerKernelPhi r theta u

The concrete kernel cost already beats the Lipschitz loss on the fixed outer quarter of the smoothing ball when theta < 5/4.

theorem V7.Stage5AboveTwoLowerResume.exists_infimal_minimizer_of_closed_ball_barrier {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) {chi : ℝ} (hchi : 0 < chi) (ell : Point d → ℝ) (x : Point d) (hp : 1 ≤ p) (hcontinuous : Continuous (Stage5AboveTwoLower.S5ARepair.smoothingCost kernel chi ell x)) (hbarrier : ∀ (v : Point d), chi ≤ lpNorm p v → Stage5AboveTwoLower.S5ARepair.smoothingCost kernel chi ell x 0 < Stage5AboveTwoLower.S5ARepair.smoothingCost kernel chi ell x v) : ∃ (v : Point d), Stage5AboveTwoLower.S5ARepair.IsInfimalMinimizer kernel chi ell x v ∧ lpNorm p v < chi

A continuous smoothing cost whose value outside the closed smoothing ball is strictly larger than the zero-displacement cost has a global minimizer, and every global minimizer lies strictly inside that ball. This is the exact finite-dimensional compact-ball reduction required before the concrete kernel barrier is discharged.

theorem V7.Stage5AboveTwoLowerResume.exists_infimal_minimizer_of_radial_kernel {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) {chi : ℝ} (hchi : 0 < chi) (ell : Point d → ℝ) (x : Point d) (hp : 1 ≤ p) (hlip : IsOneLipschitz p ell) (hphi : Continuous kernel.phi) (hphi0 : kernel.phi 0 = 0) (hradial : ∀ (u : Point d), 1 ≤ lpNorm p u → lpNorm p u < kernel.phi u) : ∃ (v : Point d), Stage5AboveTwoLower.S5ARepair.IsInfimalMinimizer kernel chi ell x v ∧ lpNorm p v < chi

The compact-ball theorem specialized to the radial barrier used by the V7 smoothing kernel. The remaining concrete kernel obligation is precisely to prove this radial inequality from lowerKernelPhi and r0 ≤ p.

theorem V7.Stage5AboveTwoLowerResume.exists_infimal_minimizer_lowerKernelPhi {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) {r theta chi : ℝ} (hr : 2 < r) (hrp : r ≤ p) (htheta : 1 < theta) (htr : 2 * theta < r) (hchi : 0 < chi) (hkernelPhi : kernel.phi = lowerKernelPhi r theta) (ell : Point d → ℝ) (hlip : IsOneLipschitz p ell) (x : Point d) : ∃ (v : Point d), Stage5AboveTwoLower.S5ARepair.IsInfimalMinimizer kernel chi ell x v ∧ lpNorm p v < chi

Finite-dimensional attainment and strict interiority for the actual kernel selected by the Stage-5 construction.

theorem V7.Stage5AboveTwoLowerResume.exists_infimal_minimizer_lowerKernelPhi_with_margin {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) {r theta chi : ℝ} (hr : 2 < r) (hrp : r ≤ p) (htheta : 1 < theta) (hthetaUpper : theta < 5 / 4) (htr : 2 * theta < r) (hchi : 0 < chi) (hkernelPhi : kernel.phi = lowerKernelPhi r theta) (ell : Point d → ℝ) (hlip : IsOneLipschitz p ell) (x : Point d) : ∃ (v : Point d), Stage5AboveTwoLower.S5ARepair.IsInfimalMinimizer kernel chi ell x v ∧ lpNorm p v ≤ chi - chi / 4

The actual minimizer can be chosen with the uniform outer-quarter margin ‖v‖_p ≤ 3 chi / 4, independently of the centre and of the one-Lipschitz objective.

theorem V7.Stage5AboveTwoLowerResume.localSmoothingValue_bounds_lowerKernelPhi {p : ℝ} {d : ℕ} (kernel : SmoothingKernelData p d) {r theta chi : ℝ} (hr : 2 < r) (hrp : r ≤ p) (htheta : 1 < theta) (htr : 2 * theta < r) (hchi : 0 < chi) (hkernelPhi : kernel.phi = lowerKernelPhi r theta) (ell : Point d → ℝ) (hlip : IsOneLipschitz p ell) (x : Point d) : ell x - chi ≤ localSmoothingValue kernel chi ell x ∧ localSmoothingValue kernel chi ell x ≤ ell x

Exact approximation bounds for the concrete infimal value.