Regret.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

Clipped Bellman regret for edit-distance refinement

The deterministic bound of Lemma lem:generic-regret in Section 7 of An Almost-Linear Approximation Scheme for Edit Distance (manuscript of September 24, 2026) applies to an arbitrary finite set of children satisfying the Bellman inequality and exact-cost connection inequality.

def OAI.EditApproximation.clipped line 20
Source documentation
Values are clipped at the exact cost only for the regret analysis.
```
def clipped (cost value : ℝ) : ℝ := max cost value
```
theorem OAI.EditApproximation.clipped_bellman_bound line 22

theorem OAI.EditApproximation.clipped_endpoint_decrease line 35

Source documentation

Clipping preserves the useful endpoint decrease bound even when the initial estimate itself lies below the true cost.

theorem clipped_endpoint_decrease (cost initial final mass gap : ℝ)
    (hmono : final ≤ initial) (hinit : initial ≤ mass)
    (hgapCost : |gap| ≤ cost) (hgapMass : |gap| ≤ mass) :
    clipped cost initial - clipped cost final ≤ mass - |gap| := by
…

Mentions: OAI.EditApproximation.clipped

theorem OAI.EditApproximation.generic_regret_telescope line 50

Source documentation

Finite-time telescoping of the clipped parent Bellman inequalities. The summation uses indices t + 1, corresponding to manuscript indices 1, …, S.

theorem generic_regret_telescope {ι : Type*} (children : Finset ι)
    (S : ℕ) (cost charge : ℝ) (childCost : ι → ℝ)
    (parent : ℕ → ℝ) (child : ℕ → ι → ℝ)
    (hsplit : cost ≤ charge + ∑ i ∈ children, childCost i)
    (hbellman : ∀ t < S, parent (t + 1) ≤ charge + ∑ i ∈ children, child t i) :
    ∑ t ∈ range S,
        (clipped cost (parent (t + 1)) - charge -
          ∑ i ∈ children, clipped (childCost i) (child (t + 1) i)) ≤
      ∑ i ∈ children,
        (clipped (childCost i) (child 0 i) - clipped (childCost i) (child S i)) := by
…

Mentions: OAI.EditApproximation.clipped

theorem OAI.EditApproximation.generic_regret_mass_bound line 83

Source documentation

The endpoint terms in generic regret are bounded by the warmup masses minus the absolute length gaps.

theorem generic_regret_mass_bound {ι : Type*} (children : Finset ι)
    (S : ℕ) (cost charge : ℝ) (childCost mass gap : ι → ℝ)
    (parent : ℕ → ℝ) (child : ℕ → ι → ℝ)
    (hsplit : cost ≤ charge + ∑ i ∈ children, childCost i)
    (hbellman : ∀ t < S, parent (t + 1) ≤ charge + ∑ i ∈ children, child t i)
    (hmono : ∀ i ∈ children, child S i ≤ child 0 i)
    (hinit : ∀ i ∈ children, child 0 i ≤ mass i)
    (hgapCost : ∀ i ∈ children, |gap i| ≤ childCost i)
    (hgapMass : ∀ i ∈ children, |gap i| ≤ mass i) :
    ∑ t ∈ range S,
        (clipped cost (parent (t + 1)) - charge -
          ∑ i ∈ children, clipped (childCost i) (child (t + 1) i)) ≤
…

Mentions: OAI.EditApproximation.clipped

theorem OAI.EditApproximation.sum_mass_sub_abs_le line 104

Source documentation

Since child length gaps add to the parent's gap, their absolute values give the final bound in manuscript Equation eq:generic-regret.

theorem sum_mass_sub_abs_le {ι : Type*} (children : Finset ι)
    (mass gap : ι → ℝ) :
    ∑ i ∈ children, (mass i - |gap i|) ≤
      (∑ i ∈ children, mass i) - |∑ i ∈ children, gap i| := by
…

