IsComputable instances for basic real operations

This file provides IsComputable instances for scientific literals, dite/ite, Real.sign, max, min, abs, conjugate exponents, and finite sums, closing the IsComputable typeclass under the basic operations on real numbers. The instances that branch on a comparison (Real.sign, max, min, abs) inherit its classical sign test and are noncomputable.

@[implicit_reducible]

instance IsComputable.instComputableOfScientific (m : ℕ) (b : Bool) (e : ℕ) : IsComputable (OfScientific.ofScientific m b e)

Equations

• IsComputable.instComputableOfScientific m b e = { seq := ↑(OfScientific.ofScientific m b e), prop := ⋯ }

@[implicit_reducible]

instance IsComputable.instComputableDite (p : Prop) (x : p → ℝ) (y : ¬p → ℝ) [Decidable p] [hx : (p : p) → IsComputable (x p)] [hy : (p : ¬p) → IsComputable (y p)] : IsComputable (dite p x y)

Equations

• IsComputable.instComputableDite p x y = if h : p then IsComputable.liftEq ⋯ (hx h) else IsComputable.liftEq ⋯ (hy h)

@[implicit_reducible, inline]

instance IsComputable.instComputableIte (p : Prop) (x y : ℝ) [Decidable p] [hx : IsComputable x] [hy : IsComputable y] : IsComputable (if p then x else y)

Equations

• IsComputable.instComputableIte p x y = IsComputable.instComputableDite p (fun (x_1 : p) => x) fun (x : ¬p) => y

@[implicit_reducible, inline]

noncomputable instance IsComputable.instComputableSign (x : ℝ) [hx : IsComputable x] : IsComputable x.sign

Equations

• IsComputable.instComputableSign x = { seq := ↑(IsComputable.seq x).sign, prop := ⋯ }

@[implicit_reducible]

noncomputable instance IsComputable.instComputableMax (x y : ℝ) [hx : IsComputable x] [hy : IsComputable y] : IsComputable (max x y)

Equations

• IsComputable.instComputableMax x y = IsComputable.liftEq ⋯ inferInstance

@[implicit_reducible]

noncomputable instance IsComputable.instComputableMin (x y : ℝ) [hx : IsComputable x] [hy : IsComputable y] : IsComputable (min x y)

Equations

• IsComputable.instComputableMin x y = IsComputable.liftEq ⋯ inferInstance

@[implicit_reducible]

noncomputable instance IsComputable.instComputableAbs (x : ℝ) [hx : IsComputable x] : IsComputable |x|

Equations

• IsComputable.instComputableAbs x = IsComputable.liftEq ⋯ inferInstance

@[implicit_reducible]

noncomputable instance IsComputable.instComputableConjExponent (x : ℝ) [hx : IsComputable x] : IsComputable x.conjExponent

Equations

• IsComputable.instComputableConjExponent x = IsComputable.liftEq ⋯ inferInstance

@[implicit_reducible]

instance IsComputable.instComputableFinsetSum {ι : Type u_1} (xs : ι → ℝ) (s : Finset ι) [hxs : (i : ι) → IsComputable (xs i)] : IsComputable (s.sum xs)

Equations

• IsComputable.instComputableFinsetSum xs s = { seq := Finset.fold (fun (x1 x2 : ComputableℝSeq) => x1 + x2) 0 (fun (i : ι) => IsComputable.seq (xs i)) s, prop := ⋯ }