theorem mirror_descent_update_objective_add_constant_eq_bregman_form {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (ω : E → EReal) (xk gradf : E) (t : ℝ) : (fun (x : E) => mirror_descent_update_objective (fun (y : E) => (ω y).toReal) xk gradf t x + (inner ℝ (gradient (fun (y : E) => (ω y).toReal) xk) xk - (ω xk).toReal)) = fun (x : E) => inner ℝ (t • gradf) x + B[ω] x xk

The Chapter 9 owner mirror_descent_update_objective differs from the textbook Bregman-form mirror-step objective only by the constant ⟪∇ω(x^k), x^k⟫ - ω(x^k).

theorem isMinOn_mirror_descent_update_objective_iff_isMinOn_bregman_form {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (ω : E → EReal) (C : Set E) (xk xNext gradf : E) (t : ℝ) : xNext ∈ C ∧ IsMinOn (mirror_descent_update_objective (fun (y : E) => (ω y).toReal) xk gradf t) C xNext ↔ xNext ∈ C ∧ IsMinOn (fun (x : E) => inner ℝ (t • gradf) x + B[ω] x xk) C xNext

The canonical Chapter 9 one-step owner and the textbook Bregman-form objective have the same minimizers on C.

theorem effectiveDomain_addIndicator_eq_of_isBregmanPotentialOn {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ω : E → EReal} {C : Set E} {σ : ℝ} (hω : IsBregmanPotentialOn ω C σ) : effective_domain (ω + δ_ C) = C

Helper for Text 9.4: for a Bregman potential on C, the constrained potential ω + δ_ C has effective domain exactly C.

theorem toReal_addIndicator_eq_of_mem {E : Type u} {ω : E → EReal} {C : Set E} {xk : E} (hxC : xk ∈ C) : ((ω + δ_ C) xk).toReal = (ω xk).toReal

Helper for Text 9.4: on feasible points, the constrained potential ω + δ_ C has the same real value as ω.

theorem constrainedPotential_proper_of_mem {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ω : E → EReal} {C : Set E} {σ : ℝ} (hω : IsBregmanPotentialOn ω C σ) {x : E} (hx : x ∈ C) : IsProperExtendedRealFunction (ω + δ_ C)

Helper for Text 9.4: once one feasible point is known, the constrained potential ω + δ_ C is proper.

theorem mirrorDescentBregmanObjective_eq_constrainedPotential_minus_pairing {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → EReal} {C : Set E} {xk gradf : E} {t : ℝ} {x : E} (hx : x ∈ C) : inner ℝ (t • gradf) x + B[ω] x xk = ((ω + δ_ C) x).toReal - inner ℝ (gradient (fun (y : E) => (ω y).toReal) xk - t • gradf) x + (inner ℝ (gradient (fun (y : E) => (ω y).toReal) xk) xk - (ω xk).toReal)

Helper for Text 9.4: on feasible points, the Bregman-form mirror objective is the constrained potential minus the dual pairing with ∇ω(x^k) - t g_f, up to an x-independent constant.

theorem constrainedPotentialGap_iff_mirrorDescentComparison {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → EReal} {C : Set E} {σ : ℝ} {xk xNext gradf : E} {t : ℝ} (hω : IsBregmanPotentialOn ω C σ) {y : E} (hxNext : xNext ∈ C) (hy : y ∈ C) : ↑(inner ℝ (gradient (fun (z : E) => (ω z).toReal) xk - t • gradf) (y - xNext)) ≤ (ω + δ_ C) y - (ω + δ_ C) xNext ↔ inner ℝ (t • gradf) xNext + B[ω] xNext xk ≤ inner ℝ (t • gradf) y + B[ω] y xk

Helper for Text 9.4: on feasible points, the constrained-potential support-gap inequality is exactly the mirror-descent comparison.

theorem constrainedPotential_properClosedConvex {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {ω : E → EReal} {C : Set E} {σ : ℝ} {xk : E} (hC_closed : IsClosed C) (hω : IsBregmanPotentialOn ω C σ) (hxk : xk ∈ C ∩ subdifferential_domain ω) : IsProperExtendedRealFunction (ω + δ_ C) ∧ LowerSemicontinuous (ω + δ_ C) ∧ is_convex_function (ω + δ_ C)

Helper for Text 9.4: the constrained potential ω + δ_ C is proper, lower semicontinuous, and convex under the standing Bregman-potential and closed-feasible-set assumptions.

theorem eval_mem_subdifferential_conjugate_of_mem_subdifferential {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → EReal} (hf_proper : IsProperExtendedRealFunction f) {x : E} {y : Module.Dual ℝ E} (hy : y ∈ ∂f(x)) : (Module.Dual.eval ℝ E) x ∈ ∂conjugate_function f(y)

Helper for Text 9.4: a primal subgradient of f at x yields the bidual evaluation subgradient of conjugate_function f at the same dual vector.

theorem mem_subdifferential_of_eval_mem_subdifferential_conjugate {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf_proper : IsProperExtendedRealFunction f) (hf_closed : LowerSemicontinuous f) (hf_convex : is_convex_function f) {x : E} {y : Module.Dual ℝ E} (hy : (Module.Dual.eval ℝ E) x ∈ ∂conjugate_function f(y)) : y ∈ ∂f(x)

Helper for Text 9.4: under proper/closed/convex hypotheses, conjugate-side evaluation subgradient membership transports back to primal subgradient membership.

theorem conjugateFunctionFiniteEverywhere_of_proper_closed_strongConvexOn {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {σ : ℝ} {f : E → EReal} (hσ : 0 < σ) (hf_proper : IsProperExtendedRealFunction f) (hf_closed : LowerSemicontinuous f) (hstrong : StrongConvexOn (effective_domain f) σ fun (x : E) => (f x).toReal) (y : Module.Dual ℝ E) : conjugate_function f y ≠ ⊥ ∧ conjugate_function f y < ⊤

Helper for Text 9.4: strong convexity of f makes its conjugate finite at every dual vector, transported back from the continuous-dual theorem in Chapter 5.

theorem differentiableAt_primalConjugate_of_proper_closed_strongConvexOn {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {σ : ℝ} {f : E → EReal} (hσ : 0 < σ) (hf_proper : IsProperExtendedRealFunction f) (hf_closed : LowerSemicontinuous f) (hstrong : StrongConvexOn (effective_domain f) σ fun (x : E) => (f x).toReal) (g : E) : DifferentiableAt ℝ (fun (y : E) => (f∗ y).toReal) g

Helper for Text 9.4: the real-valued primal conjugate is differentiable at every point once the constrained potential is proper, closed, and strongly convex.

theorem dualMap_riesz_eval_eq_riesz {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (x : E) : (ContinuousLinearMap.coeLM ℝ ∘ₛₗ ↑(InnerProductSpace.toDual ℝ E).toLinearEquiv).dualMap ((Module.Dual.eval ℝ E) x) = ↑((InnerProductSpace.toDualMap ℝ E) x)

Helper for Text 9.4: pulling back the bidual evaluation functional along the Riesz map gives the primal Riesz functional of the same vector.

theorem primalConjugate_convex {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hconv : is_convex_function (conjugate_function f)) : is_convex_function f∗

Helper for Text 9.4: precomposing a convex conjugate with the Riesz map keeps the primal conjugate f∗ convex on E.

theorem eqAddIffLeftEqSubOfNeBot {a b c : EReal} (ha_ne_bot : a ≠ ⊥) (hb_ne_bot : b ≠ ⊥) (hc_ne_top : c ≠ ⊤) : c = a + b ↔ a = c - b

Helper for Text 9.4: for finite c and non-⊥ summands, the equality c = a + b can be rewritten as a = c - b.

theorem pairingEqAddConjugate_iff_memSubdifferential_ofProper {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → EReal} (hf_proper : IsProperExtendedRealFunction f) (x : E) (y : Module.Dual ℝ E) : ↑(y x) = f x + conjugate_function f y ↔ y ∈ ∂f(x)

Helper for Text 9.4: for a proper extended-real-valued function, Fenchel--Young equality is equivalent to primal subgradient membership.

theorem toDualMap_mem_subdifferential_primalConjugate_iff_eval_mem_subdifferential_conjugate {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf_proper : IsProperExtendedRealFunction f) (hf_closed : LowerSemicontinuous f) (hf_convex : is_convex_function f) (hfinite : ∀ (z : E), f∗ z ≠ ⊥ ∧ f∗ z < ⊤) {x g : E} : ↑((InnerProductSpace.toDualMap ℝ E) x) ∈ ∂fun (y : E) => ↑(f∗ y).toReal(g) ↔ (Module.Dual.eval ℝ E) x ∈ ∂conjugate_function f(↑((InnerProductSpace.toDualMap ℝ E) g))

Helper for Text 9.4: after normalizing the primal conjugate through the Riesz map, a subgradient of x ↦ ((f∗ x).toReal : EReal) at g is the same as the evaluation subgradient of conjugate_function f at toDualMap g.

theorem evalMemSubdifferentialConjugate_iff_memEuclideanSubdifferentialAt_primalConjugate {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {f : E → EReal} (hf_proper : IsProperExtendedRealFunction f) (hf_closed : LowerSemicontinuous f) (hf_convex : is_convex_function f) (hfinite : ∀ (y : E), f∗ y ≠ ⊥ ∧ f∗ y < ⊤) {x g : E} : (Module.Dual.eval ℝ E) x ∈ ∂conjugate_function f(↑((InnerProductSpace.toDualMap ℝ E) g)) ↔ x ∈ euclideanSubdifferentialAt (fun (y : E) => (f∗ y).toReal) g

Helper for Text 9.4: pulling the conjugate subdifferential back along the Riesz map turns evaluation functionals into Euclidean subgradients of the primal conjugate.

theorem mirror_descent_step_isMinOn_iff_dual_mem_subdifferential_add_indicator {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → EReal} {C : Set E} {σ : ℝ} {xk xNext gradf : E} {t : ℝ} (hω : IsBregmanPotentialOn ω C σ) (hxk : xk ∈ C ∩ subdifferential_domain ω) : xNext ∈ C ∧ IsMinOn (mirror_descent_update_objective (fun (y : E) => (ω y).toReal) xk gradf t) C xNext ↔ (InnerProductSpace.toDualMap ℝ E) (gradient (fun (y : E) => (ω y).toReal) xk - t • gradf) ∈ ∂ₛω + δ_ C (xNext)

Helper for Text 9.4: if hω : IsBregmanPotentialOn ω C σ and x^k ∈ C ∩ dom(∂ ω), then the Chapter 9 mirror-descent step, encoded in Lean as x⁺ ∈ C ∧ IsMinOn (mirror_descent_update_objective ((fun y ↦ (ω y).toReal)) x^k g_f t) C x⁺, is equivalent to the constrained subgradient condition ∇ω(x^k) - t g_f ∈ ∂ (ω + δ_C)(x⁺).

theorem mirror_descent_step_isMinOn_iff_eq_gradient_conjugate_add_indicator {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {ω : E → EReal} {C : Set E} {σ : ℝ} {xk xNext gradf : E} {t : ℝ} (hC_closed : IsClosed C) (hω : IsBregmanPotentialOn ω C σ) (hxk : xk ∈ C ∩ subdifferential_domain ω) : xNext ∈ C ∧ IsMinOn (mirror_descent_update_objective (fun (y : E) => (ω y).toReal) xk gradf t) C xNext ↔ xNext = gradient (fun (y : E) => ((ω + δ_ C)∗ y).toReal) (gradient (fun (y : E) => (ω y).toReal) xk - t • gradf)

Text 9.4: letting ω̃ = ω + δ_C, if C is closed, hω : IsBregmanPotentialOn ω C σ, and x^k ∈ C ∩ dom(∂ ω), then the mirror-descent update step, encoded in Lean as x⁺ ∈ C ∧ IsMinOn (mirror_descent_update_objective ((fun y ↦ (ω y).toReal)) x^k g_f t) C x⁺, is equivalent to the source-facing conjugate formula x⁺ = ∇ ω̃∗(∇ω(x^k) - t g_f), expressed in Lean via the real-valued restriction of ω̃∗.