Rule (3.7) gives
ProvedThreeOpSplitting.Accel.stepsize_identity_part2Let , and , and let be generated by the stepsize rule (3.7). Then for every
This is the counterpart for Part 2 of the identity that makes (3.10) telescope.
import Mathlib import Definitions.Def_ThreeOpSplitting_Accel_Stepsizes open Filter Topology
namespace ThreeOpSplitting.Accel
/-- Proof of Theorem 3.3, Part 2 (p. 846): the rule (3.7) ensures
`1/γ_{k+1}² = (1 + 2γ_k(μ_B - γ_kL_C²/2))/γ_k²` for all `k ≥ 0`. -/
theorem stepsize_identity_part2 (μB LC γ0 : ℝ)
(hμB : 0 < μB) (hLC : 0 < LC) (hγ0 : 0 < γ0) (hγ0' : γ0 < 2 * μB / LC ^ 2) (k : ℕ) :
1 / stepsPart2 μB LC γ0 (k + 1) ^ 2
= (1 + 2 * stepsPart2 μB LC γ0 k * (μB - stepsPart2 μB LC γ0 k * LC ^ 2 / 2))
/ stepsPart2 μB LC γ0 k ^ 2 := by sorry
end ThreeOpSplitting.Accel
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
The statement concerns a real-valued sequence , where is written . This function comes from the imported module Definitions.Def_ThreeOpSplitting_Accel_Stepsizes, and its definition is not shown here. Nothing in this statement says how is computed from , , and . In particular, it does not say whether as the sequence's value at index equals the input parameter . The statement also does not say whether the are nonzero or positive. The attached documentation comment describes the result as a stepsize identity from a "Theorem 3.3, Part 2" and a "rule (3.7)". That description is commentary only; the code does not enforce it.
The theorem takes three real parameters , , and a natural number , under these hypotheses:
- ;
- ;
- .
For every such choice of parameters and every , it asserts the exact equality
The hypotheses can all be satisfied, for example with , so the theorem is not vacuously true. The hypotheses appear only as assumptions; the equation itself does not mention them. Their only effect on the claim is to restrict it to the parameter choices above.
Degenerate cases:
- Small : is included, and there the claim links to the sequence's value at index . No other special cases arise from .
- Division by zero: the formal statement uses total real division, where . If some , the right-hand side is whatever its numerator is. If , the left-hand side is . So if , the statement asserts only , which holds exactly when . If but , it asserts that the right-hand numerator is .
- Signs: the statement fixes only through its square and the displayed numerator. Whether the stay positive, or stay below , depends entirely on the unshown definition of the sequence. The hypothesis applies only to the input parameter .
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.