Documentation

LeanPool.ZhangYeungInequality.PFR.ForMathlib.Pair

LeanPool.ZhangYeungInequality.PFR.ForMathlib.Pair #

Imported Lean Pool material for LeanPool.ZhangYeungInequality.PFR.ForMathlib.Pair.

source
@[reducible, inline]
abbrev prod {Ω : Type u_1} {S : Type u_2} {T : Type u_3} (X : Ω → S) (Y : Ω → T) (ω : Ω) :
S × T

The pair of two random variables

Equations
Instances For
    source
    def ZhangYeungPFR.«term⟨_,_⟩» :
    Lean.ParserDescr

    The pair of two random variables

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem prod_eq {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {X : Ω → S} {Y : Ω → T} {ω : Ω} :
      prod X Y ω = (X ω, Y ω)