theorem OAI.EditApproximation.predicted_length_gap_bound line 113
Source documentation
At a comparison node whose predicted normalized length gap is close to one, almost all warmup mass is accounted for by the absolute gap.
```
theorem predicted_length_gap_bound (W Z gap τ : ℝ)
    (hZ : 0 < Z) (hZW : Z ≤ W) (hτ : 0 ≤ τ)
    (hprediction : 1 - τ < |gap| / Z) :
    W - |gap| ≤ (W - Z) + τ * W := by
…
```

theorem OAI.EditApproximation.near_length_gap_regret_bound line 124

Source documentation

The refined generic bound at a node that is not bad and whose normalized length-gap predictor lies near one. The parameter q is H^(-1/4) in the manuscript.

theorem near_length_gap_regret_bound (W Z gap τ q F cost : ℝ)
    (hZ : 0 < Z) (hZW : Z ≤ W) (hτ : 0 ≤ τ)
    (hprediction : 1 - τ < |gap| / Z)
    (hdiscrepancy : W - Z ≤ q * cost)
    (hmass : W ≤ 4 * F * cost) :
    W - |gap| ≤ (q + 4 * τ * F) * cost := by
…

theorem OAI.EditApproximation.entropy_exponential_bound line 136

Source documentation

Scalar exponential estimate used in Lemma lem:entropy, Equation eq:entropy-exponential.

theorem entropy_exponential_bound (κ x : ℝ)
    (hκ : 0 ≤ κ) (hκhalf : κ ≤ 1 / 2) (hx : 0 ≤ x) (hxκ : x ≤ κ) :
    Real.exp ((1 - 2 * κ) * x) ≤ 1 + (1 - κ) * x := by
…

theorem OAI.EditApproximation.entropy_potential_telescoping line 164

Source documentation

The final telescoping step of Lemma lem:entropy. Here played t is the inner product with the chosen distribution, comparator t is the comparator inner product, and decrement t is its normalized decrement. The potential-increment and variational bounds are explicit internal proof obligations; this theorem does not assume a published online-learning guarantee.

theorem entropy_potential_telescoping (S : ℕ) (η κ bound : ℝ)
    (potential played comparator decrement : ℕ → ℝ)
    (hη : 0 < η) (hκ : 0 ≤ κ)
    (hincrement : ∀ t < S,
      potential (t + 1) - potential t ≤ η * played t)
    (hstart : potential 0 ≤ bound)
    (hcomparator : η * ((∑ t ∈ range S, comparator t) -
        2 * κ * ∑ t ∈ range S, decrement t) ≤ potential S)
    (hdecrement : ∑ t ∈ range S, decrement t ≤ 1) :
    (∑ t ∈ range S, comparator t) - bound / η - 2 * κ ≤
      ∑ t ∈ range S, played t := by
…

theorem OAI.EditApproximation.entropy_approximation_loss line 197

Source documentation

Accumulating the loss from approximate mixture vectors. In the application, error = H^(-3) and the coordinate gains lie in [-1, 0].

theorem entropy_approximation_loss (S : ℕ) (bound error : ℝ)
    (exactValue approximateValue : ℕ → ℝ)
    (hexact : bound ≤ ∑ t ∈ range S, exactValue t)
    (happrox : ∀ t < S, exactValue t - error ≤ approximateValue t) :
    bound - S * error ≤ ∑ t ∈ range S, approximateValue t := by
…

theorem OAI.EditApproximation.finite_relative_entropy_nonnegative line 212

Source documentation

Nonnegativity of relative entropy for a finite probability vector and a strictly positive reference vector. Zero coordinates of the first vector are allowed and contribute zero.

theorem finite_relative_entropy_nonnegative {ι : Type*} (coordinates : Finset ι)
    (p q : ι → ℝ)
    (hp : ∀ i ∈ coordinates, 0 ≤ p i)
    (hq : ∀ i ∈ coordinates, 0 < q i)
    (hpsum : ∑ i ∈ coordinates, p i = 1)
    (hqsum : ∑ i ∈ coordinates, q i = 1) :
    0 ≤ ∑ i ∈ coordinates, p i * Real.log (p i / q i) := by
…

