Numerics.lean`

65 declarations, 0 contain sorry, 0 declared as axioms

Finite numerical optimizer for edit-distance refinement

These are the explicit fixed-step recurrence and rational mixture calculations from Section 9 of An Almost-Linear Approximation Scheme for Edit Distance (September 24, 2026). The recurrence is an internal analytic obligation of the manuscript, not an assumed published theorem.

def OAI.EditApproximation.frankWolfeStep line 21
Source documentation
The conditional-gradient step size in the finite entropy optimizer.
```
noncomputable def frankWolfeStep (j : ℕ) : ℝ := 2 / ((j : ℝ) + 2)
```
theorem OAI.EditApproximation.frankWolfeStep_nonnegative line 23
theorem OAI.EditApproximation.frankWolfeStep_le_one line 27

theorem OAI.EditApproximation.frank_wolfe_scalar_step line 35

Source documentation

The scalar induction step giving the optimizer's 8/(σ(j+1)) error term.

theorem frank_wolfe_scalar_step (σ error x : ℝ) (hσ : 0 < σ) (hx : 0 ≤ x) :
    (1 - 2 / (x + 3)) * (2 * error + 8 / (σ * (x + 2))) +
        2 * error * (2 / (x + 3)) + 2 * (2 / (x + 3)) ^ 2 / σ ≤
      2 * error + 8 / (σ * (x + 3)) := by
…

theorem OAI.EditApproximation.frank_wolfe_gap_bound line 53

Source documentation

The first update removes dependence on the initial objective gap. The conclusion corresponds to manuscript indices j ≥ 1.

theorem frank_wolfe_gap_bound (σ error : ℝ) (gap : ℕ → ℝ)
    (hσ : 0 < σ)
    (hrecurrence : ∀ j,
      gap (j + 1) ≤ (1 - frankWolfeStep j) * gap j +
        2 * error * frankWolfeStep j + 2 * (frankWolfeStep j) ^ 2 / σ) :
    ∀ j : ℕ, gap (j + 1) ≤ 2 * error + 8 / (σ * ((j : ℝ) + 2)) := by
…

Mentions: OAI.EditApproximation.frankWolfeStep

def OAI.EditApproximation.optimizerMixtureWeight line 87
Source documentation
Exact rational weight of the vertex selected at step j, after K steps.
```
def optimizerMixtureWeight (K j : ℕ) : ℚ :=
…
```
theorem OAI.EditApproximation.sum_optimizer_numerators line 90
theorem OAI.EditApproximation.optimizerMixtureWeight_positive line 99
theorem OAI.EditApproximation.sum_optimizerMixtureWeight line 105
theorem OAI.EditApproximation.optimizerMixtureWeight_update_old line 113
theorem OAI.EditApproximation.optimizerMixtureWeight_update_new line 122

def OAI.EditApproximation.rationalOptimizerIterate line 130

Source documentation

Exact rational conditional-gradient iterates.

def rationalOptimizerIterate {ι : Type*} (initial : ι → ℚ) (selected : ℕ → ι → ℚ) :
    ℕ → ι → ℚ
  | 0 => initial
  | j + 1 => fun i =>
    (1 - 2 / ((j : ℚ) + 2)) * rationalOptimizerIterate initial selected j i +
      (2 / ((j : ℚ) + 2)) * selected j i

/-- After the first update, the initial vertex has weight zero. The
remaining iterates are exactly the explicit rational triangular mixture
used by the fair-bit sampler in Section 9. -/

theorem OAI.EditApproximation.rationalOptimizerIterate_eq_mixture line 140
Source documentation
After the first update, the initial vertex has weight zero. The remaining iterates are exactly the explicit rational triangular mixture used by the fair-bit sampler in Section 9.
```
theorem rationalOptimizerIterate_eq_mixture {ι : Type*}
    (initial : ι → ℚ) (selected : ℕ → ι → ℚ) (K : ℕ) (i : ι) :
    rationalOptimizerIterate initial selected (K + 1) i =
      ∑ j ∈ range (K + 1), optimizerMixtureWeight (K + 1) j * selected j i := by
…
```
Mentions: OAI.EditApproximation.rationalOptimizerIterate, OAI.EditApproximation.optimizerMixtureWeight
theorem OAI.EditApproximation.optimizerTriangularMass_succ line 160
Source documentation
Cumulative integer mass for the triangular exact sampler.
```
theorem optimizerTriangularMass_succ (K : ℕ) :
    optimizerTriangularMass (K + 1) = optimizerTriangularMass K + (K + 1) := by
