Documentation

Papers.Rockel2026XiFootrule.CountableOrdinalTail

← Mathematical handbook
source
noncomputable def Papers.Rockel2026XiFootrule.countableTailPartition (P : ProbabilityTheory.Copula.CountableIntervalPartition) :
ProbabilityTheory.Copula.CountableIntervalPartition
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Papers.Rockel2026XiFootrule.countablePi_upper_component_tail (P : ProbabilityTheory.Copula.CountableIntervalPartition) :
    (ProbabilityTheory.Copula.countableOrdinalSumPi P).upperOrdinalComponent (P.point 1) ⋯ ⋯ = ProbabilityTheory.Copula.countableOrdinalSumPi (countableTailPartition P)
    source
    theorem Papers.Rockel2026XiFootrule.countablePi_recursive (P : ProbabilityTheory.Copula.CountableIntervalPartition) :
    ProbabilityTheory.Copula.countableOrdinalSumPi P = (ProbabilityTheory.Copula.independence 2).ordinalSum (ProbabilityTheory.Copula.countableOrdinalSumPi (countableTailPartition P)) (P.point 1)
    source
    theorem Papers.Rockel2026XiFootrule.countablePi_gap_recursive (P : ProbabilityTheory.Copula.CountableIntervalPartition) :
    (ProbabilityTheory.Copula.countableOrdinalSumPi P).chatterjeeXi - (ProbabilityTheory.Copula.countableOrdinalSumPi P).spearmanFootrule = (1 - ↑(P.point 1)) ^ 2 * ((ProbabilityTheory.Copula.countableOrdinalSumPi (countableTailPartition P)).chatterjeeXi - (ProbabilityTheory.Copula.countableOrdinalSumPi (countableTailPartition P)).spearmanFootrule)
    source
    noncomputable def Papers.Rockel2026XiFootrule.tailIter (P : ProbabilityTheory.Copula.CountableIntervalPartition) :
    ℕ → ProbabilityTheory.Copula.CountableIntervalPartition
    Equations
    Instances For
      source
      theorem Papers.Rockel2026XiFootrule.countablePi_xi_eq_footrule (P : ProbabilityTheory.Copula.CountableIntervalPartition) :
      (ProbabilityTheory.Copula.countableOrdinalSumPi P).chatterjeeXi = (ProbabilityTheory.Copula.countableOrdinalSumPi P).spearmanFootrule
      source
      theorem Papers.Rockel2026XiFootrule.countablePi_isSI (P : ProbabilityTheory.Copula.CountableIntervalPartition) :
      (ProbabilityTheory.Copula.countableOrdinalSumPi P).IsSI

      Adjacent countable independence-block sums are stochastically increasing.