APNOutputs/AICollaborator/Optimization/LastIterateConvergence.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: Google DeepMind published the AlphaProof Nexus proof artifacts. The pinned repository identifies the mathematical sources and collaborators, including OEIS, Erdős Problems, Gergely Bérczi, and Mario Krenn; those source records remain the authority for individual credit.

Project sources: Pinned AlphaProof Nexus results documentation, AlphaProof Nexus paper, Pinned human-written natural-language proof companions

35 declarations, 0 contain sorry, 0 declared as axioms

ODE Analysis of Stochastic Gradient Methods with Optimism and Anchoring for Minimax Problems

Reference: arxiv/1905.10899 by Ernest K. Ryu, Kun Yuan, Wotao Yin

Imports (1)
  1. abbrev Arxiv.«1905.10899».E_n line 32 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat

    Proof uses: EuclideanSpace, Real, Fin

  2. abbrev Arxiv.«1905.10899».F_m line 33 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat

    Proof uses: EuclideanSpace, Real, Fin

  3. abbrev Arxiv.«1905.10899».Z_space line 34 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat

    Proof uses: WithLp, OfNat.ofNat, ENNReal, Prod, Arxiv.«1905.10899».E_n, Arxiv.«1905.10899».F_m

    5 instances, coercions and auxiliary constants left out.

  4. def Arxiv.«1905.10899».toProd line 36 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, ContinuousLinearEquiv, Real, RingHom.id, Arxiv.«1905.10899».Z_space, OfNat.ofNat, ENNReal, Arxiv.«1905.10899».E_n, Arxiv.«1905.10899».F_m, Fin, Prod

    Proof uses: WithLp.prodContinuousLinearEquiv

    81 instances, coercions and auxiliary constants left out.

  5. structure Arxiv.«1905.10899».State line 39 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat

  6. def Arxiv.«1905.10899».F_operator Operator G(z) = (∇_x L(z), -∇_y L(z)) line 46 source

    Source comment

    Operator G(z) = (∇_x L(z), -∇_y L(z))

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Arxiv.«1905.10899».Z_space, Real

    Proof uses: Prod, Arxiv.«1905.10899».E_n, Arxiv.«1905.10899».F_m, ContinuousLinearEquiv, RingHom.id, OfNat.ofNat, ENNReal, Fin, Arxiv.«1905.10899».toProd, gradient, ContinuousLinearEquiv.symm, Prod.mk, Prod.fst, Neg.neg, Prod.snd

    59 instances, coercions and auxiliary constants left out.

    noncomputable def F_operator
  (L : (Z_space n m) → ℝ)
  (z : Z_space n m) : Z_space n m :=
…

    Mentions: Arxiv.«1905.10899».Z_space

  7. def Arxiv.«1905.10899».IsSaddlePoint line 52 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Arxiv.«1905.10899».Z_space, Real

    Proof uses: Arxiv.«1905.10899».IsSaddlePoint.match_1, Prod, Arxiv.«1905.10899».E_n, Arxiv.«1905.10899».F_m, ContinuousLinearEquiv, RingHom.id, OfNat.ofNat, ENNReal, Fin, Arxiv.«1905.10899».toProd, And, LE.le, ContinuousLinearEquiv.symm, Prod.mk

    50 instances, coercions and auxiliary constants left out.

  8. def Arxiv.«1905.10899».step Anchored Simultaneous Gradient Descent z_{t+1} = z_t - α_t * G(z_t) + β_t * (z_0 - z_t) line 59 source

    Source comment

    Anchored Simultaneous Gradient Descent z_{t+1} = z_t - α_t * G(z_t) + β_t * (z_0 - z_t)

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Arxiv.«1905.10899».Z_space, Real, Arxiv.«1905.10899».State

    Proof uses: Arxiv.«1905.10899».F_operator, Arxiv.«1905.10899».State.z, HSMul.hSMul, OfNat.ofNat, ENNReal, Prod, Arxiv.«1905.10899».E_n, Arxiv.«1905.10899».F_m, Fin, HSub.hSub, Arxiv.«1905.10899».State.z0, HAdd.hAdd, Arxiv.«1905.10899».State.mk, Arxiv.«1905.10899».State.t, HAppend.hAppend, List, Arxiv.«1905.10899».State.history, List.cons, List.nil

    40 instances, coercions and auxiliary constants left out.

    noncomputable def step
  (L : (Z_space n m) → ℝ)
  (s : State n m)
  (grad_coeff anchor_coeff : ℝ)
  : State n m :=