…
```
Mentions: OAI.EditApproximation.optimizerTriangularMass
theorem OAI.EditApproximation.optimizerTriangularMass_twice line 165
theorem OAI.EditApproximation.optimizerSampler_block_card line 175
Source documentation
The integers assigned to selection index j form a block of exactly j+1 points.
```
theorem optimizerSampler_block_card (j : ℕ) :
    (Icc (optimizerTriangularMass j + 1) (optimizerTriangularMass (j + 1))).card = j + 1 := by
…
```
Mentions: OAI.EditApproximation.optimizerTriangularMass
theorem OAI.EditApproximation.optimizerSampler_block_weight line 182
Source documentation
Counting the fair uniform integer sampler gives exactly the stored mixture weights, including repeated selected vertices.
```
theorem optimizerSampler_block_weight (K j : ℕ) (hK : 0 < K) :
    ((j + 1 : ℕ) : ℚ) / optimizerTriangularMass K = optimizerMixtureWeight K j := by
…
```
Mentions: OAI.EditApproximation.optimizerTriangularMass, OAI.EditApproximation.optimizerMixtureWeight
theorem OAI.EditApproximation.entropy_smoothing_upper line 195
Source documentation
The increase of -x log x after adding a positive smoothing parameter is bounded by that parameter's own entropy.
```
theorem entropy_smoothing_upper (x σ : ℝ) (hx : 0 ≤ x) (hσ : 0 < σ) :
    Real.negMulLog (x + σ) - Real.negMulLog x ≤ Real.negMulLog σ := by
…
```
theorem OAI.EditApproximation.entropy_smoothing_lower line 211
Source documentation
The negative change in the smoothed entropy coordinate is linear in the smoothing parameter on the relevant interval [0,2].
```
theorem entropy_smoothing_lower (x σ : ℝ) (hx : 0 ≤ x) (hσ : 0 < σ)
    (hupper : x + σ ≤ 2) :
    Real.negMulLog x - Real.negMulLog (x + σ) ≤ 2 * σ := by
…
```
theorem OAI.EditApproximation.negMulLog_le_two_sqrt line 235

theorem OAI.EditApproximation.entropy_smoothing_coordinate line 252

Source documentation

A uniform coordinate modulus for entropy smoothing, valid including zero coordinates.

theorem entropy_smoothing_coordinate (x σ : ℝ)
    (hx : 0 ≤ x) (hx1 : x ≤ 1) (hσ : 0 < σ) (hσ1 : σ ≤ 1) :
    |Real.negMulLog (x + σ) - Real.negMulLog x| ≤ 2 * Real.sqrt σ := by
…

theorem OAI.EditApproximation.finite_entropy_smoothing_bound line 267

Source documentation

Manuscript Equation eq:entropy-smoothing, with a slightly stronger constant from the coordinate estimate. The linear coefficient vector cancels, so the bound is independent of its magnitude.

theorem finite_entropy_smoothing_bound {ι : Type*} (coordinates : Finset ι)
    (p objective : ι → ℝ) (σ η : ℝ)
    (hp : ∀ i ∈ coordinates, 0 ≤ p i)
    (hpsum : ∑ i ∈ coordinates, p i = 1)
    (hσ : 0 < σ) (hσ1 : σ ≤ 1) :
    |((∑ i ∈ coordinates, Real.negMulLog (p i + σ)) +
        η * ∑ i ∈ coordinates, objective i * p i) -
      entropyValue coordinates η objective p| ≤ 4 * coordinates.card * Real.sqrt σ := by
…

Mentions: OAI.EditApproximation.entropyValue

theorem OAI.EditApproximation.entropy_quadratic_hasDerivAt line 297
theorem OAI.EditApproximation.entropy_quadratic_convex line 308
Source documentation
Negative entropy minus half the square is convex on the probability coordinate interval. This is the exact curvature bound used for the objective-gap estimate in the finite optimizer.
```
theorem entropy_quadratic_convex :
    ConvexOn ℝ (Set.Icc (0 : ℝ) 1) (fun z : ℝ => z * Real.log z - z ^ 2 / 2) := by
