theorem helperForLemma33_0_5_fixedRadiusLocalInfimum_productInfimum_nonexceptionalBound {n : ℕ} (ε : { r : ℝ // 0 < r }) {f : (Fin n → ℝ) → EReal} {x y : Fin n → ℝ} {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (h₁ : ⨅ (w : { w : Fin n → ℝ // ‖w - x‖ < ↑ε }), f ↑w ≠ ⊥ ∨ ⨅ (w : { w : Fin n → ℝ // ‖w - y‖ < ↑ε }), f ↑w ≠ ⊤) (h₂ : ⨅ (w : { w : Fin n → ℝ // ‖w - x‖ < ↑ε }), f ↑w ≠ ⊤ ∨ ⨅ (w : { w : Fin n → ℝ // ‖w - y‖ < ↑ε }), f ↑w ≠ ⊥) : ⨅ (p : { w : Fin n → ℝ // ‖w - x‖ < ↑ε } × { w : Fin n → ℝ // ‖w - y‖ < ↑ε }), ↑a * f ↑p.1 + ↑b * f ↑p.2 ≤ (↑a * ⨅ (w : { w : Fin n → ℝ // ‖w - x‖ < ↑ε }), f ↑w) + ↑b * ⨅ (w : { w : Fin n → ℝ // ‖w - y‖ < ↑ε }), f ↑w

Helper for Lemma33.0.5: outside the two mixed (⊥, ⊤) corners, the product-indexed infimum of weighted endpoint values is bounded by the weighted sum of the endpoint local infima.

theorem helperForLemma33_0_5_fixedRadiusLocalInfimum_preserves_convexity {n : ℕ} (ε : { r : ℝ // 0 < r }) {f : (Fin n → ℝ) → EReal} (hConv : IsERealConvexOn Set.univ f) : IsERealConvexOn Set.univ fun (x : Fin n → ℝ) => ⨅ (w : { w : Fin n → ℝ // ‖w - x‖ < ↑ε }), f ↑w

Helper for Lemma33.0.5: at a fixed radius, local infima preserve convexity.

theorem helperForLemma33_0_5_fixedRadiusLocalInfimum_convexFunction {n : ℕ} (ε : { r : ℝ // 0 < r }) {f : (Fin n → ℝ) → EReal} (hConv : IsERealConvexOn Set.univ f) : ConvexFunction fun (x : Fin n → ℝ) => ⨅ (w : { w : Fin n → ℝ // ‖w - x‖ < ↑ε }), f ↑w

Helper for Lemma33.0.5: at a fixed radius, local infima have a convex epigraph.

theorem helperForLemma33_0_5_fixedRadiusLocalInfimum_preserves_parameterConcavity {m n : ℕ} (ε : { r : ℝ // 0 < r }) (v : Fin n → ℝ) {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hConc : ∀ (w : Fin n → ℝ), IsERealConcaveOn Set.univ fun (u : Fin m → ℝ) => K u w) : IsERealConcaveOn Set.univ fun (u : Fin m → ℝ) => ⨅ (w : { w : Fin n → ℝ // ‖w - v‖ < ↑ε }), K u ↑w

Helper for Lemma33.0.5: at a fixed radius in the second variable, local infima preserve concavity in the first variable.

theorem helperForLemma33_0_5_fixedRadiusLocalSupremum_preserves_parameterConvexity {m n : ℕ} (ε : { r : ℝ // 0 < r }) (u : Fin m → ℝ) {K : (Fin m → ℝ) → (Fin n → ℝ) → EReal} (hConv : ∀ (w : Fin m → ℝ), IsERealConvexOn Set.univ fun (v : Fin n → ℝ) => K w v) : IsERealConvexOn Set.univ fun (v : Fin n → ℝ) => ⨆ (w : { w : Fin m → ℝ // ‖w - u‖ < ↑ε }), K (↑w) v

Helper for Lemma33.0.5: at a fixed radius in the first variable, local suprema preserve convexity in the second variable.

theorem helperForLemma33_0_5_functionConcaveClosure_preserves_concavity {n : ℕ} {f : (Fin n → ℝ) → EReal} (hConc : IsERealConcaveOn Set.univ f) : IsERealConcaveOn Set.univ fun (x : Fin n → ℝ) => ⨅ (ε : { r : ℝ // 0 < r }), ⨆ (w : { w : Fin n → ℝ // ‖w - x‖ < ↑ε }), f ↑w

Helper for Lemma33.0.5: the one-variable concave closure obtained from local suprema remains concave.

theorem helperForLemma33_0_5_functionConvexClosure_convexFunction {n : ℕ} {f : (Fin n → ℝ) → EReal} (hConv : IsERealConvexOn Set.univ f) : ConvexFunction fun (x : Fin n → ℝ) => ⨆ (ε : { r : ℝ // 0 < r }), ⨅ (w : { w : Fin n → ℝ // ‖w - x‖ < ↑ε }), f ↑w

Helper for Lemma33.0.5: the one-variable convex closure obtained from local infima remains convex.

theorem helperForLemma33_0_5_functionConvexClosure_raw_idempotent {n : ℕ} {f : (Fin n → ℝ) → EReal} (x : Fin n → ℝ) : ⨆ (δ : { r : ℝ // 0 < r }), ⨅ (z : { z : Fin n → ℝ // ‖z - x‖ < ↑δ }), ⨆ (ε : { r : ℝ // 0 < r }), ⨅ (w : { w : Fin n → ℝ // ‖w - ↑z‖ < ↑ε }), f ↑w = ⨆ (ε : { r : ℝ // 0 < r }), ⨅ (w : { w : Fin n → ℝ // ‖w - x‖ < ↑ε }), f ↑w

Helper for Lemma33.0.5: the raw sup-inf closure operator is idempotent.

theorem helperForLemma33_0_5_functionConvexClosure_lowerSemicontinuous {n : ℕ} {f : (Fin n → ℝ) → EReal} : LowerSemicontinuous fun (x : Fin n → ℝ) => ⨆ (ε : { r : ℝ // 0 < r }), ⨅ (w : { w : Fin n → ℝ // ‖w - x‖ < ↑ε }), f ↑w

Helper for Lemma33.0.5: the raw sup-inf closure operator is lower semicontinuous.

theorem helperForLemma33_0_5_functionConvexClosure_raw_le_self {n : ℕ} {f : (Fin n → ℝ) → EReal} (x : Fin n → ℝ) : ⨆ (ε : { r : ℝ // 0 < r }), ⨅ (w : { w : Fin n → ℝ // ‖w - x‖ < ↑ε }), f ↑w ≤ f x

Helper for Lemma33.0.5: the raw sup-inf closure never exceeds the original function, because every ball contains its own center.

theorem helperForLemma33_0_5_functionConvexClosure_top_has_topNeighborhood {n : ℕ} {f : (Fin n → ℝ) → EReal} {y : Fin n → ℝ} (hTopOrBot : ∀ (x : Fin n → ℝ), ⨆ (ε : { r : ℝ // 0 < r }), ⨅ (w : { w : Fin n → ℝ // ‖w - x‖ < ↑ε }), f ↑w = ⊤ ∨ ⨆ (ε : { r : ℝ // 0 < r }), ⨅ (w : { w : Fin n → ℝ // ‖w - x‖ < ↑ε }), f ↑w = ⊥) (hyTop : ⨆ (ε : { r : ℝ // 0 < r }), ⨅ (w : { w : Fin n → ℝ // ‖w - y‖ < ↑ε }), f ↑w = ⊤) : ∃ (δ : { r : ℝ // 0 < r }), ∀ (z : { z : Fin n → ℝ // ‖z - y‖ < ↑δ }), ⨆ (ε : { r : ℝ // 0 < r }), ⨅ (w : { w : Fin n → ℝ // ‖w - ↑z‖ < ↑ε }), f ↑w = ⊤

Helper for Lemma33.0.5: if the raw sup-inf closure takes the value ⊤ at some point and all of its values are already classified into {⊤, ⊥}, then a whole neighborhood is forced to stay at ⊤.

theorem helperForLemma33_0_5_closedImproperConvex_values_top_or_bot {n : ℕ} {g : (Fin n → ℝ) → EReal} (hConv : ConvexFunction g) (hLsc : LowerSemicontinuous g) (hBot : ∃ (x : Fin n → ℝ), g x = ⊥) (x : Fin n → ℝ) : g x = ⊤ ∨ g x = ⊥

Helper for Lemma33.0.5: a lower semicontinuous convex function on univ that already attains ⊥ is improper, so Chapter 2 forces all of its values to lie in {⊤, ⊥}.

theorem helperForLemma33_0_5_topBotValued_rawClosure_eq_bot_implies_everyBall_has_botWitness {n : ℕ} {g : (Fin n → ℝ) → EReal} {x : Fin n → ℝ} (hTopOrBot : ∀ (z : Fin n → ℝ), g z = ⊤ ∨ g z = ⊥) (hRawIdem : ⨆ (ε : { r : ℝ // 0 < r }), ⨅ (w : { w : Fin n → ℝ // ‖w - x‖ < ↑ε }), g ↑w = g x) (hxBot : g x = ⊥) (ε : { r : ℝ // 0 < r }) : ∃ (w : { w : Fin n → ℝ // ‖w - x‖ < ↑ε }), g ↑w = ⊥

Helper for Lemma33.0.5: once a {⊤, ⊥}-valued raw closure equals ⊥ at x, every positive-radius ball around x already contains an exact ⊥ witness.

theorem helperForLemma33_0_5_topNeighborhood_contradicts_botWitnessUnderConvexity {n : ℕ} {g : (Fin n → ℝ) → EReal} {x y : Fin n → ℝ} {a b : ℝ} (hConv : IsERealConvexOn Set.univ g) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (hPosA : 0 < a) {δ : { r : ℝ // 0 < r }} (hTopNeighborhood : ∀ (z : { z : Fin n → ℝ // ‖z - (a • x + b • y)‖ < ↑δ }), g ↑z = ⊤) {w : Fin n → ℝ} (hw : ‖w - x‖ < ↑δ) (hwBot : g w = ⊥) (hyTop : g y = ⊤) : False

Helper for Lemma33.0.5: a strict convex combination of an exact ⊥ witness at the x endpoint and the ⊤ endpoint value at y cannot land inside a neighborhood where the target function is identically ⊤.

theorem helperForLemma33_0_5_functionConvexClosure_mixedBotTop_collapse_from_rawClassification {n : ℕ} {f : (Fin n → ℝ) → EReal} {x y : Fin n → ℝ} {a b : ℝ} (hClosureConv : IsERealConvexOn Set.univ fun (z : Fin n → ℝ) => ⨆ (ε : { r : ℝ // 0 < r }), ⨅ (w : { w : Fin n → ℝ // ‖w - z‖ < ↑ε }), f ↑w) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (hPosA : 0 < a) (_hPosB : 0 < b) (hClosureXBot : ⨆ (ε : { r : ℝ // 0 < r }), ⨅ (w : { w : Fin n → ℝ // ‖w - x‖ < ↑ε }), f ↑w = ⊥) (hClosureYTop : ⨆ (ε : { r : ℝ // 0 < r }), ⨅ (w : { w : Fin n → ℝ // ‖w - y‖ < ↑ε }), f ↑w = ⊤) : ⨆ (ε : { r : ℝ // 0 < r }), ⨅ (w : { w : Fin n → ℝ // ‖w - (a • x + b • y)‖ < ↑ε }), f ↑w = ⊥

Helper for Lemma33.0.5: once the raw sup-inf closure is already known to satisfy Jensen, the mixed (⊥, ⊤) branch collapses by combining top neighborhoods at ⊤ points with exact ⊥ witnesses in every ball around a ⊥ point.

theorem helperForLemma33_0_5_convexFunction_leftBot_rightNotTop_forces_comboBot {n : ℕ} {g : (Fin n → ℝ) → EReal} {x y : Fin n → ℝ} {a b : ℝ} (hConvFun : ConvexFunction g) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (hPosA : 0 < a) (hxBot : g x = ⊥) (hyNeTop : g y ≠ ⊤) : g (a • x + b • y) = ⊥

Helper for Lemma33.0.5: for a convex epigraph, an exact ⊥ left endpoint and any right endpoint different from ⊤ already force every strict convex combination to be ⊥.