Documentation

Papers.AnsariRockel2026RhoFootrule.EarlierCurve

← Mathematical handbook
source
theorem Papers.AnsariRockel2026RhoFootrule.upperRho_concave :
ConcaveOn ℝ (Set.Icc (-1 / 2) 1) upperRho

The attained upper rho boundary is concave in footrule.

source
noncomputable def Papers.AnsariRockel2026RhoFootrule.oldContact (N : ℕ) :
ℝ
Equations
Instances For
    source
    noncomputable def Papers.AnsariRockel2026RhoFootrule.oldCorner (N : ℕ) :
    ℝ
    Equations
    Instances For
      source
      noncomputable def Papers.AnsariRockel2026RhoFootrule.oldCornerRho (N : ℕ) :
      ℝ
      Equations
      Instances For
        source
        noncomputable def Papers.AnsariRockel2026RhoFootrule.oldContactRho (N : ℕ) :
        ℝ
        Equations
        Instances For
          source
          noncomputable def Papers.AnsariRockel2026RhoFootrule.oldLeftLine (N : ℕ) (x : ℝ) :
          ℝ
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def Papers.AnsariRockel2026RhoFootrule.oldRightLine (N : ℕ) (x : ℝ) :
            ℝ
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Papers.AnsariRockel2026RhoFootrule.upperRho_oldContact (N : ℕ) (hN : 0 < N) :
              upperRho (oldContact N) = oldContactRho N
              source
              noncomputable def Papers.AnsariRockel2026RhoFootrule.oldCornerV (N : ℕ) :
              ℝ
              Equations
              Instances For
                source
                theorem Papers.AnsariRockel2026RhoFootrule.oldCornerV_bounds (N : ℕ) (hN : 0 < N) :
                0 ≤ oldCornerV N ∧ (↑N + 1) * oldCornerV N ≤ 1 / (2 * ↑N)
                source
                theorem Papers.AnsariRockel2026RhoFootrule.oldCornerV_sq (N : ℕ) (hN : 0 < N) :
                oldCornerV N ^ 2 = 1 / (2 * ↑N ^ 2 * (↑N + 1) ^ 3)
                source
                noncomputable def Papers.AnsariRockel2026RhoFootrule.oldCornerData (N : ℕ) (hN : 0 < N) :
                ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem Papers.AnsariRockel2026RhoFootrule.oldCornerData_footrule (N : ℕ) (hN : 0 < N) :
                  (ProbabilityTheory.Copula.RankRegion.RhoFootrule.UpperParameter.left (oldCornerData N hN)).footrule = oldCorner N
                  source
                  theorem Papers.AnsariRockel2026RhoFootrule.upperRho_oldCorner (N : ℕ) (hN : 0 < N) :
                  upperRho (oldCorner N) = oldCornerRho N + (1 - 2 * ↑N * (↑N + 1) * oldCornerV N) / (↑N ^ 2 * (↑N + 1) ^ 3)
                  source
                  theorem Papers.AnsariRockel2026RhoFootrule.oldCorner_strict_gap (N : ℕ) (hN : 2 ≤ N) :
                  oldCornerRho N < upperRho (oldCorner N)
                  source
                  theorem Papers.AnsariRockel2026RhoFootrule.oldCorner_order (N : ℕ) (hN : 0 < N) :
                  oldContact N < oldCorner N ∧ oldCorner N < oldContact (N + 1)
                  source
                  theorem Papers.AnsariRockel2026RhoFootrule.oldContact_mem (N : ℕ) (hN : 0 < N) :
                  oldContact N ∈ Set.Icc (-1 / 2) 1
                  source
                  theorem Papers.AnsariRockel2026RhoFootrule.oldCorner_mem (N : ℕ) (hN : 0 < N) :
                  oldCorner N ∈ Set.Icc (-1 / 2) 1
                  source
                  theorem Papers.AnsariRockel2026RhoFootrule.earlier_left_strict (N : ℕ) (hN : 2 ≤ N) (x : ℝ) (hx : x ∈ Set.Ioc (oldContact N) (oldCorner N)) :
                  oldLeftLine N x < upperRho x

                  Strict improvement on the first linear segment of every later contact interval.

                  source
                  theorem Papers.AnsariRockel2026RhoFootrule.earlier_right_strict (N : ℕ) (hN : 2 ≤ N) (x : ℝ) (hx : x ∈ Set.Ico (oldCorner N) (oldContact (N + 1))) :
                  oldRightLine N x < upperRho x

                  Strict improvement on the second linear segment of every later contact interval.

                  source
                  theorem Papers.AnsariRockel2026RhoFootrule.earlier_first_radical (x : ℝ) (hx : x ∈ Set.Icc (-1 / 2) (-1 / 8)) :
                  upperRho x = 2 * x + 1 / 2 - √3 / 9 * √(1 + 2 * x) ^ 3

                  First radical branch of the earlier curve, including both endpoints.

                  source
                  theorem Papers.AnsariRockel2026RhoFootrule.earlier_second_radical (x : ℝ) (hx : x ∈ Set.Icc (-1 / 8) (1 / 4)) :
                  upperRho x = x + 3 / 8 - √6 / 36 * √(1 - 4 * x) ^ 3

                  Second radical branch of the earlier curve, also sharp on the whole closed interval.

                  source
                  theorem Papers.AnsariRockel2026RhoFootrule.earlier_endpoint :
                  upperRho 1 = 1
                  source
                  theorem Papers.AnsariRockel2026RhoFootrule.oldContactRho_eq_quadratic (N : ℕ) (hN : 0 < N) :
                  oldContactRho N = 1 - 2 / 3 * (1 - oldContact N) ^ 2
                  source
                  theorem Papers.AnsariRockel2026RhoFootrule.earlier_contact (N : ℕ) (hN : 2 ≤ N) :
                  upperRho (oldContact N) = oldLeftLine N (oldContact N)