ActionVectors.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The actual fixed-block action hull

Coordinates are precisely the child/state pairs occurring in a finite band. Each action assigns its fixed rational child mass to one state per child. This verifies the probability, coverage and block-mass hypotheses used by the numerical optimizer and optimistic entropy regret.

theorem OAI.EditApproximation.action_coordinate_mem line 24
theorem OAI.EditApproximation.actionVector_probability line 30
theorem OAI.EditApproximation.actionVector_coordinate_coverage line 67
theorem OAI.EditApproximation.actionVector_block_mass line 81
theorem OAI.EditApproximation.actionVector_inner_product line 98

theorem OAI.EditApproximation.actionVector_cost_identity line 126

Source documentation

The coordinate normalization translates entropy gains exactly into the unnormalized costs of a band action.

theorem actionVector_cost_identity {β σ : Type*} [Fintype β] [Nonempty β]
    [DecidableEq β] [DecidableEq σ] (band : Finset (β → σ))
    (mass : β → ℚ) (hpos : ∀ child, 0 < mass child) (cost : β × σ → ℝ)
    {action : β → σ} (haction : action ∈ band) :
    -((∑ child, mass child : ℚ) : ℝ) *
      (∑ coordinate ∈ bandCoordinates band,
        (-cost coordinate / (mass coordinate.1 : ℝ)) * (actionVector mass action coordinate : ℝ)) =
          ∑ child, cost (child, action child) := by
…

Mentions: OAI.EditApproximation.bandCoordinates, OAI.EditApproximation.actionVector

theorem OAI.EditApproximation.band_block_nonempty line 143
theorem OAI.EditApproximation.band_hull_block_mass line 149
theorem OAI.EditApproximation.band_entropy_optimizer line 175