LeanMachineLearning

1.10. ForMathlib.MeasureTheory.MeasurableSpace.Embedding🔗

From the authors

Measurable equivalences

Measurable equivalences between product and pi types, used to manipulate histories of sequential learning algorithms (elements of Fin n → 𝓐 × 𝓨 or Iic n → 𝓐 × 𝓨).

  • MeasurableEquiv.uniqueProd, MeasurableEquiv.prodUnique: drop a component that lives in a type with a unique element.

  • MeasurableEquiv.IicSuccProd: (Π i : Iic (n + 1), X i) ≃ᵐ (Π i : Iic n, X i) × X (n + 1).

  • MeasurableEquiv.finSuccPiIic: (Π i : Fin (n + 1), X i) ≃ᵐ (Π i : Iic n, X i).

  • MeasurableEquiv.finSuccProd: (Fin (n + 1) → X) ≃ᵐ (Fin n → X) × X.

Module LeanMachineLearning.ForMathlib.MeasureTheory.MeasurableSpace.Embedding contains 20 exposed declarations.