Bracketing a Real Value

Effective rounding algorithms refine an interval until its endpoints are adjacent representable values. A location records whether the input is the lower endpoint or, for an interior point, whether it lies below, at, or above the interval midpoint. This is the Lean counterpart of Flocq's Calc.Bracket location semantics.

inductive TorchLean.Floats.NeuralLocation : Type

Position of a real value relative to the lower endpoint and midpoint of a bracket.

• exact : NeuralLocation
• inexact (midpointOrder : Ordering) : NeuralLocation

@[implicit_reducible]

instance TorchLean.Floats.instDecidableEqNeuralLocation : DecidableEq NeuralLocation

def TorchLean.Floats.instDecidableEqNeuralLocation.decEq (x✝ x✝¹ : NeuralLocation) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance TorchLean.Floats.instReprNeuralLocation : Repr NeuralLocation

def TorchLean.Floats.instReprNeuralLocation.repr : NeuralLocation → ℕ → Std.Format

noncomputable def TorchLean.Floats.neuralInbetweenLocation (d u x : ℝ) : NeuralLocation

Compute the location of x in a bracket whose lower endpoint is d.

inductive TorchLean.Floats.NeuralInbetween (d u x : ℝ) : NeuralLocation → Prop

Semantic meaning of a bracket location.

• exact {d u x : ℝ} (hx : x = d) : NeuralInbetween d u x NeuralLocation.exact
• inexact {d u x : ℝ} (l : Ordering) (hx : d < x ∧ x < u) (hmid : cmp x ((d + u) / 2) = l) : NeuralInbetween d u x (NeuralLocation.inexact l)

theorem TorchLean.Floats.neuralInbetweenLocation_spec {d u x : ℝ} (_hdu : d < u) (hx : d ≤ x ∧ x < u) : NeuralInbetween d u x (neuralInbetweenLocation d u x)

The computed location satisfies the bracket semantics.

