← Mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.continuous_gammaValue {X : Type u_1} [TopologicalSpace X] {s c m : X → ℝ} (hs : Continuous s) (hc : Continuous c) (hm : Continuous m) (hpos : ∀ (x : X), 0 < s x) : Continuous fun (x : X) => gammaValue (s x) (c x) (m x)

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoGamma.contactGamma (N : ℕ) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoGamma.contactGamma N = ProbabilityTheory.Copula.RankRegion.RhoGamma.gammaValue (1 / ↑N) (-(1 / (8 * ↑N ^ 2))) (1 / (2 * ↑N))

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.left_zero (N : ℕ) (hN : 0 < N) : (UpperParameter.left (RhoFootrule.leftFamily N hN 0)).gamma = contactGamma N

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.right_zero (N : ℕ) (hN : 0 < N) : (UpperParameter.right (RhoFootrule.rightFamily N hN 0)).gamma = contactGamma (N + 1)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.middle_join (N : ℕ) (hN : 0 < N) : (UpperParameter.left (RhoFootrule.leftFamily N hN 1)).gamma = (UpperParameter.right (RhoFootrule.rightFamily N hN 1)).gamma

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.continuous_right_gamma (N : ℕ) (hN : 0 < N) : Continuous fun (u : ↑unitInterval) => (UpperParameter.right (RhoFootrule.rightFamily N hN u)).gamma

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.continuous_left_gamma (N : ℕ) (hN : 0 < N) : Continuous fun (u : ↑unitInterval) => (UpperParameter.left (RhoFootrule.leftFamily N hN u)).gamma

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.between_contacts {g : ℝ} (N : ℕ) (hN : 0 < N) (hlo : contactGamma N ≤ g) (hhi : g ≤ contactGamma (N + 1)) : ∃ (p : UpperParameter), p.gamma = g

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.cornerLength_le_two_div {s : ℝ} (hs : 0 < s) (c : ℝ) : cornerLength s c ≤ 2 / s

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShift_near_endpoint {s : ℝ} (hs : 1 ≤ s) : gammaValue s (3 / 8 - s / 2) (1 / 2) ≤ -1 + 8 / s

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.halfShift_join : gammaValue 1 (3 / 8 - 1 / 2) (1 / 2) = contactGamma 1

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.below_first_contact {g : ℝ} (hg : -1 < g) (hg1 : g ≤ contactGamma 1) : ∃ (p : UpperParameter), p.gamma = g

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.contactGamma_tendsto : Filter.Tendsto contactGamma Filter.atTop (nhds 1)

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.through_contacts (N : ℕ) (hN : 0 < N) {g : ℝ} (hg : -1 < g) (hhi : g ≤ contactGamma N) : ∃ (p : UpperParameter), p.gamma = g

theorem ProbabilityTheory.Copula.RankRegion.RhoGamma.upperParameter_exists {g : ℝ} (hg : g ∈ Set.Icc (-1) 1) : ∃ (p : UpperParameter), p.gamma = g