theorem OAI.EditApproximation.finite_gibbs_variational_bound line 248

Source documentation

The finite Gibbs variational bound used when the innovation supremum over the actual action hull is extended to the simplex. This is a proved inequality, with no maximization-oracle assumption.

theorem finite_gibbs_variational_bound {ι : Type*} (coordinates : Finset ι)
    (p q gain : ι → ℝ)
    (hp : ∀ i ∈ coordinates, 0 ≤ p i)
    (hq : ∀ i ∈ coordinates, 0 < q i)
    (hpsum : ∑ i ∈ coordinates, p i = 1)
    (hqsum : ∑ i ∈ coordinates, q i = 1) :
    (∑ i ∈ coordinates, p i * gain i) -
        (∑ i ∈ coordinates, p i * Real.log (p i / q i)) ≤
      Real.log (∑ i ∈ coordinates, q i * Real.exp (gain i)) := by
…

theorem OAI.EditApproximation.entropy_small_increment_logsum line 299

Source documentation

The small-decrement logarithmic moment bound in the entropy innovation argument. The bound on η * innovation i is the only smallness requirement needed here.

theorem entropy_small_increment_logsum {ι : Type*} (coordinates : Finset ι)
    (p innovation : ι → ℝ) (η κ : ℝ)
    (hp : ∀ i ∈ coordinates, 0 < p i)
    (hpsum : ∑ i ∈ coordinates, p i = 1)
    (hκ : 0 ≤ κ) (hκhalf : κ ≤ 1 / 2)
    (hinnovation : ∀ i ∈ coordinates, 0 ≤ η * innovation i)
    (hsmall : ∀ i ∈ coordinates, η * innovation i ≤ κ) :
    Real.log (∑ i ∈ coordinates,
        p i * Real.exp (η * (1 - 2 * κ) * innovation i)) ≤
      η * (1 - κ) * ∑ i ∈ coordinates, p i * innovation i := by
…

theorem OAI.EditApproximation.fixed_block_mass_inner_product line 337

Source documentation

Equal probability mass in every child block makes every blockwise constant vector have the same inner product with the two distributions.

theorem fixed_block_mass_inner_product {ι β : Type*} [Fintype β] [DecidableEq β]
    (coordinates : Finset ι) (block : ι → β) (p q : ι → ℝ) (baseline : β → ℝ)
    (hblock : ∀ b, (∑ i ∈ coordinates with block i = b, p i) =
      ∑ i ∈ coordinates with block i = b, q i) :
    (∑ i ∈ coordinates, p i * baseline (block i)) =
      ∑ i ∈ coordinates, q i * baseline (block i) := by
…

theorem OAI.EditApproximation.entropy_innovation_variational_bound line 361

Source documentation

The innovation variational inequality for the actual action hull. Its fixed block masses are used exactly through hfixedMass: the blockwise minimum vector baseline has the same inner product with every feasible vector. The residual innovation has small range.

Combined with the entropy penalty at a positive maximizer, this bounds the potential increment without replacing the action hull by a simplex in the algorithm.

theorem entropy_innovation_variational_bound {ι : Type*} (coordinates : Finset ι)
    (p q decrement baseline innovation : ι → ℝ) (η κ : ℝ)
    (hp : ∀ i ∈ coordinates, 0 < p i)
    (hq : ∀ i ∈ coordinates, 0 ≤ q i)
    (hpsum : ∑ i ∈ coordinates, p i = 1)
    (hqsum : ∑ i ∈ coordinates, q i = 1)
    (hη : 0 ≤ η) (hκ : 0 ≤ κ) (hκhalf : κ ≤ 1 / 2)
    (hbaseline : ∀ i ∈ coordinates, 0 ≤ baseline i)
    (hdecomposition : ∀ i ∈ coordinates, decrement i = baseline i + innovation i)
    (hfixedMass : (∑ i ∈ coordinates, q i * baseline i) =
      ∑ i ∈ coordinates, p i * baseline i)
    (hinnovation : ∀ i ∈ coordinates, 0 ≤ η * innovation i)
…