theorem TorchLean.Floats.neuralInbetween_unique {d u x : ℝ} {l l' : NeuralLocation} (hl : NeuralInbetween d u x l) (hl' : NeuralInbetween d u x l') : l = l'

A value has at most one semantic location in a fixed bracket.

theorem TorchLean.Floats.neuralInbetween_bounds {d u x : ℝ} {l : NeuralLocation} (hdu : d < u) (hl : NeuralInbetween d u x l) : d ≤ x ∧ x < u

Every semantic location places the input in the half-open bracket [d, u).

theorem TorchLean.Floats.neuralInbetween_strict_bounds {d u x : ℝ} {order : Ordering} (hl : NeuralInbetween d u x (NeuralLocation.inexact order)) : d < x ∧ x < u

An inexact location places the input strictly between the bracket endpoints.

theorem TorchLean.Floats.neuralInbetween_distance {d u x : ℝ} {order : Ordering} (hl : NeuralInbetween d u x (NeuralLocation.inexact order)) : cmp (x - d) (u - x) = order

Midpoint comparison is equivalent to comparing distances from the two endpoints.

theorem TorchLean.Floats.neuralInbetween_abs_distance {d u x : ℝ} {order : Ordering} (hl : NeuralInbetween d u x (NeuralLocation.inexact order)) : cmp |d - x| |u - x| = order

The midpoint order also compares the absolute distances to the endpoints.

theorem TorchLean.Floats.neuralInbetween_exists {d u : ℝ} (hdu : d < u) (location : NeuralLocation) : ∃ (x : ℝ), NeuralInbetween d u x location

Every location is realized by a point in every nondegenerate bracket.

theorem TorchLean.Floats.neuralOrderedSteps {start step : ℝ} (hstep : 0 < step) (k : ℤ) : start + ↑k * step < start + ↑(k + 1) * step

Consecutive points in a positive-step arithmetic progression are strictly ordered.

theorem TorchLean.Floats.neuralStepMidpoint (start step : ℝ) (steps : ℤ) : (start + (start + ↑steps * step)) / 2 = start + ↑steps / 2 * step

Midpoint of an arithmetic progression interval.

theorem TorchLean.Floats.neuralInbetween_step_interior {start step x : ℝ} {steps k : ℤ} {localLocation : NeuralLocation} {globalOrder : Ordering} (hstep : 0 < step) (_hsteps : 1 < steps) (hk : 0 < k ∧ k < steps) (hl : NeuralInbetween (start + ↑k * step) (start + ↑(k + 1) * step) x localLocation) (hmid : cmp x (start + ↑steps / 2 * step) = globalOrder) : NeuralInbetween start (start + ↑steps * step) x (NeuralLocation.inexact globalOrder)

Lift a location in an interior arithmetic-progression cell to the full interval. The caller supplies the comparison with the full midpoint; later refinement rules compute that comparison from the cell index and local location.

theorem TorchLean.Floats.neuralInbetween_step_low {start step x : ℝ} {steps k : ℤ} {localLocation : NeuralLocation} (hstep : 0 < step) (hsteps : 1 < steps) (hk : 0 < k) (hcell : 2 * k + 1 < steps) (hl : NeuralInbetween (start + ↑k * step) (start + ↑(k + 1) * step) x localLocation) : NeuralInbetween start (start + ↑steps * step) x (NeuralLocation.inexact Ordering.lt)

A subinterval strictly below the global midpoint has global location .lt.

theorem TorchLean.Floats.neuralInbetween_step_high {start step x : ℝ} {steps k : ℤ} {localLocation : NeuralLocation} (hstep : 0 < step) (hsteps : 1 < steps) (hcell : steps < 2 * k) (hk : k < steps) (hl : NeuralInbetween (start + ↑k * step) (start + ↑(k + 1) * step) x localLocation) : NeuralInbetween start (start + ↑steps * step) x (NeuralLocation.inexact Ordering.gt)

A subinterval strictly above the global midpoint has global location .gt.

theorem TorchLean.Floats.neuralInbetween_step_zero_exact {start step x : ℝ} {steps : ℤ} (hl : NeuralInbetween start (start + step) x NeuralLocation.exact) : NeuralInbetween start (start + ↑steps * step) x NeuralLocation.exact

Exactness at the first cell's lower endpoint remains exact in the full interval.

theorem TorchLean.Floats.neuralInbetween_step_zero_inexact {start step x : ℝ} {steps : ℤ} {order : Ordering} (hstep : 0 < step) (hsteps : 1 < steps) (hl : NeuralInbetween start (start + step) x (NeuralLocation.inexact order)) : NeuralInbetween start (start + ↑steps * step) x (NeuralLocation.inexact Ordering.lt)

An inexact point in the first cell lies below the full midpoint when there are several cells.

theorem TorchLean.Floats.neuralInbetween_step_middle_even_exact {start step x : ℝ} {steps k : ℤ} (hstep : 0 < step) (hsteps : 1 < steps) (hmiddle : 2 * k = steps) (hl : NeuralInbetween (start + ↑k * step) (start + ↑(k + 1) * step) x NeuralLocation.exact) : NeuralInbetween start (start + ↑steps * step) x (NeuralLocation.inexact Ordering.eq)

At the central lower endpoint of an even subdivision, the global location is midpoint exact.

theorem TorchLean.Floats.neuralInbetween_step_middle_even_inexact {start step x : ℝ} {steps k : ℤ} {order : Ordering} (hstep : 0 < step) (hsteps : 1 < steps) (hmiddle : 2 * k = steps) (hl : NeuralInbetween (start + ↑k * step) (start + ↑(k + 1) * step) x (NeuralLocation.inexact order)) : NeuralInbetween start (start + ↑steps * step) x (NeuralLocation.inexact Ordering.gt)

An inexact point in the central cell of an even subdivision is above the global midpoint.

theorem TorchLean.Floats.neuralInbetween_step_middle_odd_exact {start step x : ℝ} {steps k : ℤ} (hstep : 0 < step) (hsteps : 1 < steps) (hmiddle : 2 * k + 1 = steps) (hl : NeuralInbetween (start + ↑k * step) (start + ↑(k + 1) * step) x NeuralLocation.exact) : NeuralInbetween start (start + ↑steps * step) x (NeuralLocation.inexact Ordering.lt)

At the lower endpoint of the central cell of an odd subdivision, the global location is low.

theorem TorchLean.Floats.neuralInbetween_step_middle_odd_inexact {start step x : ℝ} {steps k : ℤ} {order : Ordering} (hstep : 0 < step) (hsteps : 1 < steps) (hmiddle : 2 * k + 1 = steps) (hl : NeuralInbetween (start + ↑k * step) (start + ↑(k + 1) * step) x (NeuralLocation.inexact order)) : NeuralInbetween start (start + ↑steps * step) x (NeuralLocation.inexact order)

In the central cell of an odd subdivision, local and global midpoint locations agree.

def TorchLean.Floats.neuralRefineLocationEven (steps k : ℤ) (location : NeuralLocation) : NeuralLocation

Refine a local location when the enclosing subdivision count is even.

def TorchLean.Floats.neuralRefineLocationOdd (steps k : ℤ) (location : NeuralLocation) : NeuralLocation

Refine a local location when the enclosing subdivision count is odd.

theorem TorchLean.Floats.neuralRefineLocationEven_correct {start step x : ℝ} {steps k : ℤ} {location : NeuralLocation} (hstep : 0 < step) (hsteps : 1 < steps) (heven : Even steps) (hk : 0 ≤ k ∧ k < steps) (hl : NeuralInbetween (start + ↑k * step) (start + ↑(k + 1) * step) x location) : NeuralInbetween start (start + ↑steps * step) x (neuralRefineLocationEven steps k location)

Correctness of location refinement for an even number of cells.

theorem TorchLean.Floats.neuralRefineLocationOdd_correct {start step x : ℝ} {steps k : ℤ} {location : NeuralLocation} (hstep : 0 < step) (hsteps : 1 < steps) (hodd : Odd steps) (hk : 0 ≤ k ∧ k < steps) (hl : NeuralInbetween (start + ↑k * step) (start + ↑(k + 1) * step) x location) : NeuralInbetween start (start + ↑steps * step) x (neuralRefineLocationOdd steps k location)

Correctness of location refinement for an odd number of cells.

noncomputable def TorchLean.Floats.neuralRefineLocation (steps k : ℤ) (location : NeuralLocation) : NeuralLocation

Refine a local location, selecting the even or odd subdivision rule automatically.

theorem TorchLean.Floats.neuralRefineLocation_correct {start step x : ℝ} {steps k : ℤ} {location : NeuralLocation} (hstep : 0 < step) (hsteps : 1 < steps) (hk : 0 ≤ k ∧ k < steps) (hl : NeuralInbetween (start + ↑k * step) (start + ↑(k + 1) * step) x location) : NeuralInbetween start (start + ↑steps * step) x (neuralRefineLocation steps k location)

Correctness of automatic local-to-global location refinement.