theorem ERealFunction.convexOn_univ_toReal_normPowerEnvelope_of_mem_gammaZero {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ↑(Set.Ioi ⊥)) (γ : PosReal) (p : ↑(Set.Ici 1)) (hf : f ∈ Γ₀(H)) (hp : 1 < ↑p) : _root_.ConvexOn ℝ Set.univ fun (x : H) => (normPowerEnvelope f p γ x).toReal

Proposition 12.15 (1): if f ∈ Γ₀(H), γ ∈ ℝ_{++}, and p > 1, then the real-valued representative of the p-power envelope is convex on H.

theorem ERealFunction.normPowerEnvelope_mem_Ioo_of_mem_gammaZero {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ↑(Set.Ioi ⊥)) (γ : PosReal) (p : ↑(Set.Ici 1)) (hf : f ∈ Γ₀(H)) (hp : 1 < ↑p) (x : H) : normPowerEnvelope f p γ x ∈ Set.Ioo ⊥ ⊤

Proposition 12.15 (2): if f ∈ Γ₀(H), γ ∈ ℝ_{++}, and p > 1, then the p-power envelope is real-valued at every point of H.

theorem ERealFunction.continuous_toReal_normPowerEnvelope_of_mem_gammaZero {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ↑(Set.Ioi ⊥)) (γ : PosReal) (p : ↑(Set.Ici 1)) (hf : f ∈ Γ₀(H)) (hp : 1 < ↑p) : Continuous fun (x : H) => (normPowerEnvelope f p γ x).toReal

Proposition 12.15 (3): if f ∈ Γ₀(H), γ ∈ ℝ_{++}, and p > 1, then the real-valued representative of the p-power envelope is continuous on H.

theorem ERealFunction.exactAt_and_existsUnique_mem_argmin_normPowerEnvelope_of_mem_gammaZero {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (f : H → ↑(Set.Ioi ⊥)) (γ : PosReal) (p : ↑(Set.Ici 1)) (hf : f ∈ Γ₀(H)) (hp : 1 < ↑p) (x : H) : infimalConvolution.ExactAt f (normPowerKernel p γ) x ∧ ∃! y : H, y ∈ Argmin fun (z : H) => ↑(f z) + ↑(normPowerKernel p γ (x - z))

Proposition 12.15 (4): for f ∈ Γ₀(H), γ ∈ ℝ_{++}, p > 1, and every x ∈ H, the infimal convolution defining the p-power regularization is exact at x, and the translated objective y ↦ f y + ‖x - y‖^p / (γ p) has a unique global minimizer.