theorem OAI.EditApproximation.entropy_first_order_on_segment line 413

Source documentation

First-order optimality of entropy plus a linear objective along a feasible segment. The segment-maximization hypothesis is exactly what an entropy maximizer on a convex action hull supplies.

theorem entropy_first_order_on_segment {ι : Type*} (coordinates : Finset ι)
    (p q objective : ι → ℝ) (η : ℝ)
    (hp : ∀ i ∈ coordinates, 0 < p i)
    (hmax : ∀ t : ℝ, 0 ≤ t → t ≤ 1 →
      (∑ i ∈ coordinates,
        (Real.negMulLog (p i + t * (q i - p i)) +
          η * objective i * (p i + t * (q i - p i)))) ≤
      ∑ i ∈ coordinates, (Real.negMulLog (p i) + η * objective i * p i)) :
    ∑ i ∈ coordinates,
      (-Real.log (p i) - 1 + η * objective i) * (q i - p i) ≤ 0 := by
…

theorem OAI.EditApproximation.entropy_penalty_of_first_order line 457

Source documentation

The exact relative-entropy penalty at a positive first-order maximizer. This proves manuscript Equation eq:entropy-penalty once the first-order condition is supplied by entropy_first_order_on_segment.

theorem entropy_penalty_of_first_order {ι : Type*} (coordinates : Finset ι)
    (p q objective : ι → ℝ) (η : ℝ)
    (hp : ∀ i ∈ coordinates, 0 < p i)
    (hpsum : ∑ i ∈ coordinates, p i = 1)
    (hqsum : ∑ i ∈ coordinates, q i = 1)
    (hfirst : ∑ i ∈ coordinates,
      (-Real.log (p i) - 1 + η * objective i) * (q i - p i) ≤ 0) :
    (∑ i ∈ coordinates, Real.negMulLog (q i)) +
        η * (∑ i ∈ coordinates, objective i * q i) ≤
      (∑ i ∈ coordinates, Real.negMulLog (p i)) +
        η * (∑ i ∈ coordinates, objective i * p i) -
        (∑ i ∈ coordinates, q i * Real.log (q i / p i)) := by
…

theorem OAI.EditApproximation.entropy_maximizer_positive line 511

Source documentation

An entropy maximizer cannot have a zero coordinate when a strictly positive feasible vector is available. Only maximization on the segments to that vector is needed, so this applies to the actual finite action hull in the manuscript.

theorem entropy_maximizer_positive {ι : Type*} (coordinates : Finset ι)
    (p witness objective : ι → ℝ) (η : ℝ)
    (hp : ∀ i ∈ coordinates, 0 ≤ p i)
    (hw : ∀ i ∈ coordinates, 0 < witness i)
    (hmax : ∀ t : ℝ, 0 ≤ t → t ≤ 1 →
      (∑ i ∈ coordinates,
        (Real.negMulLog ((1 - t) * p i + t * witness i) +
          η * objective i * ((1 - t) * p i + t * witness i))) ≤
      ∑ i ∈ coordinates, (Real.negMulLog (p i) + η * objective i * p i)) :
    ∀ i ∈ coordinates, 0 < p i := by
…

theorem OAI.EditApproximation.finite_entropy_nonnegative line 582

Source documentation

Entropy is nonnegative on a finite probability vector.

theorem finite_entropy_nonnegative {ι : Type*} (coordinates : Finset ι)
    (p : ι → ℝ) (hp : ∀ i ∈ coordinates, 0 ≤ p i)
    (hpsum : ∑ i ∈ coordinates, p i = 1) :
    0 ≤ ∑ i ∈ coordinates, Real.negMulLog (p i) := by
…

theorem OAI.EditApproximation.finite_entropy_le_log_card line 593

Source documentation

The entropy of a finite probability vector is at most the logarithm of the number of listed coordinates.

theorem finite_entropy_le_log_card {ι : Type*} (coordinates : Finset ι)
    (p : ι → ℝ) (hp : ∀ i ∈ coordinates, 0 ≤ p i)
    (hpsum : ∑ i ∈ coordinates, p i = 1) :
    (∑ i ∈ coordinates, Real.negMulLog (p i)) ≤ Real.log coordinates.card := by
