OAI/Combinatorics/EditApproximation/Geometry/BandRegret.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.rationalOptimisticHistory_cast line 21
2. def OAI.EditApproximation.computedOnlineVector line 30
3. theorem OAI.EditApproximation.rationalOnlineLinear_objective line 36
4. theorem OAI.EditApproximation.computed_finite_block_entropy_regret line 51

   Source documentation

   Fixed-block regret for the actual rational optimizer, with its prescribed G^80 iterations and H^-3 numerical loss.

   theorem computed_finite_block_entropy_regret {ι β : Type*} [Fintype β] [DecidableEq β]
       (coordinates : Finset ι) (block : ι → β) (vertices : List (ι → ℚ))
       (S H : ℕ) (η κ : ℚ) (rangeBound : ℝ)
       (gain decrement : ℕ → ι → ℚ) (comparator : ι → ℝ)
       (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)
       (hcQ : comparator ∈ convexHull ℝ (rationalVertexSet vertices))
       (hblocks : ∀ b, (coordinates.filter (fun i => block i = b)).Nonempty)
       (hblockMass : ∀ p ∈ convexHull ℝ (rationalVertexSet vertices),
         ∀ q ∈ convexHull ℝ (rationalVertexSet vertices), ∀ b,
   …

   Mentions: OAI.EditApproximation.rationalVertexSet

5. theorem OAI.EditApproximation.band_computed_entropy_regret line 124

   Source documentation

   Specialization to the actual child/state coordinates and rational fixed child masses of a nonempty band.

   theorem band_computed_entropy_regret {β σ : Type*} [Fintype β] [Nonempty β]
       [DecidableEq β] [DecidableEq σ] (band : Finset (β → σ)) (hband : band.Nonempty)
       (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, (0 : ℝ) ≤ decrement t i)
       (hrange : ∀ t < S, ∀ i ∈ bandCoordinates band, ∀ j ∈ bandCoordinates band,
         i.1 = j.1 → |(decrement t i : ℝ) - decrement t j| ≤ rangeBound)
       (hdecrement : ∀ i ∈ bandCoordinates band, ∑ t ∈ range S, (decrement t i : ℝ) ≤ 1)
       (hgain : ∀ t < S, ∀ i ∈ bandCoordinates band,
   …

   Mentions: OAI.EditApproximation.bandCoordinates