AMMLib.State.AMMsNN

source

def AMMs.r0₀ (amms : AMMs) (t0 t1 : T) :

NNReal

Equations

amms.r0₀ t0 t1 = (amms.res t0) t1

Instances For

source

def AMMs.r1₀ (amms : AMMs) (t0 t1 : T) :

NNReal

Equations

amms.r1₀ t0 t1 = (amms.res t1) t0

Instances For

source

@[simp]

theorem AMMs.r0_same₀ (amms : AMMs) (t : T) :

amms.r0₀ t t = 0

source

@[simp]

theorem AMMs.r1_same₀ (amms : AMMs) (t : T) :

amms.r1₀ t t = 0

source

@[simp]

theorem AMMs.r0_toNNReal (amms : AMMs) (t0 t1 : T) (hinit : amms.init t0 t1) :

↑(amms.r0 t0 t1 hinit) = amms.r0₀ t0 t1

source

@[simp]

theorem AMMs.r1_toNNReal (amms : AMMs) (t0 t1 : T) (hinit : amms.init t0 t1) :

↑(amms.r1 t0 t1 hinit) = amms.r1₀ t0 t1

source

theorem AMMs.r0_reorder₀ (amms : AMMs) (t1 t0 : T) :

amms.r0₀ t1 t0 = amms.r1₀ t0 t1

source

theorem AMMs.r1_reorder₀ (amms : AMMs) (t1 t0 : T) :

amms.r1₀ t1 t0 = amms.r0₀ t0 t1

source

@[simp]

theorem AMMs.r0_of_initialize₀ (amms : AMMs) {t0 t1 : T} (hdif : t0 ≠ t1) (r0 r1 : ℝ>0) :

(amms.initialize hdif r0 r1).r0₀ t0 t1 = ↑r0

source

@[simp]

theorem AMMs.r1_of_initialize₀ (amms : AMMs) {t0 t1 : T} (hdif : t0 ≠ t1) (r0 r1 : ℝ>0) :

(amms.initialize hdif r0 r1).r1₀ t0 t1 = ↑r1

source

@[simp]

theorem AMMs.r0_of_initialize_diffpair₀ (amms : AMMs) {t0 t1 : T} (hdif : t0 ≠ t1) (r0 r1 : ℝ>0) (t0' t1' : T) (difp : diffmint t0 t1 t0' t1') :

(amms.initialize hdif r0 r1).r0₀ t0' t1' = amms.r0₀ t0' t1'

source

@[simp]

theorem AMMs.r1_of_initialize_diffpair₀ (amms : AMMs) {t0 t1 : T} (hdif : t0 ≠ t1) (r0 r1 : ℝ>0) (t0' t1' : T) (difp : diffmint t0 t1 t0' t1') :

(amms.initialize hdif r0 r1).r1₀ t0' t1' = amms.r1₀ t0' t1'

source

@[simp]

theorem AMMs.r0_of_add_r0₀ (amms : AMMs) (t0 t1 : T) (x : ℝ>0) (h : amms.init t0 t1) :

(amms.add_r0 t0 t1 h x).r0₀ t0 t1 = ↑x + amms.r0₀ t0 t1

source

@[simp]

theorem AMMs.r0_of_add_r0_diff₀ (amms : AMMs) (t0 t1 : T) (x : ℝ>0) (h : amms.init t0 t1) (t0' t1' : T) (hdiff : diffmint t0 t1 t0' t1') :

(amms.add_r0 t0 t1 h x).r0₀ t0' t1' = amms.r0₀ t0' t1'

source

@[simp]

theorem AMMs.r0_of_add_r1₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) :

(amms.add_r1 t0 t1 h x).r0₀ t0 t1 = amms.r0₀ t0 t1

source

@[simp]

theorem AMMs.r0_of_add_r1_diff₀ (amms : AMMs) (t0 t1 : T) (x : ℝ>0) (h : amms.init t0 t1) (t0' t1' : T) (hdiff : diffmint t0 t1 t0' t1') :

(amms.add_r1 t0 t1 h x).r0₀ t0' t1' = amms.r0₀ t0' t1'

source

@[simp]

theorem AMMs.r1_of_add_r1₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) :

(amms.add_r1 t0 t1 h x).r1₀ t0 t1 = ↑x + amms.r1₀ t0 t1

source

@[simp]

theorem AMMs.r1_of_add_r1_diff₀ (amms : AMMs) (t0 t1 : T) (x : ℝ>0) (h : amms.init t0 t1) (t0' t1' : T) (hdiff : diffmint t0 t1 t0' t1') :

(amms.add_r1 t0 t1 h x).r1₀ t0' t1' = amms.r1₀ t0' t1'

source

@[simp]

theorem AMMs.r1_of_add_r0₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) :