…

def OAI.EditApproximation.entropyValue line 626
Source documentation
Entropy plus the linear objective, with the manuscript's scaling.
```
noncomputable def entropyValue {ι : Type*} (coordinates : Finset ι)
    (η : ℝ) (objective p : ι → ℝ) : ℝ :=
…
```
theorem OAI.EditApproximation.entropyValue_eq line 630

theorem OAI.EditApproximation.exists_entropy_maximizer line 644

Source documentation

The entropy potential is attained on every nonempty compact action hull, since the zero-coordinate convention gives continuous entropy.

theorem exists_entropy_maximizer {ι : Type*} (coordinates : Finset ι)
    (Q : Set (ι → ℝ)) (η : ℝ) (objective : ι → ℝ)
    (hcompact : IsCompact Q) (hne : Q.Nonempty) :
    ∃ p ∈ Q, IsMaxOn (entropyValue coordinates η objective) Q p := by
…

Mentions: OAI.EditApproximation.entropyValue

theorem OAI.EditApproximation.entropy_hull_maximizer_positive line 654

Source documentation

Positivity of the entropy maximizer on a convex feasible hull with a positive feasible witness.

theorem entropy_hull_maximizer_positive {ι : Type*} (coordinates : Finset ι)
    (Q : Set (ι → ℝ)) (η : ℝ) (objective p witness : ι → ℝ)
    (hconvex : Convex ℝ Q) (hpQ : p ∈ Q) (hwQ : witness ∈ Q)
    (hp : ∀ i ∈ coordinates, 0 ≤ p i)
    (hw : ∀ i ∈ coordinates, 0 < witness i)
    (hmax : IsMaxOn (entropyValue coordinates η objective) Q p) :
    ∀ i ∈ coordinates, 0 < p i := by
…

Mentions: OAI.EditApproximation.entropyValue

theorem OAI.EditApproximation.entropy_hull_penalty line 669

Source documentation

The exact KL penalty holds for every competitor in the action hull, including competitors with zero coordinates.

theorem entropy_hull_penalty {ι : Type*} (coordinates : Finset ι)
    (Q : Set (ι → ℝ)) (η : ℝ) (objective p q : ι → ℝ)
    (hconvex : Convex ℝ Q) (hpQ : p ∈ Q) (hqQ : q ∈ Q)
    (hp : ∀ i ∈ coordinates, 0 < p i)
    (hpsum : ∑ i ∈ coordinates, p i = 1)
    (hqsum : ∑ i ∈ coordinates, q i = 1)
    (hmax : IsMaxOn (entropyValue coordinates η objective) Q p) :
    entropyValue coordinates η objective q ≤ entropyValue coordinates η objective p -
      ∑ i ∈ coordinates, q i * Real.log (q i / p i) := by
…

Mentions: OAI.EditApproximation.entropyValue

theorem OAI.EditApproximation.entropyValue_add_scaled line 692

theorem OAI.EditApproximation.entropy_hull_potential_step line 712

Source documentation

One complete optimistic entropy-potential step on the actual hull. The old objective and its predicted increment are arbitrary and may have negative coordinates. Only the residual decrement is small.

theorem entropy_hull_potential_step {ι : Type*} (coordinates : Finset ι)
    (Q : Set (ι → ℝ)) (η κ : ℝ)
    (old gain decrement baseline innovation oldLeader predicted newLeader : ι → ℝ)
    (hconvex : Convex ℝ Q)
    (hpredQ : predicted ∈ Q) (hnewQ : newLeader ∈ Q)
    (hpred : ∀ i ∈ coordinates, 0 < predicted i)
    (hnew : ∀ i ∈ coordinates, 0 ≤ newLeader i)
    (hpredsum : ∑ i ∈ coordinates, predicted i = 1)
    (hnewsum : ∑ i ∈ coordinates, newLeader i = 1)
    (holdMax : IsMaxOn (entropyValue coordinates η old) Q oldLeader)
    (hpredMax : IsMaxOn
      (entropyValue coordinates η (fun i => old i + gain i)) Q predicted)
