ControlCartPole

CartPole equations/constants: Farama Gymnasium classic_control/cartpole.py. Explicit Euler, dt=0.02, Boolean action=false/true gives -10/+10 N. Deterministic initial states and a shaped LOSS are used here (not Gym reward).
Imports
import Control; open Control; import Math;
Table of Contents

Types

ControlCartPole

(inductive)
inductive ControlCartPole

Constructors

For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.

ControlCartPole (inductive)

mk

constructor
ControlCartPole

Functions

position

def position (s : ControlCartPole) : Float

velocity

def velocity (s : ControlCartPole) : Float

angle

def angle (s : ControlCartPole) : Float

angular_velocity

def angular_velocity (s : ControlCartPole) : Float

step

def step (s : ControlCartPole) (right : Bool) : ControlCartPole

invalid

def invalid (s : ControlCartPole) : Bool

linear

def linear (angle_gain : Float) (rate_gain : Float) (x : Float) (v : Float) (theta : Float) (rate : Float) : Bool

reference

def reference (x : Float) (v : Float) (theta : Float) (rate : Float) : Bool

left

def left (x : Float) (v : Float) (theta : Float) (rate : Float) : Bool

advance

def advance (policy : (x : Float) → (v : Float) → (theta : Float) → (rate : Float) → Bool) (s : ControlCartPole) : ControlCartPole

cost

def cost (s : ControlCartPole) : Float

episode

def episode (horizon : Int | horizon ≥ 0 && horizon ≤ 500) (policy : (x : Float) → (v : Float) → (theta : Float) → (rate : Float) → Bool) (initial : ControlCartPole) : Control

training

def training (policy : (x : Float) → (v : Float) → (theta : Float) → (rate : Float) → Bool) : Float

held_out

def held_out (policy : (x : Float) → (v : Float) → (theta : Float) → (rate : Float) → Bool) : Float