…
```

theorem OAI.EditApproximation.entropy_coordinate_strong_gap line 332

Source documentation

The entropy coordinate gap is at least half the squared coordinate distance, including the competitor value zero by continuity.

theorem entropy_coordinate_strong_gap (x y : ℝ)
    (hx : 0 ≤ x) (hx1 : x ≤ 1) (hy : 0 < y) (hy1 : y ≤ 1) :
    (x - y) ^ 2 / 2 ≤
      x * Real.log x - y * Real.log y - (Real.log y + 1) * (x - y) := by
…

theorem OAI.EditApproximation.finite_relative_entropy_sq_gap line 352

Source documentation

Relative entropy dominates half the squared Euclidean distance on the finite probability simplex.

theorem finite_relative_entropy_sq_gap {ι : 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) :
    (∑ i ∈ coordinates, (q i - p i) ^ 2) / 2 ≤
      ∑ i ∈ coordinates, q i * Real.log (q i / p i) := by
…

theorem OAI.EditApproximation.entropy_gap_to_l1 line 376

Source documentation

A true entropy-objective gap controls the ℓ₁ error of a feasible mixture, with the manuscript's exact factor sqrt (2d gap).

theorem entropy_gap_to_l1 {ι : Type*} (coordinates : Finset ι)
    (Q : Set (ι → ℝ)) (η : ℝ) (objective maximizer mixture : ι → ℝ)
    (hconvex : Convex ℝ Q) (hmaxQ : maximizer ∈ Q) (hmixQ : mixture ∈ Q)
    (hmax : ∀ i ∈ coordinates, 0 < maximizer i)
    (hmix : ∀ i ∈ coordinates, 0 ≤ mixture i)
    (hmaxsum : ∑ i ∈ coordinates, maximizer i = 1)
    (hmixsum : ∑ i ∈ coordinates, mixture i = 1)
    (hmaximize : IsMaxOn (entropyValue coordinates η objective) Q maximizer) :
    (∑ i ∈ coordinates, |mixture i - maximizer i|) ≤
      Real.sqrt (2 * coordinates.card *
        (entropyValue coordinates η objective maximizer -
          entropyValue coordinates η objective mixture)) := by
…

Mentions: OAI.EditApproximation.entropyValue

theorem OAI.EditApproximation.smoothing_gap_transfer line 407

Source documentation

Converting a uniform smoothing error and a smoothed objective gap to a gap for the true entropy objective.

theorem smoothing_gap_transfer (trueBest trueValue smoothBest smoothValue error gap : ℝ)
    (hbest : trueBest ≤ smoothBest + error)
    (hvalue : smoothValue ≤ trueValue + error)
    (hgap : smoothBest - smoothValue ≤ gap) :
    trueBest - trueValue ≤ gap + 2 * error := by linarith

theorem OAI.EditApproximation.optimizer_work_budget_gap line 413
theorem OAI.EditApproximation.optimizer_smoothing_root line 424
theorem OAI.EditApproximation.optimizer_explicit_gap_budget line 432
Source documentation
The explicit total objective-gap bound after the prescribed number of fixed-step updates.
```
theorem optimizer_explicit_gap_budget (G d : ℝ) (hG : 4 ≤ G) (hd : d ≤ G) :
    2 / G ^ 20 + 8 / G ^ 30 + 8 * d / G ^ 25 ≤ 12 / G ^ 20 := by
…
```

theorem OAI.EditApproximation.optimizer_final_l1_precision line 457

Source documentation

The quantitative final H^(-3) precision calculation. The squared distance premise is supplied by the proved entropy/KL curvature bound.

theorem optimizer_final_l1_precision (H G d distance gap : ℝ)
    (hH : 4 ≤ H) (hHG : H ≤ G) (hd : 0 ≤ d) (hdG : d ≤ G)
    (hsquared : distance ^ 2 ≤ 2 * d * gap) (hgap : gap ≤ 12 / G ^ 20) :
    distance ≤ 1 / H ^ 3 := by
…

theorem OAI.EditApproximation.rationalLogApproximation_cast line 505
Source documentation
Rational truncated logarithm used for the entropy-gradient calculation. Its evaluation uses only rational arithmetic.
```
theorem rationalLogApproximation_cast (r : ℚ) (K : ℕ) :
    (rationalLogApproximation r K : ℝ) =
      2 * ∑ k ∈ range K,
        ((((r : ℝ) - 1) / ((r : ℝ) + 1)) ^ (2 * k + 1) / (2 * k + 1)) := by
