← Mathematical handbook

Revealing a central interval inside the symmetric-pair model

theorem Verification.foldKernel_prefix (t v : ↑unitInterval) : ∫ (u : ↑unitInterval) in Set.Iic t, foldKernel v u = (↑t - min (↑t) (max 0 (1 - 2 * ↑v)) + min (↑t) (max 0 (2 * ↑v - 1))) / 2

theorem Verification.reveal_prefix_eq_fold (t v : ↑unitInterval) : (∫ (u : ↑unitInterval) in Set.Iic t, if (1 - ↑t) / 2 + ↑u ≤ ↑v then 1 else 0) = ∫ (u : ↑unitInterval) in Set.Iic t, foldKernel v u

noncomputable def Verification.partialRevealKernel (t v u : ↑unitInterval) : ℝ

Equations

• Verification.partialRevealKernel t v u = if u ≤ t then if (1 - ↑t) / 2 + ↑u ≤ ↑v then 1 else 0 else Verification.foldKernel v u

theorem Verification.partialRevealKernel_measurable (t : ↑unitInterval) : Measurable fun (p : ↑unitInterval × ↑unitInterval) => partialRevealKernel t p.1 p.2

theorem Verification.partialRevealKernel_mem (t v u : ↑unitInterval) : partialRevealKernel t v u ∈ Set.Icc 0 1

theorem Verification.partialRevealKernel_integrable (t v : ↑unitInterval) : MeasureTheory.Integrable (partialRevealKernel t v) MeasureTheory.volume

theorem Verification.partialRevealKernel_mean (t v : ↑unitInterval) : ∫ (u : ↑unitInterval), partialRevealKernel t v u = ↑v

theorem Verification.partialRevealKernel_monotone (t u : ↑unitInterval) : Monotone fun (v : ↑unitInterval) => partialRevealKernel t v u

theorem Verification.partialRevealKernel_zero (t : ↑unitInterval) : partialRevealKernel t 0 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 0

theorem Verification.partialRevealKernel_one (t : ↑unitInterval) : partialRevealKernel t 1 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 1

noncomputable def Verification.partialReveal (t : ↑unitInterval) : ProbabilityTheory.Copula 2

Equations

• Verification.partialReveal t = Verification.copulaOfConditionalAE (Verification.partialRevealKernel t) ⋯ ⋯ ⋯ ⋯ ⋯

theorem Verification.partialReveal_conditionalCDF (t v : ↑unitInterval) : (fun (u : ↑unitInterval) => (partialReveal t).conditionalCDF u v) =ᵐ[MeasureTheory.volume] partialRevealKernel t v