Documentation

Verification.FoldedUniform

← Mathematical handbook

The copula of (abs(2U-1), U) #

noncomputable def Verification.foldLower (u : ↑unitInterval) :

↑unitInterval

Equations

Verification.foldLower u = ⟨(1 - ↑u) / 2, ⋯⟩

Instances For

noncomputable def Verification.foldUpper (u : ↑unitInterval) :

↑unitInterval

Equations

Verification.foldUpper u = ⟨(1 + ↑u) / 2, ⋯⟩

Instances For

theorem Verification.continuous_foldLower :

Continuous foldLower

theorem Verification.continuous_foldUpper :

Continuous foldUpper

noncomputable def Verification.foldKernel (v u : ↑unitInterval) :

Equations

Verification.foldKernel v u = (if Verification.foldLower u ≤ v then 1 else 0) / 2 + (if Verification.foldUpper u ≤ v then 1 else 0) / 2

Instances For

theorem Verification.foldKernel_measurable :

Measurable fun (p : ↑unitInterval × ↑unitInterval) => foldKernel p.1 p.2

theorem Verification.foldKernel_mem (v u : ↑unitInterval) :

foldKernel v u ∈ Set.Icc 0 1

theorem Verification.foldKernel_integrable (v : ↑unitInterval) :

MeasureTheory.Integrable (foldKernel v) MeasureTheory.volume

theorem Verification.fold_indicator_integrable (f : ↑unitInterval → ↑unitInterval) (hf : Measurable f) (v : ↑unitInterval) :

MeasureTheory.Integrable (fun (u : ↑unitInterval) => if f u ≤ v then 1 else 0) MeasureTheory.volume

theorem Verification.fold_lower_integral (v : ↑unitInterval) :

(∫ (u : ↑unitInterval), if foldLower u ≤ v then 1 else 0) = unitClamp (2 * ↑v)

theorem Verification.fold_upper_integral (v : ↑unitInterval) :

(∫ (u : ↑unitInterval), if foldUpper u ≤ v then 1 else 0) = unitClamp (2 * ↑v - 1)

theorem Verification.foldKernel_mean (v : ↑unitInterval) :

∫ (u : ↑unitInterval), foldKernel v u = ↑v

theorem Verification.foldKernel_monotone (u : ↑unitInterval) :

Monotone fun (v : ↑unitInterval) => foldKernel v u

theorem Verification.foldKernel_zero :

foldKernel 0 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 0

theorem Verification.foldKernel_one :

foldKernel 1 =ᵐ[MeasureTheory.volume] fun (x : ↑unitInterval) => 1

noncomputable def Verification.foldedUniform :

ProbabilityTheory.Copula 2

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Verification.foldedUniform_conditionalCDF (v : ↑unitInterval) :

(fun (u : ↑unitInterval) => foldedUniform.conditionalCDF u v) =ᵐ[MeasureTheory.volume] foldKernel v

theorem Verification.foldedUniform_cdf (u v : ↑unitInterval) :

foldedUniform.cdf ![u, v] = ∫ (t : ↑unitInterval) in Set.Iic u, foldKernel v t