Documentation

Copula.OrdinalSum.Rescale

← Copula mathematical handbook

Coordinates for two-block ordinal sums #

The clipped inverse affine maps are defined even when a block has zero length. Its weight is then zero in the ordinal-sum CDF.

source
noncomputable def ProbabilityTheory.Copula.OrdinalSum.lowerCoord (a u : ↑unitInterval) :
↑unitInterval

Rescale the lower interval [0,a], clipping values above it.

Equations
Instances For
    source
    noncomputable def ProbabilityTheory.Copula.OrdinalSum.upperCoord (a u : ↑unitInterval) :
    ↑unitInterval

    Rescale the upper interval [a,1], clipping values below it.

    Equations
    Instances For
      source
      theorem ProbabilityTheory.Copula.OrdinalSum.lowerCoord_mono (a : ↑unitInterval) :
      Monotone (lowerCoord a)
      source
      theorem ProbabilityTheory.Copula.OrdinalSum.upperCoord_mono (a : ↑unitInterval) :
      Monotone (upperCoord a)
      source
      theorem ProbabilityTheory.Copula.OrdinalSum.continuous_lowerCoord (a : ↑unitInterval) :
      Continuous (lowerCoord a)
      source
      theorem ProbabilityTheory.Copula.OrdinalSum.continuous_upperCoord (a : ↑unitInterval) :
      Continuous (upperCoord a)
      source
      @[simp]
      theorem ProbabilityTheory.Copula.OrdinalSum.lowerCoord_zero (a : ↑unitInterval) :
      lowerCoord a 0 = 0
      source
      @[simp]
      theorem ProbabilityTheory.Copula.OrdinalSum.upperCoord_of_le (a u : ↑unitInterval) (hu : u ≤ a) :
      upperCoord a u = 0
      source
      @[simp]
      theorem ProbabilityTheory.Copula.OrdinalSum.upperCoord_zero (a : ↑unitInterval) :
      upperCoord a 0 = 0
      source
      theorem ProbabilityTheory.Copula.OrdinalSum.lowerCoord_of_ge (a u : ↑unitInterval) (ha : 0 < a) (hu : a ≤ u) :
      lowerCoord a u = 1
      source
      theorem ProbabilityTheory.Copula.OrdinalSum.coe_lowerCoord_of_le (a u : ↑unitInterval) (ha : 0 < a) (hu : u ≤ a) :
      ↑(lowerCoord a u) = ↑u / ↑a
      source
      theorem ProbabilityTheory.Copula.OrdinalSum.coe_upperCoord_of_ge (a u : ↑unitInterval) (ha : a < 1) (hu : a ≤ u) :
      ↑(upperCoord a u) = (↑u - ↑a) / (1 - ↑a)
      source
      @[simp]
      theorem ProbabilityTheory.Copula.OrdinalSum.lowerCoord_zero_left (u : ↑unitInterval) :
      lowerCoord 0 u = 0
      source
      @[simp]
      theorem ProbabilityTheory.Copula.OrdinalSum.upperCoord_one_left (u : ↑unitInterval) :
      upperCoord 1 u = 0
      source
      @[simp]
      theorem ProbabilityTheory.Copula.OrdinalSum.lowerCoord_one_left (u : ↑unitInterval) :
      lowerCoord 1 u = u
      source
      @[simp]
      theorem ProbabilityTheory.Copula.OrdinalSum.upperCoord_zero_left (u : ↑unitInterval) :
      upperCoord 0 u = u
      source
      theorem ProbabilityTheory.Copula.OrdinalSum.lowerCoord_one (a : ↑unitInterval) (ha : 0 < a) :
      lowerCoord a 1 = 1
      source
      theorem ProbabilityTheory.Copula.OrdinalSum.upperCoord_one (a : ↑unitInterval) (ha : a < 1) :
      upperCoord a 1 = 1
      source
      theorem ProbabilityTheory.Copula.OrdinalSum.weight_lowerCoord (a u : ↑unitInterval) :
      ↑a * ↑(lowerCoord a u) = min ↑a ↑u
      source
      theorem ProbabilityTheory.Copula.OrdinalSum.weight_upperCoord (a u : ↑unitInterval) :
      (1 - ↑a) * ↑(upperCoord a u) = max 0 (↑u - ↑a)
      source
      theorem ProbabilityTheory.Copula.OrdinalSum.weighted_coords (a u : ↑unitInterval) :
      ↑a * ↑(lowerCoord a u) + (1 - ↑a) * ↑(upperCoord a u) = ↑u
      source
      def ProbabilityTheory.Copula.OrdinalSum.lowerEmbed (a u : ↑unitInterval) :
      ↑unitInterval

      Embed a unit coordinate into the lower interval.

      Equations
      Instances For
        source
        def ProbabilityTheory.Copula.OrdinalSum.upperEmbed (a u : ↑unitInterval) :
        ↑unitInterval

        Embed a unit coordinate into the upper interval.

        Equations
        Instances For
          source
          theorem ProbabilityTheory.Copula.OrdinalSum.lowerEmbed_le (a u : ↑unitInterval) :
          lowerEmbed a u ≤ a
          source
          theorem ProbabilityTheory.Copula.OrdinalSum.le_upperEmbed (a u : ↑unitInterval) :
          a ≤ upperEmbed a u
          source
          theorem ProbabilityTheory.Copula.OrdinalSum.lowerCoord_lowerEmbed (a u : ↑unitInterval) (ha : 0 < a) :
          lowerCoord a (lowerEmbed a u) = u
          source
          theorem ProbabilityTheory.Copula.OrdinalSum.upperCoord_upperEmbed (a u : ↑unitInterval) (ha : a < 1) :
          upperCoord a (upperEmbed a u) = u