(amms.add_r0 t0 t1 h x).r1₀ t0 t1 = amms.r1₀ t0 t1

source

@[simp]

theorem AMMs.r1_of_add_r0_swapped₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) :

(amms.add_r0 t1 t0 ⋯ x).r1₀ t0 t1 = ↑x + amms.r1₀ t0 t1

source

@[simp]

theorem AMMs.r1_of_add_r1_swapped₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) :

(amms.add_r1 t1 t0 ⋯ x).r1₀ t0 t1 = amms.r1₀ t0 t1

source

@[simp]

theorem AMMs.r0_of_add_r1_swapped₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) :

(amms.add_r1 t1 t0 ⋯ x).r0₀ t0 t1 = ↑x + amms.r0₀ t0 t1

source

@[simp]

theorem AMMs.r0_of_add_r0_swapped₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) :

(amms.add_r0 t1 t0 ⋯ x).r0₀ t0 t1 = amms.r0₀ t0 t1

source

@[simp]

theorem AMMs.r1_of_add_r0_diff₀ (amms : AMMs) (t0 t1 : T) (x : ℝ>0) (h : amms.init t0 t1) (t0' t1' : T) (hdiff : diffmint t0 t1 t0' t1') :

(amms.add_r0 t0 t1 h x).r1₀ t0' t1' = amms.r1₀ t0' t1'

source

@[simp]

theorem AMMs.r0_of_sub_r0₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r0 t0 t1 h) :

(amms.sub_r0 t0 t1 h x h').r0₀ t0 t1 = amms.r0₀ t0 t1 - ↑x

source

@[simp]

theorem AMMs.r0_of_sub_r1₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r1 t0 t1 h) :

(amms.sub_r1 t0 t1 h x h').r0₀ t0 t1 = amms.r0₀ t0 t1

source

@[simp]

theorem AMMs.r1_of_sub_r1₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r1 t0 t1 h) :

(amms.sub_r1 t0 t1 h x h').r1₀ t0 t1 = amms.r1₀ t0 t1 - ↑x

source

@[simp]

theorem AMMs.r1_of_sub_r0₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r0 t0 t1 h) :

(amms.sub_r0 t0 t1 h x h').r1₀ t0 t1 = amms.r1₀ t0 t1

source

@[simp]

theorem AMMs.r0_of_sub_r0_diff₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r0 t0 t1 h) (t0' t1' : T) (hdiff : diffmint t0 t1 t0' t1') :

(amms.sub_r0 t0 t1 h x h').r0₀ t0' t1' = amms.r0₀ t0' t1'

source

@[simp]

theorem AMMs.r0_of_sub_r1_diff₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r1 t0 t1 h) (t0' t1' : T) (hdiff : diffmint t0 t1 t0' t1') :

(amms.sub_r1 t0 t1 h x h').r0₀ t0' t1' = amms.r0₀ t0' t1'

source

@[simp]

theorem AMMs.r1_of_sub_r1_diff₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r1 t0 t1 h) (t0' t1' : T) (hdiff : diffmint t0 t1 t0' t1') :

(amms.sub_r1 t0 t1 h x h').r1₀ t0' t1' = amms.r1₀ t0' t1'

source

@[simp]

theorem AMMs.r1_of_sub_r0_diff₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r0 t0 t1 h) (t0' t1' : T) (hdiff : diffmint t0 t1 t0' t1') :

(amms.sub_r0 t0 t1 h x h').r1₀ t0' t1' = amms.r1₀ t0' t1'

source

@[simp]

theorem AMMs.r0_of_sub_r0_swapped₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r0 t1 t0 ⋯) :

(amms.sub_r0 t1 t0 ⋯ x h').r0₀ t0 t1 = amms.r0₀ t0 t1

source

@[simp]

theorem AMMs.r0_of_sub_r1_swapped₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r1 t1 t0 ⋯) :

(amms.sub_r1 t1 t0 ⋯ x h').r0₀ t0 t1 = amms.r0₀ t0 t1 - ↑x

source

@[simp]

theorem AMMs.r1_of_sub_r1_swapped₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r1 t1 t0 ⋯) :

(amms.sub_r1 t1 t0 ⋯ x h').r1₀ t0 t1 = amms.r1₀ t0 t1

source

@[simp]

theorem AMMs.r1_of_sub_r0_swapped₀ (amms : AMMs) (t0 t1 : T) (h : amms.init t0 t1) (x : ℝ>0) (h' : x < amms.r0 t1 t0 ⋯) :

(amms.sub_r0 t1 t0 ⋯ x h').r1₀ t0 t1 = amms.r1₀ t0 t1 - ↑x

source

theorem AMMs.eq_iff (amms amms' : AMMs) :

amms = amms' ↔ ∀ (t0 t1 : T), amms.r0₀ t0 t1 = amms'.r0₀ t0 t1