OAI/Combinatorics/EditApproximation/Probability/FiniteKeyRestriction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Restricting independent finite key streams preserves their exact product law. Unused keys need not be allocated by a lazy implementation.

  1. theorem OAI.EditApproximation.finite_pi_restrict_map line 12
  2. theorem OAI.EditApproximation.finite_pi_restrict_image_map line 25
  3. theorem OAI.EditApproximation.finite_uniform_array_cast line 42
  4. theorem OAI.EditApproximation.finite_uniform_arrays_restrict_cast line 52

    Source documentation

    The accepted finite sampler outputs can be keyed by a larger bounded universe. Restriction and the range equalities give the original independent time arrays exactly.

    theorem finite_uniform_arrays_restrict_cast {ι κ : Type*} [Fintype ι] [Fintype κ]
    (R : ℕ) (n : ι → ℕ) (m : κ → ℕ)
    [∀ i, NeZero (n i)] [∀ k, NeZero (m k)]
    (key : κ → ι) (hinjective : Function.Injective key)
    (hrange : ∀ k, n (key k) = m k) :
    (Measure.pi (fun i => Measure.pi (fun _ : Fin R =>
      (PMF.uniformOfFintype (Fin (n i))).toMeasure))).map
        (fun draw k t => Fin.cast (hrange k) (draw (key k) t)) =
      Measure.pi (fun k => Measure.pi (fun _ : Fin R =>
        (PMF.uniformOfFintype (Fin (m k))).toMeasure)) := by
…