Documentation

Papers.AnsariRockel2026RhoFootrule.Mixability

← Mathematical handbook

Theorem 2.4: the generalized mixability optimization problem #

Every coupling of two centered uniforms is represented by shifting both uniform coordinates by -1/2. Reflection of the second coordinate identifies their absolute sum with the absolute displacement problem, preserving the entire probability law.

source
noncomputable def Papers.AnsariRockel2026RhoFootrule.centeredSumMean (C : ProbabilityTheory.Copula 2) :
ℝ
Equations
Instances For
    source
    noncomputable def Papers.AnsariRockel2026RhoFootrule.centeredSumVariance (C : ProbabilityTheory.Copula 2) :
    ℝ
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Papers.AnsariRockel2026RhoFootrule.centered_sum_law (C : ProbabilityTheory.Copula 2) (f : ℝ → ℝ) (hf : Continuous f) :
      ∫ (x : Fin 2 → ↑unitInterval), f |↑(x 0) - 1 / 2 + (↑(x 1) - 1 / 2)| ∂C.toMeasure = ∫ (x : Fin 2 → ↑unitInterval), f |↑(x 0) - ↑(x 1)| ∂(C.reflect {1}).toMeasure

      Reflection identifies the full law, hence every continuous test function, of the magnitudes.

      source
      theorem Papers.AnsariRockel2026RhoFootrule.centered_sum_statistics (C : ProbabilityTheory.Copula 2) :
      centeredSumMean C = meanDistance (C.reflect {1}) ∧ centeredSumVariance C = distanceVariance (C.reflect {1})

      Both optimization statistics are preserved by the reflection equivalence.

      source
      def Papers.AnsariRockel2026RhoFootrule.mixabilityVariances (m : ℝ) :
      Set ℝ

      Feasible variances in the source constrained optimization problem.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Papers.AnsariRockel2026RhoFootrule.mixability_minimum {m : ℝ} (hm : m ∈ Set.Icc 0 (1 / 2)) :
        IsLeast (mixabilityVariances m) (minimumVariance m)

        Theorem 2.4: the source infimum is attained and equals the exact correction.

        source
        theorem Papers.AnsariRockel2026RhoFootrule.mixability_infimum {m : ℝ} (hm : m ∈ Set.Icc 0 (1 / 2)) :
        sInf (mixabilityVariances m) = minimumVariance m

        The infimum notation in equation (33).

        source
        theorem Papers.AnsariRockel2026RhoFootrule.mixability_zero_iff {m : ℝ} (hm : m ∈ Set.Icc 0 (1 / 2)) :
        sInf (mixabilityVariances m) = 0 ↔ m = 0 ∨ ∃ (N : ℕ), 0 < N ∧ m = 1 / (2 * ↑N)

        Exactly the source set of generalized complete-mixability magnitudes.

        source
        theorem Papers.AnsariRockel2026RhoFootrule.centered_sum_variance_bound {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.ProbabilityMeasure Ω) (X : Ω → Fin 2 → ↑unitInterval) (hX : Measurable X) (hU : ∀ (i : Fin 2), MeasureTheory.Measure.map (fun (ω : Ω) => X ω i) ↑μ = MeasureTheory.volume) :
        have m := ∫ (ω : Ω), |↑(X ω 0) - 1 / 2 + (↑(X ω 1) - 1 / 2)| ∂↑μ; minimumVariance m ≤ ∫ (ω : Ω), (|↑(X ω 0) - 1 / 2 + (↑(X ω 1) - 1 / 2)| - m) ^ 2 ∂↑μ

        The bound applies on an arbitrary probability space, via the joint law of any two uniforms.