Documentation

Verification.DiagonalHoleEndpoints

← Mathematical handbook

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

Equations

Verification.medianLow u = if ↑u ≤ 1 / 2 then 1 else 0

Instances For

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

Equations

Verification.medianHigh u = 1 - Verification.medianLow u

Instances For

theorem Verification.medianLow_measurable :

Measurable medianLow

theorem Verification.medianHigh_measurable :

Measurable medianHigh

theorem Verification.medianLow_mem (u : ↑unitInterval) :

medianLow u ∈ Set.Icc 0 1

theorem Verification.medianHigh_mem (u : ↑unitInterval) :

medianHigh u ∈ Set.Icc 0 1

theorem Verification.medianLow_integrable :

MeasureTheory.Integrable medianLow MeasureTheory.volume

theorem Verification.medianHigh_integrable :

MeasureTheory.Integrable medianHigh MeasureTheory.volume

theorem Verification.medianLow_prefix (t : ↑unitInterval) :

∫ (u : ↑unitInterval) in Set.Iic t, medianLow u = min (↑t) (1 / 2)

theorem Verification.medianHigh_prefix (t : ↑unitInterval) :

∫ (u : ↑unitInterval) in Set.Iic t, medianHigh u = max 0 (↑t - 1 / 2)

theorem Verification.medianLow_integral :

∫ (u : ↑unitInterval), medianLow u = 1 / 2

theorem Verification.medianHigh_integral :

∫ (u : ↑unitInterval), medianHigh u = 1 / 2

noncomputable def Verification.medianOffDensity (p : ↑unitInterval × ↑unitInterval) :

Equations

Verification.medianOffDensity p = 2 * (Verification.medianLow p.1 * Verification.medianHigh p.2 + Verification.medianHigh p.1 * Verification.medianLow p.2)

Instances For

theorem Verification.medianOffDensity_measurable :

Measurable medianOffDensity

theorem Verification.medianOffDensity_nonneg (p : ↑unitInterval × ↑unitInterval) :

0 ≤ medianOffDensity p

theorem Verification.medianOffDensity_integral (t : ↑unitInterval) :

∫ (u : ↑unitInterval), medianOffDensity (u, t) = 1

noncomputable def Verification.diagonalHoleCorner :

Equations

Verification.diagonalHoleCorner = Verification.diagonalHoleBand (1 / 2) (1 / 2) Verification.diagonalHoleCorner._proof_1 Verification.diagonalHoleCorner._proof_1

Instances For

theorem Verification.diagonalHoleCorner_density (u v : ↑unitInterval) (hv : ↑v ≠ 1 / 2) :

diagonalHoleCorner.density (u, v) = medianOffDensity (u, v)

theorem Verification.diagonalHoleCorner_columnDensity :

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

theorem Verification.diagonalHoleCorner_marginal :

diagonalHoleCorner.marginal = MeasureTheory.volume

theorem Verification.diagonalHoleCorner_copula_density :

diagonalHoleCorner.copula.toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (medianOffDensity (x 0, x 1))

theorem Verification.medianOffDensity_cube_integrable :

MeasureTheory.Integrable (fun (x : Fin 2 → ↑unitInterval) => medianOffDensity (x 0, x 1)) MeasureTheory.volume

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

∫ (x : Fin (Nat.succ 0).succ → ↑unitInterval) in Set.Iic ![u, v], medianOffDensity (x 0, x 1) = 2 * (min (↑u) (1 / 2) * max 0 (↑v - 1 / 2) + max 0 (↑u - 1 / 2) * min (↑v) (1 / 2))