Documentation

Verification.FootruleParameter

← Mathematical handbook

Monotonicity and the admissible inverse parameter #

source
theorem Verification.hasDerivAt_footruleClosed (r : ℝ) (hr : r ≠ 0) :
HasDerivAt footruleClosed ((2 * r - 1) * (-2 * r ^ 2 + 2 * r + 1) / r ^ 2) r
source
theorem Verification.hasDerivAt_xiClosed (r : ℝ) (hr : r ≠ 0) :
HasDerivAt xiClosed (-2 * (1 - r) * (2 * r - 1) * (-2 * r ^ 2 + 2 * r + 1) / r ^ 3) r
source
theorem Verification.continuousOn_footruleClosed :
ContinuousOn footruleClosed (Set.Icc (1 / 2) 1)
source
theorem Verification.continuousOn_xiClosed :
ContinuousOn xiClosed (Set.Icc (1 / 2) 1)
source
theorem Verification.strictMonoOn_footruleClosed :
StrictMonoOn footruleClosed (Set.Icc (1 / 2) 1)
source
theorem Verification.strictAntiOn_xiClosed :
StrictAntiOn xiClosed (Set.Icc (1 / 2) 1)
source
theorem Verification.continuousOn_relaxedParameter :
ContinuousOn relaxedParameter (Set.Icc 0 2)
source
theorem Verification.strictAntiOn_relaxedParameter :
StrictAntiOn relaxedParameter (Set.Icc 0 2)
source
theorem Verification.continuousOn_relaxedFootrule :
ContinuousOn relaxedFootrule (Set.Icc 0 2)
source
theorem Verification.continuousOn_relaxedXi :
ContinuousOn relaxedXi (Set.Icc 0 2)
source
theorem Verification.strictAntiOn_relaxedFootrule :
StrictAntiOn relaxedFootrule (Set.Icc 0 2)
source
theorem Verification.strictMonoOn_relaxedXi :
StrictMonoOn relaxedXi (Set.Icc 0 2)
source
theorem Verification.relaxed_endpoints :
relaxedFootrule 0 = 0 ∧ relaxedFootrule 2 = -1 / 2 ∧ relaxedXi 0 = 0 ∧ relaxedXi 2 = 12 * Real.log 2 - 8
source
theorem Verification.existsUnique_relaxedParameter (y : ℝ) (hy : y ∈ Set.Icc (-1 / 2) 0) :
∃! μ : ℝ, μ ∈ Set.Icc 0 2 ∧ relaxedFootrule μ = y

The inverse is unique on the source's admissible interval, not on all of R.

source
def Verification.footruleCubic (y μ : ℝ) :
ℝ
Equations
Instances For
    source
    theorem Verification.relaxedFootrule_eq_iff_cubic (y μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) :
    relaxedFootrule μ = y ↔ footruleCubic y μ = 0

    The cubic and the prescribed footrule equation are equivalent on [0,2].

    source
    theorem Verification.existsUnique_footruleCubic (y : ℝ) (hy : y ∈ Set.Icc (-1 / 2) 0) :
    ∃! μ : ℝ, μ ∈ Set.Icc 0 2 ∧ footruleCubic y μ = 0

    Theorem 3.3's cubic has exactly one admissible root for each nonpositive target footrule.

    source
    theorem Verification.footruleCubic_not_unique_real :
    footruleCubic (-1 / 2) 2 = 0 ∧ footruleCubic (-1 / 2) (-1) = 0 ∧ 2 ≠ -1

    Global uniqueness in R would be false: at y=-1/2 there are two distinct real roots.

    source
    theorem Verification.xi_footrule_closed_lower_bound (C : ProbabilityTheory.Copula 2) (μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) :
    μ * footruleClosed (relaxedParameter μ) + xiClosed (relaxedParameter μ) ≤ μ * C.spearmanFootrule + C.chatterjeeXi

    The universal lower estimate with both coefficients explicitly evaluated.

    source
    theorem Verification.xi_lower_bound_of_cubic (C : ProbabilityTheory.Copula 2) (y μ : ℝ) (hμ : μ ∈ Set.Icc 0 2) (hy : C.spearmanFootrule = y) (hroot : footruleCubic y μ = 0) :
    xiClosed (relaxedParameter μ) ≤ C.chatterjeeXi

    Explicit lower bound at the unique admissible cubic parameter.