…

Mentions: OAI.EditApproximation.entropyValue

def OAI.EditApproximation.optimisticHistory line 768

Source documentation

The accumulated optimistic objective before a time index.

noncomputable def optimisticHistory {ι : Type*} (κ : ℝ)
    (gain decrement : ℕ → ι → ℝ) (t : ℕ) (i : ι) : ℝ :=
…

theorem OAI.EditApproximation.optimisticHistory_succ line 772
theorem OAI.EditApproximation.optimisticHistory_inner_product line 781

theorem OAI.EditApproximation.finite_hull_entropy_regret line 799

Source documentation

Lemma lem:entropy for a finite compact convex action hull. The fixed child-block masses enter through the equality of the baseline inner products; fixed_block_mass_inner_product supplies that equality from the individual block masses. The potential argument uses positivity and the relative-entropy penalty.

theorem finite_hull_entropy_regret {ι : Type*} (coordinates : Finset ι)
    (Q : Set (ι → ℝ)) (S : ℕ) (η κ : ℝ)
    (gain decrement baseline innovation predicted : ℕ → ι → ℝ)
    (witness comparator : ι → ℝ)
    (hcompact : IsCompact Q) (hconvex : Convex ℝ Q)
    (hwQ : witness ∈ Q) (hcQ : comparator ∈ Q)
    (hw : ∀ i ∈ coordinates, 0 < witness i)
    (hprob : ∀ p ∈ Q,
      (∀ i ∈ coordinates, 0 ≤ p i) ∧ (∑ i ∈ coordinates, p i = 1))
    (hη : 0 < η) (hκ : 0 ≤ κ) (hκhalf : κ ≤ 1 / 2)
    (hpredQ : ∀ t < S, predicted t ∈ Q)
    (hpredMax : ∀ t < S, IsMaxOn
…

theorem OAI.EditApproximation.bounded_gain_l1_approximation line 887

Source documentation

Replacing a probability vector by an approximation in ℓ₁ loses at most that error against any coordinate gain in [-1, 0].

theorem bounded_gain_l1_approximation {ι : Type*} (coordinates : Finset ι)
    (gain exactVector approximateVector : ι → ℝ) (error : ℝ)
    (hgain : ∀ i ∈ coordinates, -1 ≤ gain i ∧ gain i ≤ 0)
    (hl1 : ∑ i ∈ coordinates, |approximateVector i - exactVector i| ≤ error) :
    (∑ i ∈ coordinates, gain i * exactVector i) - error ≤
      ∑ i ∈ coordinates, gain i * approximateVector i := by
…

theorem OAI.EditApproximation.finite_block_entropy_regret line 911

Source documentation

The entropy-regret lemma in its fixed-child-block form. Baseline decrements are constructed as the actual minimum within each child block; the range hypothesis supplies the small residual required by the potential proof.

theorem finite_block_entropy_regret {ι β : Type*} [Fintype β] [DecidableEq β]
    (coordinates : Finset ι) (block : ι → β)
    (Q : Set (ι → ℝ)) (S : ℕ) (η κ rangeBound : ℝ)
    (gain decrement predicted : ℕ → ι → ℝ) (witness comparator : ι → ℝ)
    (hcompact : IsCompact Q) (hconvex : Convex ℝ Q)
    (hwQ : witness ∈ Q) (hcQ : comparator ∈ Q)
    (hw : ∀ i ∈ coordinates, 0 < witness i)
    (hprob : ∀ p ∈ Q,
      (∀ i ∈ coordinates, 0 ≤ p i) ∧ (∑ i ∈ coordinates, p i = 1))
    (hblocks : ∀ b, (coordinates.filter (fun i => block i = b)).Nonempty)
    (hblockMass : ∀ p ∈ Q, ∀ q ∈ Q, ∀ b,
      (∑ i ∈ coordinates with block i = b, p i) =
…