Generic Format Properties #

Elementary closure properties of the Flocq-style generic format. These lemmas are independent of the standard FIX, FLX, and FLT families.

source

@[simp]

theorem TorchLean.Floats.neuralMagnitude_neg {β : NeuralRadix} (x : ℝ) :

neuralMagnitude β (-x) = neuralMagnitude β x

Magnitude is invariant under negation.

source

@[simp]

theorem TorchLean.Floats.neuralCexp_neg {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) :

neuralCexp β fexp (-x) = neuralCexp β fexp x

The canonical exponent is invariant under negation.

source

@[simp]

theorem TorchLean.Floats.neuralScaledMantissa_neg {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) :

neuralScaledMantissa β fexp (-x) = -neuralScaledMantissa β fexp x

Negation negates the canonical scaled mantissa.

source

@[simp]

theorem TorchLean.Floats.neural_generic_format_zero {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] :

neuralGenericFormat β fexp 0

Zero belongs to every valid generic format.

source

theorem TorchLean.Floats.neural_generic_format_neg {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) (hx : neuralGenericFormat β fexp x) :

neuralGenericFormat β fexp (-x)

Generic formats are closed under negation.

source

@[simp]

theorem TorchLean.Floats.neural_generic_format_neg_iff {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) :

neuralGenericFormat β fexp (-x) ↔ neuralGenericFormat β fexp x

A value is representable exactly when its negation is representable.

source

theorem TorchLean.Floats.neural_generic_format_abs_iff {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) :

neuralGenericFormat β fexp |x| ↔ neuralGenericFormat β fexp x

A value is representable exactly when its absolute value is representable.

source

theorem TorchLean.Floats.neural_generic_format_bpow {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (e : ℤ) (h : fexp (e + 1) ≤ e) :

neuralGenericFormat β fexp (neuralBpow β e)

A radix power is representable whenever its canonical exponent is no larger than its exponent.

source

theorem TorchLean.Floats.neural_generic_format_of_toReal_of_cexp_le {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (f : NeuralFloat β) (x : ℝ) (hxf : x = neuralToReal f) (he : neuralCexp β fexp x ≤ f.exponent) :

neuralGenericFormat β fexp x

A mantissa/exponent representation is generic when its stored exponent is at least the canonical exponent selected for its value.

source

theorem TorchLean.Floats.neuralCexp_lt_magnitude_of_pos_generic {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] {x : ℝ} (hx : 0 < x) (hfmt : neuralGenericFormat β fexp x) :

neuralCexp β fexp x < neuralMagnitude β x

A positive representable value uses a canonical exponent strictly below its magnitude.

source

theorem TorchLean.Floats.neural_fexp_succ_le_of_generic_bpow {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (e : ℤ) (hfmt : neuralGenericFormat β fexp (neuralBpow β e)) :

fexp (e + 1) ≤ e

Representability of a radix power forces its canonical exponent below that power.

source

theorem TorchLean.Floats.neural_fexp_le_of_generic_bpow {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (e : ℤ) (hfmt : neuralGenericFormat β fexp (neuralBpow β e)) :

fexp e ≤ e

If β^e is representable, the exponent selected for the bin below it is at most e.

source

theorem TorchLean.Floats.neural_generic_inclusion_mag {β : NeuralRadix} {fexp₁ fexp₂ : ℤ → ℤ} [NeuralValidExp fexp₁] [NeuralValidExp fexp₂] {x : ℝ} (hexp : x ≠ 0 → fexp₂ (neuralMagnitude β x) ≤ fexp₁ (neuralMagnitude β x)) (hx : neuralGenericFormat β fexp₁ x) :

neuralGenericFormat β fexp₂ x

A value representable with fexp₁ remains representable with fexp₂ when the second canonical exponent is no larger at that value's magnitude. The condition is local because representability of x only depends on the exponent selected at magnitude x.

source

theorem TorchLean.Floats.neural_generic_inclusion {β : NeuralRadix} {fexp₁ fexp₂ : ℤ → ℤ} [NeuralValidExp fexp₁] [NeuralValidExp fexp₂] (hexp : ∀ (e : ℤ), fexp₂ e ≤ fexp₁ e) {x : ℝ} (hx : neuralGenericFormat β fexp₁ x) :

neuralGenericFormat β fexp₂ x

Pointwise-smaller exponent selection defines a containing generic format.

source

theorem TorchLean.Floats.neural_generic_format_discrete {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) (m : ℤ) (hlower : ↑m * neuralBpow β (neuralCexp β fexp x) < x) (hupper : x < ↑(m + 1) * neuralBpow β (neuralCexp β fexp x)) :

¬neuralGenericFormat β fexp x

No generic-format value lies strictly between consecutive points on its canonical grid.

source

theorem TorchLean.Floats.neural_canonical_exists_of_generic {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] {x : ℝ} (hx : neuralGenericFormat β fexp x) :

∃ (f : NeuralFloat β), x = neuralToReal f ∧ NeuralCanonical β fexp f

Every generic-format value has a canonical mantissa/exponent representation.

source

theorem TorchLean.Floats.neural_generic_format_of_canonical {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (f : NeuralFloat β) (hf : NeuralCanonical β fexp f) :

neuralGenericFormat β fexp (neuralToReal f)

The real value of a canonical representation belongs to its generic format.

source

theorem TorchLean.Floats.neural_canonical_unique {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] {f g : NeuralFloat β} (hf : NeuralCanonical β fexp f) (hg : NeuralCanonical β fexp g) (hval : neuralToReal f = neuralToReal g) :

f = g

Canonical representations of the same real value are equal.

TorchLean API

NN.Floats.NeuralFloat.Format.Generic

Generic Format Properties #