Documentation

Copula.Rank.Region.RhoTau.BoundaryFunction

← Copula mathematical handbook
source
@[reducible, inline]
abbrev ProbabilityTheory.Copula.RankRegion.RhoTau.CoefficientInterval :
Set ℝ
Equations
Instances For
    source
    noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.parameterAtTau (t : ↑CoefficientInterval) :
    LowerParameter
    Equations
    Instances For
      source
      theorem ProbabilityTheory.Copula.RankRegion.RhoTau.parameterAtTau_tau (t : ↑CoefficientInterval) :
      (parameterAtTau t).tau = ↑t
      source
      noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.boundaryMap (t : ↑CoefficientInterval) :
      ↑CoefficientInterval

      The SPT lower boundary, as an order isomorphism of the coefficient interval.

      Equations
      Instances For
        source
        theorem ProbabilityTheory.Copula.RankRegion.RhoTau.boundaryMap_parameter (p : LowerParameter) :
        ↑(boundaryMap ⟨p.tau, ⋯⟩) = p.rho
        source
        theorem ProbabilityTheory.Copula.RankRegion.RhoTau.boundaryMap_le_iff (s t : ↑CoefficientInterval) :
        boundaryMap s ≤ boundaryMap t ↔ s ≤ t
        source
        theorem ProbabilityTheory.Copula.RankRegion.RhoTau.boundaryMap_injective :
        Function.Injective boundaryMap
        source
        theorem ProbabilityTheory.Copula.RankRegion.RhoTau.boundaryMap_surjective :
        Function.Surjective boundaryMap
        source
        noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.boundaryOrderIso :
        ↑CoefficientInterval ≃o ↑CoefficientInterval
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem ProbabilityTheory.Copula.RankRegion.RhoTau.continuous_boundaryMap :
          Continuous boundaryMap
          source
          theorem ProbabilityTheory.Copula.RankRegion.RhoTau.boundaryMap_mono :
          Monotone boundaryMap