…
```
Mentions: OAI.EditApproximation.rationalLogApproximation
theorem OAI.EditApproximation.logarithm_symmetric_parameter_bound line 513
theorem OAI.EditApproximation.logarithm_series_error line 535
Source documentation
Explicit logarithm-series remainder for the rational gradient routine. Mathlib's logarithm remainder is specialized to the bounded smoothed-coordinate interval. Its bound suffices for the prescribed polynomial truncation length.
```
theorem logarithm_series_error (r σ : ℝ) (K : ℕ)
    (hσ : 0 < σ) (hσhalf : σ ≤ 1 / 2)
    (hr : σ ≤ r) (hrupper : r ≤ 1 + σ) :
    |Real.log r - 2 * ∑ k ∈ range K,
        (((r - 1) / (r + 1)) ^ (2 * k + 1) / (2 * k + 1))| ≤
      2 * Real.exp (-2 * K * σ) / σ := by
…
```
theorem OAI.EditApproximation.rationalLogApproximation_error line 579
theorem OAI.EditApproximation.logarithm_truncation_exponential_budget line 587

theorem OAI.EditApproximation.rationalLogApproximation_prescribed_precision line 620

Source documentation

The prescribed rational logarithm computation has the required absolute gradient precision G^(-20) after G^60 rational terms.

theorem rationalLogApproximation_prescribed_precision (r : ℚ) (G : ℕ)
    (hG : 4 ≤ G)
    (hr : 1 / (G : ℝ) ^ 50 ≤ (r : ℝ))
    (hrupper : (r : ℝ) ≤ 1 + 1 / (G : ℝ) ^ 50) :
    |Real.log (r : ℝ) - (rationalLogApproximation r (G ^ 60) : ℝ)| ≤
      1 / (G : ℝ) ^ 20 := by
…

Mentions: OAI.EditApproximation.rationalLogApproximation

theorem OAI.EditApproximation.finite_gradient_error line 648

theorem OAI.EditApproximation.approximate_gradient_linearization_loss line 667

Source documentation

Enumerating the vertices with an approximate gradient loses at most 2e₀ in the true linearization, even against an arbitrary feasible mixture.

theorem approximate_gradient_linearization_loss {ι : Type*} (coordinates : Finset ι)
    (gradient approximateGradient selected competitor : ι → ℝ) (error : ℝ)
    (hselected : ∀ i ∈ coordinates, 0 ≤ selected i)
    (hcompetitor : ∀ i ∈ coordinates, 0 ≤ competitor i)
    (hselectedSum : ∑ i ∈ coordinates, selected i = 1)
    (hcompetitorSum : ∑ i ∈ coordinates, competitor i = 1)
    (herror : ∀ i ∈ coordinates, |approximateGradient i - gradient i| ≤ error)
    (hchoose : (∑ i ∈ coordinates, approximateGradient i * competitor i) ≤
      ∑ i ∈ coordinates, approximateGradient i * selected i) :
    (∑ i ∈ coordinates, gradient i * competitor i) -
        (∑ i ∈ coordinates, gradient i * selected i) ≤ 2 * error := by
…

def OAI.EditApproximation.smoothedEntropyValue line 687
def OAI.EditApproximation.smoothedEntropyGradient line 691

theorem OAI.EditApproximation.smoothed_entropy_coordinate_upper line 696

Source documentation

Tangent upper bound for a single smoothed entropy coordinate.

theorem smoothed_entropy_coordinate_upper (x y σ linear : ℝ)
    (hx : 0 ≤ x) (hy : 0 ≤ y) (hσ : 0 < σ) :
    (Real.negMulLog (y + σ) + linear * y) -
        (Real.negMulLog (x + σ) + linear * x) ≤
      (-Real.log (x + σ) - 1 + linear) * (y - x) := by
…

theorem OAI.EditApproximation.smoothed_entropy_coordinate_lower line 716

Source documentation

A scalar smoothness bound obtained directly from log u ≤ u-1. The coefficient 1/σ combines with the sharper simplex diameter below to give the manuscript's exact 2 ξ²/σ remainder.

theorem smoothed_entropy_coordinate_lower (x y σ linear : ℝ)
    (hx : 0 ≤ x) (hy : 0 ≤ y) (hσ : 0 < σ) :
    (-Real.log (x + σ) - 1 + linear) * (y - x) - (y - x) ^ 2 / σ ≤
      (Real.negMulLog (y + σ) + linear * y) -
        (Real.negMulLog (x + σ) + linear * x) := by
…

theorem OAI.EditApproximation.probability_vectors_sq_distance_le_two line 738
theorem OAI.EditApproximation.smoothed_entropy_tangent_upper line 756
theorem OAI.EditApproximation.smoothed_entropy_mixture_lower line 766

theorem OAI.EditApproximation.smoothed_frank_wolfe_recurrence line 816

Source documentation

The manuscript's fixed-step optimizer recurrence follows from the actual smoothed entropy objective and approximate gradient selection.

theorem smoothed_frank_wolfe_recurrence {ι : Type*} (coordinates : Finset ι)
    (σ ξ error : ℝ) (linear p selected best approximateGradient : ι → ℝ)
    (hp : ∀ i ∈ coordinates, 0 ≤ p i)
    (hselected : ∀ i ∈ coordinates, 0 ≤ selected i)
    (hbest : ∀ i ∈ coordinates, 0 ≤ best i)
    (hpsum : ∑ i ∈ coordinates, p i = 1)
    (hselectedSum : ∑ i ∈ coordinates, selected i = 1)
    (hbestSum : ∑ i ∈ coordinates, best i = 1)
    (hσ : 0 < σ) (hξ : 0 ≤ ξ) (hξ1 : ξ ≤ 1)
    (hgradient : ∀ i ∈ coordinates,
      |approximateGradient i - smoothedEntropyGradient σ linear p i| ≤ error)
    (hchoose : (∑ i ∈ coordinates, approximateGradient i * best i) ≤
…

Mentions: OAI.EditApproximation.smoothedEntropyGradient

theorem OAI.EditApproximation.rationalOptimizerIterate_cast_step line 856

Source documentation

Casting the exact rational update gives precisely the analytic step.

theorem rationalOptimizerIterate_cast_step {ι : Type*}
    (initial : ι → ℚ) (selected : ℕ → ι → ℚ) (j : ℕ) :
    (fun i => (rationalOptimizerIterate initial selected (j + 1) i : ℝ)) =
      (fun i => (1 - frankWolfeStep j) * (rationalOptimizerIterate initial selected j i : ℝ) +
        frankWolfeStep j * (selected j i : ℝ)) := by
…

Mentions: OAI.EditApproximation.rationalOptimizerIterate, OAI.EditApproximation.frankWolfeStep

theorem OAI.EditApproximation.rationalOptimizerIterate_probability line 865

Source documentation

All exact rational iterates are probability vectors.

theorem rationalOptimizerIterate_probability {ι : Type*} (coordinates : Finset ι)
    (initial : ι → ℚ) (selected : ℕ → ι → ℚ)
    (hinitial : ∀ i ∈ coordinates, (0 : ℝ) ≤ initial i)
    (hinitialSum : ∑ i ∈ coordinates, (initial i : ℝ) = 1)
    (hselected : ∀ j i, i ∈ coordinates → (0 : ℝ) ≤ selected j i)
    (hselectedSum : ∀ j, ∑ i ∈ coordinates, (selected j i : ℝ) = 1) :
    ∀ j, (∀ i ∈ coordinates, (0 : ℝ) ≤ rationalOptimizerIterate initial selected j i) ∧
      (∑ i ∈ coordinates, (rationalOptimizerIterate initial selected j i : ℝ)) = 1 := by
…

Mentions: OAI.EditApproximation.rationalOptimizerIterate

theorem OAI.EditApproximation.rationalOptimizerIterate_mem line 889

Source documentation

Convex feasibility is preserved by the actual rational iterates.

theorem rationalOptimizerIterate_mem {ι : Type*}
    (Q : Set (ι → ℝ)) (initial : ι → ℚ) (selected : ℕ → ι → ℚ)
    (hconvex : Convex ℝ Q) (hinitial : (fun i => (initial i : ℝ)) ∈ Q)
    (hselected : ∀ j, (fun i => (selected j i : ℝ)) ∈ Q) :
    ∀ j, (fun i => (rationalOptimizerIterate initial selected j i : ℝ)) ∈ Q := by
…

Mentions: OAI.EditApproximation.rationalOptimizerIterate

theorem OAI.EditApproximation.rational_optimizer_smoothed_gap_bound line 904

Source documentation

Objective convergence of the exact rational implementation follows from the proved smoothness and rational approximate-gradient choices.

theorem rational_optimizer_smoothed_gap_bound {ι : Type*} (coordinates : Finset ι)
    (σ error : ℝ) (linear best : ι → ℝ) (initial : ι → ℚ)
    (selected : ℕ → ι → ℚ) (approximateGradient : ℕ → ι → ℝ)
    (hinitial : ∀ i ∈ coordinates, (0 : ℝ) ≤ initial i)
    (hinitialSum : ∑ i ∈ coordinates, (initial i : ℝ) = 1)
    (hselected : ∀ j i, i ∈ coordinates → (0 : ℝ) ≤ selected j i)
    (hselectedSum : ∀ j, ∑ i ∈ coordinates, (selected j i : ℝ) = 1)
    (hbest : ∀ i ∈ coordinates, 0 ≤ best i)
    (hbestSum : ∑ i ∈ coordinates, best i = 1) (hσ : 0 < σ)
    (hgradient : ∀ j i, i ∈ coordinates →
      |approximateGradient j i - smoothedEntropyGradient σ linear
        (fun i => (rationalOptimizerIterate initial selected j i : ℝ)) i| ≤ error)
…

Mentions: OAI.EditApproximation.smoothedEntropyGradient, OAI.EditApproximation.rationalOptimizerIterate

theorem OAI.EditApproximation.rationalSmoothedGradient_precision line 937

Source documentation

The actual rational gradient routine, including exact linear terms.

theorem rationalSmoothedGradient_precision {ι : Type*} (coordinates : Finset ι)
    (G : ℕ) (linear p : ι → ℚ) (hG : 4 ≤ G)
    (hp : ∀ i ∈ coordinates, (0 : ℝ) ≤ p i)
    (hpsum : ∑ i ∈ coordinates, (p i : ℝ) = 1) :
    ∀ i ∈ coordinates,
      |(rationalSmoothedGradient G linear p i : ℝ) -
        smoothedEntropyGradient (1 / (G : ℝ) ^ 50)
          (fun i => (linear i : ℝ)) (fun i => (p i : ℝ)) i| ≤ 1 / (G : ℝ) ^ 20 := by
…

Mentions: OAI.EditApproximation.rationalSmoothedGradient, OAI.EditApproximation.smoothedEntropyGradient

theorem OAI.EditApproximation.rational_optimizer_true_gap_precision line 962

Source documentation

The prescribed number of exact rational updates reaches the true entropy-objective precision, with no assumed analytic recurrence.

theorem rational_optimizer_true_gap_precision {ι : Type*} (coordinates : Finset ι)
    (G : ℕ) (linear initial : ι → ℚ) (selected : ℕ → ι → ℚ) (best : ι → ℝ)
    (hG : 4 ≤ G) (hdG : coordinates.card ≤ G)
    (hinitial : ∀ i ∈ coordinates, (0 : ℝ) ≤ initial i)
    (hinitialSum : ∑ i ∈ coordinates, (initial i : ℝ) = 1)
    (hselected : ∀ j i, i ∈ coordinates → (0 : ℝ) ≤ selected j i)
    (hselectedSum : ∀ j, ∑ i ∈ coordinates, (selected j i : ℝ) = 1)
    (hbest : ∀ i ∈ coordinates, 0 ≤ best i)
    (hbestSum : ∑ i ∈ coordinates, best i = 1)
    (hchoose : ∀ j,
      (∑ i ∈ coordinates, (rationalSmoothedGradient G linear
        (rationalOptimizerIterate initial selected j) i : ℝ) * best i) ≤
…

Mentions: OAI.EditApproximation.rationalSmoothedGradient, OAI.EditApproximation.rationalOptimizerIterate

theorem OAI.EditApproximation.rational_optimizer_l1_precision line 1046

Source documentation

The final distance guarantee for the prescribed rational updates. Only their concrete finite linearization choices remain as input.

theorem rational_optimizer_l1_precision {ι : Type*} (coordinates : Finset ι)
    (Q : Set (ι → ℝ)) (H G : ℕ) (linear initial : ι → ℚ)
    (selected : ℕ → ι → ℚ) (maximizer : ι → ℝ)
    (hH : 4 ≤ H) (hHG : H ≤ G) (hdG : coordinates.card ≤ G)
    (hconvex : Convex ℝ Q) (hinitialQ : (fun i => (initial i : ℝ)) ∈ Q)
    (hselectedQ : ∀ j, (fun i => (selected j i : ℝ)) ∈ Q)
    (hmaxQ : maximizer ∈ Q)
    (hinitial : ∀ i ∈ coordinates, (0 : ℝ) ≤ initial i)
    (hinitialSum : ∑ i ∈ coordinates, (initial i : ℝ) = 1)
    (hselected : ∀ j i, i ∈ coordinates → (0 : ℝ) ≤ selected j i)
    (hselectedSum : ∀ j, ∑ i ∈ coordinates, (selected j i : ℝ) = 1)
    (hmax : ∀ i ∈ coordinates, 0 < maximizer i)
…

theorem OAI.EditApproximation.finite_linearization_maximizes_convexHull line 1094

Source documentation

Maximizing a finite list's linearization also maximizes it on the real convex hull.

theorem finite_linearization_maximizes_convexHull {ι : Type*} (coordinates : Finset ι)
    (vertices : Set (ι → ℝ)) (gradient selected : ι → ℝ)
    (hchoose : ∀ p ∈ vertices,
      (∑ i ∈ coordinates, gradient i * p i) ≤ ∑ i ∈ coordinates, gradient i * selected i) :
    ∀ p ∈ convexHull ℝ vertices,
      (∑ i ∈ coordinates, gradient i * p i) ≤ ∑ i ∈ coordinates, gradient i * selected i := by
…

theorem OAI.EditApproximation.rationalLinearizationMaximizer_spec line 1122

Source documentation

Executable finite rational comparisons, with the first listed maximizer selected in a tie. The fallback only applies to an empty list.

theorem rationalLinearizationMaximizer_spec {ι : Type*} (coordinates : Finset ι)
    (vertices : List (ι → ℚ)) (gradient : ι → ℚ) (hvertices : vertices ≠ []) :
    rationalLinearizationMaximizer coordinates vertices gradient ∈ vertices ∧
      ∀ p ∈ vertices, (∑ i ∈ coordinates, gradient i * p i) ≤
        ∑ i ∈ coordinates, gradient i * rationalLinearizationMaximizer coordinates vertices gradient i := by
…

Mentions: OAI.EditApproximation.rationalLinearizationMaximizer

def OAI.EditApproximation.finiteOptimizerSelection line 1142
Source documentation
The finite rational optimizer: every operation here is rational arithmetic, finite enumeration, or the prescribed finite logarithm sum.
```
def finiteOptimizerSelection {ι : Type*} (coordinates : Finset ι)
    (vertices : List (ι → ℚ)) (linear : ι → ℚ) (G j : ℕ) : ι → ℚ :=
