Support of seeded random tensors

Each tensor coordinate uses the source generator's key and row-major index. Over the real numbers, uniform draws lie in [0, 1). Masks contain only zero and one, and their probability endpoints give constant masks. These are properties of the seeded Spec operations.

theorem Spec.Random.sampleNat_lt (key : UInt64) (linearIndex : ℕ) {denom : ℕ} (hdenom : 0 < denom) : sampleNat key linearIndex denom < denom

Reducing the generator word modulo a positive denominator gives a valid draw.

theorem Spec.Random.sampleUnit_nonneg (u denom : ℕ) : 0 ≤ sampleUnit u denom

Converting a natural draw to a real quotient gives a nonnegative value.

theorem Spec.Random.sampleUnit_lt_one {u denom : ℕ} (hu : u < denom) : sampleUnit u denom < 1

A valid draw is strictly below one when the quotient is evaluated in the reals.

theorem Spec.Random.keepBit_eq_zero_or_eq_one {α : Type} [Context α] (keepProb : α) (u denom : ℕ) : keepBit keepProb u denom = 0 ∨ keepBit keepProb u denom = 1

Every branch of the source keep decision returns either zero or one.

@[simp]

theorem Spec.Random.keepBit_zero (u denom : ℕ) : keepBit 0 u denom = 0

A zero keep probability drops every draw.

@[simp]

theorem Spec.Random.keepBit_one (u denom : ℕ) : keepBit 1 u denom = 1

A unit keep probability keeps every draw, including at the sampling boundary.

theorem Spec.Random.Internal.uniform_apply {α : Type} [TorchLean.Storage α] [Context α] (key : UInt64) {s : Shape} (offset : ℕ) (c : s.Coord) : TorchLean.Tensor.Internal.Rep.get (uniform key offset) c = sampleUnit (sampleNat key (offset + ↑c.linearize)) (2 ^ 32)

The uniform generator uses the offset plus the coordinate's row-major index.

theorem Spec.Random.Internal.mask_apply {α : Type} [TorchLean.Storage α] [Context α] (key : UInt64) (keepProb : α) {s : Shape} (offset : ℕ) (c : s.Coord) : TorchLean.Tensor.Internal.Rep.get (mask key keepProb offset) c = keepBit keepProb (sampleNat key (offset + ↑c.linearize)) (2 ^ 32)

The mask generator uses the offset plus the coordinate's row-major index.

theorem Spec.Random.uniform_apply {α : Type} [TorchLean.Storage α] [Context α] (key : UInt64) {s : Shape} (c : s.Coord) : TorchLean.Tensor.Internal.Rep.get (uniform key) c = sampleUnit (sampleNat key ↑c.linearize) (2 ^ 32)

A uniform tensor coordinate is the source draw at its row-major index.

theorem Spec.Random.uniform_mem_Ico (key : UInt64) {s : Shape} (c : s.Coord) : TorchLean.Tensor.Internal.Rep.get (uniform key) c ∈ Set.Ico 0 1

Every seeded real uniform coordinate belongs to the half-open unit interval.

theorem Spec.Random.mask_apply {α : Type} [TorchLean.Storage α] [Context α] (key : UInt64) (keepProb : α) {s : Shape} (c : s.Coord) : TorchLean.Tensor.Internal.Rep.get (mask key keepProb) c = keepBit keepProb (sampleNat key ↑c.linearize) (2 ^ 32)

A mask coordinate is the source keep decision at its row-major index.

theorem Spec.Random.mask_eq_zero_or_eq_one {α : Type} [TorchLean.Storage α] [Context α] (key : UInt64) (keepProb : α) {s : Shape} (c : s.Coord) : TorchLean.Tensor.Internal.Rep.get (mask key keepProb) c = 0 ∨ TorchLean.Tensor.Internal.Rep.get (mask key keepProb) c = 1

Every seeded mask coordinate is binary, for every keep probability.

theorem Spec.Random.mask_mem_Icc (key : UInt64) (keepProb : ℝ) {s : Shape} (c : s.Coord) : TorchLean.Tensor.Internal.Rep.get (mask key keepProb) c ∈ Set.Icc 0 1

Every seeded real mask coordinate lies in the closed unit interval.

@[simp]

theorem Spec.Random.mask_zero_apply (key : UInt64) {s : Shape} (c : s.Coord) : TorchLean.Tensor.Internal.Rep.get (mask key 0) c = 0

A seeded real mask at keep probability zero drops every coordinate.

@[simp]

theorem Spec.Random.mask_one_apply (key : UInt64) {s : Shape} (c : s.Coord) : TorchLean.Tensor.Internal.Rep.get (mask key 1) c = 1

A seeded real mask at keep probability one keeps every coordinate.