ListBandRegret.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Regret and sampling for the literal finite band list

The numerical optimizer and exact sampler keep the same listed vertex order. Passing to the finite set is used only for coordinate support and convex-hull facts, never to reorder the executable optimizer.

theorem OAI.EditApproximation.rationalVertexSet_band_list line 19

theorem OAI.EditApproximation.list_band_computed_entropy_regret line 29

Source documentation

Actual finite-list specialization of the computed entropy optimizer.

theorem list_band_computed_entropy_regret {β σ : Type*} [Fintype β] [Nonempty β]
    [DecidableEq β] [DecidableEq σ] (band : List (β → σ)) (hband : band ≠ [])
    (mass : β → ℚ) (hpos : ∀ child, 0 < mass child)
    (S H : ℕ) (η κ : ℚ) (rangeBound : ℝ)
    (gain decrement : ℕ → β × σ → ℚ) {comparison : β → σ} (hc : comparison ∈ band)
    (hH : 4 ≤ H) (hη : 0 < η) (hκ : 0 ≤ κ) (hκhalf : κ ≤ 1 / 2)
    (hηrange : (η : ℝ) * rangeBound ≤ (κ : ℝ))
    (hdecrementNonneg : ∀ t < S, ∀ i ∈ bandCoordinates band.toFinset, (0 : ℝ) ≤ decrement t i)
    (hrange : ∀ t < S, ∀ i ∈ bandCoordinates band.toFinset, ∀ j ∈ bandCoordinates band.toFinset,
      i.1 = j.1 → |(decrement t i : ℝ) - decrement t j| ≤ rangeBound)
    (hdecrement : ∀ i ∈ bandCoordinates band.toFinset, ∑ t ∈ range S, (decrement t i : ℝ) ≤ 1)
    (hgain : ∀ t < S, ∀ i ∈ bandCoordinates band.toFinset,
…

Mentions: OAI.EditApproximation.bandCoordinates

theorem OAI.EditApproximation.finiteOptimizerActionDraw_linear_mean line 79

theorem OAI.EditApproximation.finiteOptimizerActionDraw_child_cost_mean line 99

Source documentation

Exact expected weighted child cost of the returned optimizer action.

theorem finiteOptimizerActionDraw_child_cost_mean {β σ : Type*} [Fintype β] [Nonempty β]
    [DecidableEq β] [DecidableEq σ] (band : List (β → σ)) (hband : band ≠ [])
    (mass : β → ℚ) (hpos : ∀ child, 0 < mass child)
    (table : ℕ → β × σ → ℚ) (κ : ℚ) (t : ℕ)
    (linear : β × σ → ℚ) (G K : ℕ) (hK : 0 < K) :
    uniformMean (fun integer : Fin (optimizerTriangularMass K) =>
      let action := finiteOptimizerActionDraw band hband mass linear G K integer
…

Mentions: OAI.EditApproximation.uniformMean, OAI.EditApproximation.optimizerTriangularMass, OAI.EditApproximation.finiteOptimizerActionDraw