← Mathematical handbook

Identifying the folded example with its stated joint law

noncomputable def Verification.foldSample (p : ↑unitInterval × ↑unitInterval) : Fin 2 → ↑unitInterval

Equations

• Verification.foldSample p = if ↑p.2 ≤ 1 / 2 then ![p.1, Verification.foldLower p.1] else ![p.1, Verification.foldUpper p.1]

theorem Verification.foldSample_measurable : Measurable foldSample

theorem Verification.foldSample_orthant (u v : ↑unitInterval) : (∫ (p : ↑unitInterval × ↑unitInterval), if foldSample p ≤ ![u, v] then 1 else 0) = foldedUniform.cdf ![u, v]

theorem Verification.foldedUniform_toMeasure_sample : foldedUniform.toMeasure = MeasureTheory.Measure.map foldSample MeasureTheory.volume

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

Equations

• Verification.foldRank u = ⟨|2 * ↑u - 1|, ⋯⟩

theorem Verification.continuous_foldRank : Continuous foldRank

theorem Verification.foldedUniform_joint_law : foldedUniform.toMeasure = MeasureTheory.Measure.map (fun (u : ↑unitInterval) => ![foldRank u, u]) MeasureTheory.volume

Exactly the law of (abs(2U-1), U), with U uniform.

theorem Verification.foldRank_measurePreserving : MeasureTheory.MeasurePreserving foldRank MeasureTheory.volume MeasureTheory.volume

The first variable in the source example is uniform too.