…

    Mentions: Arxiv.«1905.10899».Z_space, Arxiv.«1905.10899».State

  9. def Arxiv.«1905.10899».coefficients_schedule line 85 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, Nat, Prod

    Proof uses: Prod.mk, HDiv.hDiv, OfNat.ofNat, HMul.hMul, Real.sqrt, HAdd.hAdd

    11 instances, coercions and auxiliary constants left out.

  10. lemma Arxiv.«1905.10899».inner_F_operator_self_ge_zero line 90 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Arxiv.«1905.10899».Z_space, Real, GE.ge, Inner.inner, OfNat.ofNat, ENNReal, Arxiv.«1905.10899».E_n, Arxiv.«1905.10899».F_m, Fin, HSub.hSub, Arxiv.«1905.10899».F_operator, Eq, Prod

    Proof uses: sub_zero, Eq.mp, congrArg

    76 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  11. lemma Arxiv.«1905.10899».F_operator_lipschitz_bound line 100 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Arxiv.«1905.10899».Z_space, Real, NNReal, LE.le, Norm.norm, OfNat.ofNat, ENNReal, Arxiv.«1905.10899».E_n, Arxiv.«1905.10899».F_m, Fin, HSub.hSub, Arxiv.«1905.10899».F_operator, HMul.hMul, Eq, Prod

    Proof uses: sub_zero, Eq.mp, congrArg

    66 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  12. lemma Arxiv.«1905.10899».z0_eq line 111 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Arxiv.«1905.10899».Z_space, Real, Arxiv.«1905.10899».State, Eq, OfNat.ofNat, Arxiv.«1905.10899».State.mk, List.cons, List.nil, HAdd.hAdd, Arxiv.«1905.10899».step, Prod.fst, Arxiv.«1905.10899».coefficients_schedule, Prod.snd, Arxiv.«1905.10899».State.z0

    Proof uses: Nat.recAux, Eq.mpr, id, congrArg, Eq.refl

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  13. lemma Arxiv.«1905.10899».z_update_eq line 123 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Arxiv.«1905.10899».Z_space, Real, Arxiv.«1905.10899».State, Eq, OfNat.ofNat, Arxiv.«1905.10899».State.mk, List.cons, List.nil, HAdd.hAdd, Arxiv.«1905.10899».step, Prod.fst, Arxiv.«1905.10899».coefficients_schedule, Prod.snd, Arxiv.«1905.10899».State.z, ENNReal, Arxiv.«1905.10899».E_n, Arxiv.«1905.10899».F_m, Fin, HSub.hSub and 6 more

    Proof uses: Arxiv.«1905.10899».State.z0, Arxiv.«1905.10899».z0_eq, Eq.mpr, id, congrArg, rfl, Eq.refl

    96 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

  14. lemma Arxiv.«1905.10899».norm_convex_comb_sq line 138 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, LE.le, OfNat.ofNat, HPow.hPow, Nat, Norm.norm, HAdd.hAdd, HSMul.hSMul, HSub.hSub, HMul.hMul

    Proof uses: Inner.inner, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.pow_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.pow_add and 70 more

    166 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

  15. lemma Arxiv.«1905.10899».inner_cross_bound line 144 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, LE.le, HMul.hMul, Neg.neg, OfNat.ofNat, Nat, Inner.inner, HAdd.hAdd, HPow.hPow, Norm.norm, OfScientific.ofScientific, Bool.true

    Proof uses: Or, Eq, le_total, Or.inl, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.sub_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat and 104 more

    162 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

  16. lemma Arxiv.«1905.10899».one_step_bound line 150 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, LE.le, OfNat.ofNat, Inner.inner, HSub.hSub, Norm.norm, HMul.hMul, Eq, HAdd.hAdd, HSMul.hSMul, HPow.hPow, Nat, OfScientific.ofScientific, Bool.true

    Proof uses: Eq.mpr, id, congrArg, Eq.refl, Eq.symm, norm_sub_sq_real, RingHom, starRingEnd, congr, Eq.trans, inner_smul_right, inner_add_left, inner_smul_left, mul_comm, add_mul, mul_assoc, Arxiv.«1905.10899».norm_convex_comb_sq, norm_smul_of_nonneg, mul_pow, Neg.neg and 123 more

    242 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

    Open to load the checked before-and-after goal states.

  17. lemma Arxiv.«1905.10899».poly_bound line 172 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, OfNat.ofNat, Nat, HAdd.hAdd, HMul.hMul, HPow.hPow

    Proof uses: Eq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add, Mathlib.Tactic.Ring.add_mul, Mathlib.Tactic.Ring.mul_add, Mathlib.Tactic.Ring.mul_pf_right, Mathlib.Tactic.Ring.mul_one, Mathlib.Tactic.Ring.mul_zero, Mathlib.Tactic.Ring.add_pf_add_zero, Mathlib.Tactic.Ring.zero_mul and 53 more

    95 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.

  18. lemma Arxiv.«1905.10899».seq_bound_algebra_new line 179 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, OfNat.ofNat, HMul.hMul, Nat, HDiv.hDiv, HAdd.hAdd, HSub.hSub, OfScientific.ofScientific, Bool.true, HPow.hPow

    Proof uses: LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.neg_congr, Nat.cast_one, Mathlib.Tactic.Ring.neg_add and 190 more

    198 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

    Open to load the checked before-and-after goal states.

  19. lemma Arxiv.«1905.10899».bounded_iterates_D line 201 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Arxiv.«1905.10899».Z_space, Real, Differentiable, OfNat.ofNat, ENNReal, Prod, Arxiv.«1905.10899».E_n, Arxiv.«1905.10899».F_m, Fin, GE.ge, Inner.inner, HSub.hSub, Arxiv.«1905.10899».F_operator, NNReal, LT.lt, LE.le, Norm.norm, HMul.hMul, Arxiv.«1905.10899».State and 12 more

    Proof uses: Nat.recAux, Eq.mpr, id, congrArg, Eq.refl, sq_nonneg, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo and 129 more

    316 instances, coercions and auxiliary constants left out.

    Tactic trace: 37 steps

    Open to load the checked before-and-after goal states.

  20. lemma Arxiv.«1905.10899».bounded_iterates_D_exist_helper line 238 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, HMul.hMul, OfNat.ofNat, Nat, Eq, HAdd.hAdd, Real.sqrt

    Proof uses: Mathlib.Tactic.LinearCombination.le_of_le, Mathlib.Tactic.LinearCombination.add_le_eq, Real.sqrt_le_sqrt, Eq.symm, Real.sqrt_mul', Mathlib.Tactic.LinearCombination.le_rearrange, Mathlib.Tactic.Ring.le_congr, HSub.hSub, Mathlib.Tactic.Ring.sub_congr, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.add_congr, Mathlib.Tactic.Ring.atom_pf, Mathlib.Tactic.Ring.add_pf_add_lt, Mathlib.Tactic.Ring.add_pf_zero_add, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.add_mul, Mathlib.Tactic.Ring.mul_add, Mathlib.Tactic.Ring.mul_pf_right and 31 more

    70 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  21. lemma Arxiv.«1905.10899».bounded_iterates_D_exist line 243 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Arxiv.«1905.10899».Z_space, Real, Differentiable, OfNat.ofNat, ENNReal, Prod, Arxiv.«1905.10899».E_n, Arxiv.«1905.10899».F_m, Fin, GE.ge, Inner.inner, HSub.hSub, Arxiv.«1905.10899».F_operator, NNReal, LT.lt, LE.le, Norm.norm, HMul.hMul, Arxiv.«1905.10899».State and 13 more

    Proof uses: HPow.hPow, Arxiv.«1905.10899».bounded_iterates_D, Exists.intro, Real.sqrt, And.intro, le_of_lt, add_pos', Real.sqrt_pos_of_pos, Mathlib.Meta.Positivity.pos_of_isNat, inferInstance, PartialOrder, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Nat.ble, Nat.cast_one, norm_nonneg, mul_nonneg, Eq.trans and 72 more

    233 instances, coercions and auxiliary constants left out.

    Tactic trace: 26 steps

    Open to load the checked before-and-after goal states.

  22. lemma Arxiv.«1905.10899».A_bound line 277 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, OfNat.ofNat, LT.lt, HDiv.hDiv, Real.sqrt, HAdd.hAdd, HSub.hSub, OfScientific.ofScientific, Bool.true

    Proof uses: Eq.mpr, HMul.hMul, inferInstance, CommGroupWithZero, id, Eq, Mathlib.Tactic.FieldSimp.le_eq_cancel_le, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Int, Neg.neg, List.nil, Prod, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, rfl, Eq.trans, Mathlib.Tactic.FieldSimp.subst_sub, Mathlib.Tactic.FieldSimp.NF.one_eq_eval, Eq.symm and 157 more

    174 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  23. lemma Arxiv.«1905.10899».error_term_bound line 284 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, OfNat.ofNat, HDiv.hDiv, Real.sqrt, HAdd.hAdd, abs, HSub.hSub, HMul.hMul, HPow.hPow, Nat

    Proof uses: Eq.mpr, And, Inv.inv, id, Eq, Eq.trans, Neg.neg, congr, congrArg, div_eq_mul_inv, one_mul, inv_inv, mul_comm, mul_sub, mul_assoc, inferInstance, CommGroupWithZero, Mathlib.Tactic.FieldSimp.le_eq_cancel_le, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons and 143 more

    182 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

  24. lemma Arxiv.«1905.10899».contraction_factor_sq line 295 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, OfNat.ofNat, HDiv.hDiv, HAdd.hAdd, Nat, HPow.hPow, HSub.hSub, HMul.hMul, OfScientific.ofScientific, Bool.true

    Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Tactic.Ring.sub_congr and 99 more

    170 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

  25. lemma Arxiv.«1905.10899».delta_contraction_factor line 298 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, OfNat.ofNat, Nat, LT.lt, HDiv.hDiv, Real.sqrt, HAdd.hAdd, HSub.hSub, And, HPow.hPow, HMul.hMul, OfScientific.ofScientific, Bool.true

    Proof uses: Eq.mpr, Inv.inv, Mathlib.Meta.NormNum.instAtLeastTwo, id, Eq, Eq.trans, congr, congrArg, one_div, div_inv_eq_mul, div_pow, inv_pow, Real.sq_sqrt, of_eq_true, True, eq_true, LE.le.trans', Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero and 224 more

    234 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

    Open to load the checked before-and-after goal states.

  26. lemma Arxiv.«1905.10899».delta_algebra_subst line 314 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, NormedSpace, Real, Eq, HAdd.hAdd, HSub.hSub, HSMul.hSMul, Ne, OfNat.ofNat, HDiv.hDiv, HMul.hMul

    Proof uses: Eq.mpr, id, congr, congrArg, Eq.trans, smul_sub, Mathlib.Tactic.LinearCombination.eq_of_eq, Neg.neg, Mathlib.Tactic.LinearCombination.smul_const_eq, Mathlib.Tactic.LinearCombination.smul_eq_const, div_self, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval, Nat, Mathlib.Tactic.Module.NF.cons, Prod.mk, RingHom, Int, algebraMap, List.nil and 79 more

    166 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  27. lemma Arxiv.«1905.10899».delta_norm_bound line 324 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, InnerProductSpace, Real, LE.le, OfNat.ofNat, Eq, HAdd.hAdd, HSub.hSub, HSMul.hSMul, Inner.inner, Norm.norm, HMul.hMul, Real.sqrt, HPow.hPow, Nat

    Proof uses: Eq.rec, norm_add_le_of_le, le_of_sq_le_sq, LE.le.trans, Eq.mpr, id, congrArg, norm_sub_sq_real, norm_smul_of_nonneg, real_inner_smul_right, real_inner_smul_left, real_inner_comm, le_refl, Mathlib.Tactic.LinearCombination.le_of_le, add_le_add, Mathlib.Tactic.LinearCombination.add_le_eq, Mathlib.Tactic.LinearCombination.mul_le_const, Mathlib.Tactic.LinearCombination.mul_const_le, le_of_lt, Mathlib.Meta.Positivity.pos_of_isNat and 69 more

    167 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

    Open to load the checked before-and-after goal states.

  28. lemma Arxiv.«1905.10899».delta_induction line 334 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, OfNat.ofNat, Nat, HAdd.hAdd, HMul.hMul, HSub.hSub, HDiv.hDiv, OfScientific.ofScientific, Bool.true, HPow.hPow, Exists, And

    Proof uses: Exists.elim, Max.max, exists_nat_ge, Exists.intro, And.intro, le_sup_left, Iff.mpr, le_div_iff₀, add_pos', LT.lt, Nat.cast_pos', lt_of_lt_of_le, inferInstance, PartialOrder, Zero, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble and 131 more

    206 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

    Open to load the checked before-and-after goal states.

  29. lemma Arxiv.«1905.10899».bounded_differences_E line 342 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Arxiv.«1905.10899».Z_space, Real, Differentiable, OfNat.ofNat, ENNReal, Prod, Arxiv.«1905.10899».E_n, Arxiv.«1905.10899».F_m, Fin, GE.ge, Inner.inner, HSub.hSub, Arxiv.«1905.10899».F_operator, NNReal, LT.lt, LE.le, Norm.norm, HMul.hMul, Arxiv.«1905.10899».State and 14 more

    Proof uses: Arxiv.«1905.10899».bounded_iterates_D_exist, OfScientific.ofScientific, Bool.true, HPow.hPow, Real.sqrt, HSMul.hSMul, id, Eq.mpr, congrArg, HAdd, Eq.rec, Eq.refl, HSub, HSMul, Inv.inv, congr, Prod.mk, Eq.trans, Nat.cast_add, Mathlib.Meta.NormNum.IsNat.to_eq and 281 more

    394 instances, coercions and auxiliary constants left out.

    Tactic trace: 91 steps

    Open to load the checked before-and-after goal states.

  30. lemma Arxiv.«1905.10899».F_norm_bound_helper line 422 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: NormedAddCommGroup, NormedSpace, Real, Eq, HAdd.hAdd, HSub.hSub, HSMul.hSMul, LT.lt, OfNat.ofNat, LE.le, Norm.norm, HMul.hMul, HDiv.hDiv

    Proof uses: Eq.mpr, id, Eq.trans, Inv.inv, congrArg, congr, div_eq_inv_mul, Eq.mp, sub_add, sub_sub_self, mul_assoc, of_eq_true, True, one_mul

    146 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  31. lemma Arxiv.«1905.10899».rate_algebra line 430 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, OfNat.ofNat, LT.lt, HAdd.hAdd, HMul.hMul, Real.sqrt, HDiv.hDiv, HPow.hPow, Nat

    Proof uses: pow_le_pow_left₀, LE.le.trans, Mathlib.Tactic.LinearCombination.le_of_le, Inv.inv, Mathlib.Tactic.LinearCombination.mul_const_le, add_le_add, Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos, Real.sqrt_pos_of_pos, add_pos_of_pos_of_nonneg, inferInstance, PartialOrder, lt_of_lt_of_le, Zero, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl, Bool, Nat.ble, Mathlib.Tactic.LinearCombination.add_le_eq and 56 more

    112 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

  32. lemma Arxiv.«1905.10899».last_iterate_algebra_h1 line 440 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, OfNat.ofNat, Nat, HDiv.hDiv, Real.sqrt, HAdd.hAdd

    Proof uses: LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.neg_add and 87 more

    121 instances, coercions and auxiliary constants left out.

    Tactic trace: 23 steps

    Open to load the checked before-and-after goal states.

  33. lemma Arxiv.«1905.10899».last_iterate_algebra_h2 line 458 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, OfNat.ofNat, Nat, HDiv.hDiv, Real.sqrt, HAdd.hAdd

    Proof uses: LT.lt, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.neg_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.neg_add and 46 more

    91 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

    Open to load the checked before-and-after goal states.

  34. lemma Arxiv.«1905.10899».last_iterate_algebra line 469 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Real, LE.le, OfNat.ofNat, Nat, LT.lt, HAdd.hAdd, HPow.hPow, HMul.hMul, HDiv.hDiv, Real.sqrt

    Proof uses: le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.neg_congr, Nat.cast_one, Mathlib.Tactic.Ring.neg_add, Mathlib.Tactic.Ring.neg_one_mul and 76 more

    134 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

    Open to load the checked before-and-after goal states.

  35. theorem Arxiv.«1905.10899».last_iterate_convergence Exact last-iterate O(1/T) convergence for anchored gradient descent-ascent line 491 source

    Source documentation

    The last-iterate convergence of Anchored Simultaneous Gradient Descent (SimGD-A) with parameter $p = 1/2$.

    This theorem corresponds to the critical boundary case of Theorem 3 in arXiv:1905.10899, where the step size $\alpha_t$ and anchoring coefficient $\beta_t$ are set to achieve an $O(1/T)$ convergence rate on the squared norm of the operator.

    While Theorem 3 in the paper is formally stated for $p \in (1/2, 1)$, the "Further discussion" in Section 4.2 identifies $p = 1/2$ as the theoretical limit of stability and discretization.

    A DeepMind prover agent was able to proof that convergence holds for $p = 1/2$.

    L4DEL explanation

    it remained an open problem whether the improved exact O(1/t) rate is achievable

    If p ∈ (1/2, 1) and γ ≥ 2, then SimGD-A converges

    The proof departs from continuous-time ordinary differential equations (ODE) analysis used in previous work, instead using a discrete-time recurrence-based approach.

    For a differentiable convex-concave objective whose saddle operator is monotone and Lipschitz, the schedule α_t = 1/(K√(t+γ)) and β_t = γ/(t+γ) with γ ≥ 2 gives a positive constant C such that ‖F(z_T)‖² ≤ C/T for every T ≥ 1.

    1. The hypotheses explicitly supply differentiability, monotonicity, a positive Lipschitz constant, and a saddle point z_star satisfying F(z_star)=0.
    2. The sequence is not arbitrary: each state must follow the pinned update rule with the square-root step size and reciprocal anchoring schedule.
    3. The proof first bounds every iterate relative to the saddle point, then bounds consecutive-iterate differences, and finally rewrites the update to control the last operator value.
    4. The conclusion is existential in C; the proof constructs one, but the public theorem promises only that some positive uniform constant works.

    Sources and attribution: Pinned Lean source (0647711a7118), Anja Surina et al., improved anchored-GDA paper (2026), Ernest K. Ryu, Kun Yuan, and Wotao Yin, original anchored-SimGD paper (2020 revision), George Tsoukalas et al., AlphaProof Nexus paper (Section 4)

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Arxiv.«1905.10899».Z_space, Real, Differentiable, OfNat.ofNat, ENNReal, Prod, Arxiv.«1905.10899».E_n, Arxiv.«1905.10899».F_m, Fin, GE.ge, Inner.inner, HSub.hSub, Arxiv.«1905.10899».F_operator, NNReal, LT.lt, LE.le, Norm.norm, HMul.hMul, Arxiv.«1905.10899».State and 15 more

    Proof uses: Arxiv.«1905.10899».bounded_iterates_D_exist, Arxiv.«1905.10899».bounded_differences_E, Exists.intro, And.intro, sq_nonneg, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.add_congr, Int.rawCast, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.instCommSemiringNat, Mathlib.Tactic.Ring.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 110 more

    301 instances, coercions and auxiliary constants left out.

    Tactic trace: 48 steps

    Open to load the checked before-and-after goal states.

    theorem last_iterate_convergence
  (L : (Z_space n m) → ℝ)
  (h_diff : Differentiable ℝ L)

  (h_monotone : ∀ z w : Z_space n m,
    inner ℝ (F_operator n m L z - F_operator n m L w) (z - w) ≥ (0 : ℝ)) -- Convex-Concave

  (K : NNReal) (h_K_nonneg : 0 < K) -- Lipschitz-Continuous
  (h_lipschitz : ∀ z w : Z_space n m,
    ‖F_operator n m L z - F_operator n m L w‖ ≤ K * ‖z - w‖)

  -- Algorithm Parameter
…

    Mentions: Arxiv.«1905.10899».Z_space, Arxiv.«1905.10899».F_operator, K