Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.fcast-readings

Lemmas behind operations-research checks src/rainbow/math/lemmas/fcast_readings.clj0 definitions, 4 theorems

General lemmas: fcast readings. The mathematical facts the corresponding checks rest on, each checked by the kernel.

signed/abs-pair-cases

TheoremFor all inputsNo axiomsSource

signed/abs-pair-cases :
  (ab-v : ℚ)
  → proposition/conjunction (proposition/disjunction (data/Bool.rec (fun x₁₃₂ => ℚ) 0 ab-v (signed/decide-at-most 0 ab-v) + data/Bool.rec (fun x₁₃₆ => ℚ) 0 (signed/negate ab-v) (most) = ab-v) (data/Bool.rec (fun x₁₄₀ => ℚ) 0 ab-v (signed/decide-at-most 0 ab-v) + data/Bool.rec (fun x₁₄₄ => ℚ) 0 (signed/negate ab-v) (most) = signed/negate ab-v)) (proposition/conjunction (0 ≤ data/Bool.rec (fun x₁₈₈ => ℚ) 0 ab-v (signed/decide-at-most 0 ab-v) + data/Bool.rec (fun x₁₉₂ => ℚ) 0 (signed/negate ab-v) (most)) (proposition/conjunction (ab-v ≤ data/Bool.rec (fun x₂₁₂ => ℚ) 0 ab-v (signed/decide-at-most 0 ab-v) + data/Bool.rec (fun x₂₁₆ => ℚ) 0 (signed/negate ab-v) (most)) (signed/negate ab-v ≤ data/Bool.rec (fun x₂₂₀ => ℚ) 0 ab-v (signed/decide-at-most 0 ab-v) + data/Bool.rec (fun x₂₂₄ => ℚ) 0 (signed/negate ab-v) (most))))
  where most := signed/decide-at-most 0 (signed/negate ab-v)

+ = signed/add0 = signed/zero= = signed/equivalent: equality of rational valuesℚ = signed/SignedRational≤ = signed/at-most

signed/square-difference-expand

TheoremFor all inputsNo axiomsSource

signed/square-difference-expand :
  (sd-e sd-m : ℚ)
  → (sd-e + signed/negate sd-m) · (sd-e + signed/negate sd-m) = sd-e · sd-e + (sd-m · sd-m + signed/negate ((sd-m + sd-m) · sd-e))

+ = signed/add= = signed/equivalent: equality of rational values· = signed/multiplyℚ = signed/SignedRational

signed/forecast-bias-bound

TheoremFor all inputsNo axiomsSource

signed/forecast-bias-bound :
  (fb-f : ℕ → ℚ) (fb-j : ℕ) (fb-me fb-mae : ℚ)
  (fb-hme : signed/from-nnrat (nnrat/make (data/succ fb-j) 0) · fb-me = signed/expr-sum-value fb-f (data/succ fb-j))
  (fb-hmae : signed/from-nnrat (nnrat/make (data/succ fb-j) 0) · fb-mae = signed/expr-sum-value (fun fw-t => data/Bool.rec (fun x₆ => ℚ) 0 (fb-f fw-t) (signed/decide-at-most 0 (fb-f fw-t)) + data/Bool.rec (fun x₈ => ℚ) 0 (signed/negate (fb-f fw-t)) (signed/decide-at-most 0 (signed/negate (fb-f fw-t)))) (data/succ fb-j))
  → proposition/conjunction (0 ≤ fb-mae) (conjunction)
  where conjunction := proposition/conjunction (fb-me ≤ fb-mae) (signed/negate fb-me ≤ fb-mae)

+ = signed/add0 = signed/zero= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most

signed/forecast-variance-split

TheoremFor all inputsNo axiomsSource

signed/forecast-variance-split :
  (fv-f : ℕ → ℚ) (fv-j : ℕ) (fv-me fv-mse : ℚ)
  (fv-hme : signed/from-nnrat (nnrat/make (data/succ fv-j) 0) · fv-me = signed/expr-sum-value fv-f (data/succ fv-j))
  (fv-hmse : signed/from-nnrat (nnrat/make (data/succ fv-j) 0) · fv-mse = signed/expr-sum-value (fun fs-t => fv-f fs-t · fv-f fs-t) (data/succ fv-j))
  → proposition/conjunction (signed/from-nnrat (nnrat/make (data/succ fv-j) 0) · fv-mse = fv-me · fv-me · signed/from-nnrat (nnrat/make (data/succ fv-j) 0) + value) (fv-me · fv-me ≤ fv-mse)
  where value := signed/expr-sum-value (fun fd-t => (fv-f fd-t + signed/negate fv-me) · (fv-f fd-t + signed/negate fv-me)) (data/succ fv-j)

+ = signed/add= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most