SqrtInterval — Interval Square Root via exp(log/2) #
For positive intervals, √x = exp(log(x)/2). Computed by chaining
logInterval, rational halving, and expInterval.
Used by RExpr.rsqrt to support Real.sqrt in the rsa_predict tactic,
enabling Hellinger-distance-based RSA models (@cite{herbstritt-franke-2019}).
Interval square root for positive intervals.
Uses the identity √x = exp(log(x) / 2) for x > 0.
Chains logInterval, rational halving, and expInterval.
Equations
- Linglib.Interval.sqrtInterval a ha = Linglib.Interval.expInterval { lo := (Linglib.Interval.logInterval a ha).lo / 2, hi := (Linglib.Interval.logInterval a ha).hi / 2, valid := ⋯ }
Instances For
theorem
Linglib.Interval.sqrtInterval_containsReal
{a : QInterval}
{x : ℝ}
(ha : 0 < a.lo)
(hx : a.containsReal x)
:
(sqrtInterval a ha).containsReal √x
Soundness: if x ∈ [a.lo, a.hi] and a.lo > 0, then √x ∈ sqrtInterval a.