Documentation

Copula.Rank.Region.RhoFootrule.UpperSpline

← Mathematical handbook

Algebraic certificates for the rho–footrule transport spline #

The four pieces of the periodic potential in Ansari–Rockel, Definition 5.1, are parametrized by their interval coordinates. Nonnegative square certificates prove the dual inequality on one period.

source
noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.period (n v w : ℝ) :
ℝ
Equations
Instances For
    source
    noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.offset (n v w : ℝ) :
    ℝ
    Equations
    Instances For
      source
      noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.piecePoint (n v w : ℝ) :
      Fin 4 → ℝ → ℝ
      Equations
      Instances For
        source
        noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.pieceValue (n v w : ℝ) :
        Fin 4 → ℝ → ℝ
        Equations
        Instances For
          source
          theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.ordered_piece_cost_le {n v w s t : ℝ} (hn : 0 ≤ n) (hv : 0 ≤ v) (hw : 0 ≤ w) (hs : s ∈ Set.Icc 0 1) (ht : t ∈ Set.Icc 0 1) (i j : Fin 4) (hij : i ≤ j) :
          pieceValue n v w i s + pieceValue n v w j t ≤ (piecePoint n v w j t - piecePoint n v w i s) ^ 2 - period n v w * (piecePoint n v w j t - piecePoint n v w i s)
          source
          theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.piecePoint_mem {n v w : ℝ} (hn : 0 ≤ n) (hv : 0 ≤ v) (hw : 0 ≤ w) (i : Fin 4) (s : ↑unitInterval) :
          piecePoint n v w i 0 ≤ piecePoint n v w i ↑s ∧ piecePoint n v w i ↑s ≤ piecePoint n v w i 1
          source
          theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.piecePoint_order {n v w : ℝ} (hn : 0 ≤ n) (hv : 0 ≤ v) (hw : 0 ≤ w) (i j : Fin 4) (hij : i < j) (s t : ↑unitInterval) :
          piecePoint n v w i ↑s ≤ piecePoint n v w j ↑t
          source
          theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.piece_cost_le {n v w : ℝ} (hn : 0 ≤ n) (hv : 0 ≤ v) (hw : 0 ≤ w) (i j : Fin 4) (s t : ↑unitInterval) :
          pieceValue n v w i ↑s + pieceValue n v w j ↑t ≤ (piecePoint n v w j ↑t - piecePoint n v w i ↑s) ^ 2 - period n v w * |piecePoint n v w j ↑t - piecePoint n v w i ↑s|
          source
          noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.basePotential (n v w x : ℝ) :
          ℝ

          A continuous hinge-square formula for one period of the dual potential.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.continuous_basePotential (n v w : ℝ) :
            Continuous (basePotential n v w)
            source
            theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.basePotential_piecePoint {n v w : ℝ} (hn : 0 < n) (hv : 0 ≤ v) (hw : 0 ≤ w) (i : Fin 4) (s : ↑unitInterval) :
            basePotential n v w (piecePoint n v w i ↑s) = pieceValue n v w i ↑s
            source
            theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.exists_piecePoint {n v w x : ℝ} (hx : x ∈ Set.Icc 0 (period n v w)) :
            ∃ (i : Fin 4) (s : ↑unitInterval), piecePoint n v w i ↑s = x
            source
            theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.basePotential_feasible {n v w x y : ℝ} (hn : 0 < n) (hv : 0 ≤ v) (hw : 0 ≤ w) (hx : x ∈ Set.Icc 0 (period n v w)) (hy : y ∈ Set.Icc 0 (period n v w)) :
            basePotential n v w x + basePotential n v w y ≤ (y - x) ^ 2 - period n v w * |y - x|
            source
            theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.basePotential_endpoints {n v w : ℝ} (hn : 0 < n) (hv : 0 ≤ v) (hw : 0 ≤ w) :
            basePotential n v w 0 = basePotential n v w (period n v w)
            source
            theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.quadratic_translate_le {p d : ℝ} (hp : 0 < p) (hd0 : 0 ≤ d) (hd1 : d ≤ p) (k : ℤ) :
            d ^ 2 - p * d ≤ (d + ↑k * p) ^ 2 - p * |d + ↑k * p|

            Integer translations can only increase the distance cost from its fundamental cell.

            source
            noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.potential (n v w : ℝ) (hp : 0 < period n v w) (x : ℝ) :
            ℝ

            The potential extended periodically to the real line.

            Equations
            Instances For
              source
              theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.potential_periodic (n v w : ℝ) (hp : 0 < period n v w) :
              Function.Periodic (potential n v w hp) (period n v w)
              source
              theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.continuous_potential {n v w : ℝ} (hn : 0 < n) (hv : 0 ≤ v) (hw : 0 ≤ w) (hp : 0 < period n v w) :
              Continuous (potential n v w hp)
              source
              theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.potential_eq_base {n v w x : ℝ} (hp : 0 < period n v w) (hx : x ∈ Set.Ico 0 (period n v w)) :
              potential n v w hp x = basePotential n v w x
              source
              theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperSpline.potential_feasible {n v w : ℝ} (hn : 0 < n) (hv : 0 ≤ v) (hw : 0 ≤ w) (hp : 0 < period n v w) (x y : ℝ) :
              potential n v w hp x + potential n v w hp y ≤ (y - x) ^ 2 - period n v w * |y - x|

              The source's global dual inequality, including pairs in different periods.