…
```
theorem OAI.EditApproximation.finiteRationalOptimizer_eq_iterate line 1147
def OAI.EditApproximation.rationalVertexSet line 1161

theorem OAI.EditApproximation.rationalVertexHull_probability line 1165

Source documentation

Every vector in the listed real convex hull is a probability vector.

theorem rationalVertexHull_probability {ι : Type*} (coordinates : Finset ι)
    (vertices : List (ι → ℚ))
    (hvertices : ∀ p ∈ vertices,
      (∀ i ∈ coordinates, (0 : ℝ) ≤ p i) ∧ (∑ i ∈ coordinates, (p i : ℝ)) = 1) :
    ∀ p ∈ convexHull ℝ (rationalVertexSet vertices),
      (∀ i ∈ coordinates, 0 ≤ p i) ∧ (∑ i ∈ coordinates, p i) = 1 := by
…

Mentions: OAI.EditApproximation.rationalVertexSet

theorem OAI.EditApproximation.finiteOptimizerSelection_maximizes line 1186

Source documentation

Concrete finite vertex selection satisfies the required linearization inequality against every real feasible mixture.

theorem finiteOptimizerSelection_maximizes {ι : Type*} (coordinates : Finset ι)
    (vertices : List (ι → ℚ)) (linear : ι → ℚ) (G j : ℕ)
    (hvertices : vertices ≠ []) :
    ∀ best ∈ convexHull ℝ (rationalVertexSet vertices),
      (∑ i ∈ coordinates, (rationalSmoothedGradient G linear
        (finiteRationalOptimizer coordinates vertices linear G j) i : ℝ) * best i) ≤
      ∑ i ∈ coordinates, (rationalSmoothedGradient G linear
        (finiteRationalOptimizer coordinates vertices linear G j) i : ℝ) *
        (finiteOptimizerSelection coordinates vertices linear G j i : ℝ) := by
…

Mentions: OAI.EditApproximation.rationalVertexSet, OAI.EditApproximation.rationalSmoothedGradient, OAI.EditApproximation.finiteRationalOptimizer, OAI.EditApproximation.finiteOptimizerSelection

theorem OAI.EditApproximation.finiteRationalOptimizer_l1_precision line 1205

Source documentation

Accuracy of the executable rational optimizer at every positive entropy maximizer of its listed action hull.

theorem finiteRationalOptimizer_l1_precision {ι : Type*} (coordinates : Finset ι)
    (vertices : List (ι → ℚ)) (linear : ι → ℚ) (H : ℕ) (maximizer : ι → ℝ)
    (hvertices : vertices ≠ []) (hH : 4 ≤ H)
    (hprobability : ∀ p ∈ vertices,
      (∀ i ∈ coordinates, (0 : ℝ) ≤ p i) ∧ (∑ i ∈ coordinates, (p i : ℝ)) = 1)
    (hmaxQ : maximizer ∈ convexHull ℝ (rationalVertexSet vertices))
    (hmax : ∀ i ∈ coordinates, 0 < maximizer i)
    (hmaximize : IsMaxOn (entropyValue coordinates 1 (fun i => (linear i : ℝ)))
      (convexHull ℝ (rationalVertexSet vertices)) maximizer) :
    (∑ i ∈ coordinates, |(finiteRationalOptimizer coordinates vertices linear
      (H + coordinates.card + 2) ((H + coordinates.card + 2) ^ 80) i : ℝ) - maximizer i|) ≤
        1 / (H : ℝ) ^ 3 := by
…

Mentions: OAI.EditApproximation.rationalVertexSet, OAI.EditApproximation.entropyValue, OAI.EditApproximation.finiteRationalOptimizer

theorem OAI.EditApproximation.rationalVertexHull_positive_witness line 1246

Source documentation

Averaging the finite action list gives a feasible vector positive at every covered coordinate, including lists with repeated actions.

theorem rationalVertexHull_positive_witness {ι : Type*} (coordinates : Finset ι)
    (vertices : List (ι → ℚ)) (hvertices : vertices ≠ [])
    (hnonnegative : ∀ p ∈ vertices, ∀ i ∈ coordinates, (0 : ℝ) ≤ p i)
    (hcovered : ∀ i ∈ coordinates, ∃ p ∈ vertices, (0 : ℝ) < p i) :
    ∃ witness ∈ convexHull ℝ (rationalVertexSet vertices),
      ∀ i ∈ coordinates, 0 < witness i := by
…

Mentions: OAI.EditApproximation.rationalVertexSet

theorem OAI.EditApproximation.finite_entropy_optimizer line 1278

Source documentation

The finite optimizer accuracy theorem with exactly the manuscript's probability and coordinate-coverage assumptions. The returned point is the executable rational construction defined above.

theorem finite_entropy_optimizer {ι : Type*} (coordinates : Finset ι)
    (vertices : List (ι → ℚ)) (linear : ι → ℚ) (H : ℕ)
    (hvertices : vertices ≠ []) (hH : 4 ≤ H)
    (hprobability : ∀ p ∈ vertices,
      (∀ i ∈ coordinates, (0 : ℝ) ≤ p i) ∧ (∑ i ∈ coordinates, (p i : ℝ)) = 1)
    (hcovered : ∀ i ∈ coordinates, ∃ p ∈ vertices, (0 : ℝ) < p i) :
    ∃ maximizer ∈ convexHull ℝ (rationalVertexSet vertices),
      IsMaxOn (entropyValue coordinates 1 (fun i => (linear i : ℝ)))
        (convexHull ℝ (rationalVertexSet vertices)) maximizer ∧
      (∑ i ∈ coordinates, |(finiteRationalOptimizer coordinates vertices linear
        (H + coordinates.card + 2) ((H + coordinates.card + 2) ^ 80) i : ℝ) - maximizer i|) ≤
          1 / (H : ℝ) ^ 3 := by
…

Mentions: OAI.EditApproximation.rationalVertexSet, OAI.EditApproximation.entropyValue, OAI.EditApproximation.finiteRationalOptimizer