← Mathematical handbook

The conditional branches of the randomized extremizer.

def Papers.Rockel2026ExactBlest.blockLow (a u : ↑unitInterval) : Fin 2 → ↑unitInterval

Equations

• Papers.Rockel2026ExactBlest.blockLow a u = ![ProbabilityTheory.Copula.OrdinalSum.lowerEmbed a u, unitInterval.symm (ProbabilityTheory.Copula.OrdinalSum.lowerEmbed a u)]

def Papers.Rockel2026ExactBlest.blockPlus (a p u : ↑unitInterval) : Fin 2 → ↑unitInterval

Equations

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

def Papers.Rockel2026ExactBlest.blockMinus (a p u : ↑unitInterval) : Fin 2 → ↑unitInterval

Equations

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

theorem Papers.Rockel2026ExactBlest.continuous_blockLow (a : ↑unitInterval) : Continuous (blockLow a)

theorem Papers.Rockel2026ExactBlest.continuous_blockPlus (a p : ↑unitInterval) : Continuous (blockPlus a p)

theorem Papers.Rockel2026ExactBlest.continuous_blockMinus (a p : ↑unitInterval) : Continuous (blockMinus a p)

theorem Papers.Rockel2026ExactBlest.block_joint_law (a p : ↑unitInterval) : (((ProbabilityTheory.Copula.comonotonic 2).ordinalSum (skewTent p) a).reflect {1}).toMeasure = ENNReal.ofReal ↑a • MeasureTheory.Measure.map (blockLow a) MeasureTheory.volume + ENNReal.ofReal (1 - ↑a) • (ENNReal.ofReal ↑p • MeasureTheory.Measure.map (blockPlus a p) MeasureTheory.volume + ENNReal.ofReal (1 - ↑p) • MeasureTheory.Measure.map (blockMinus a p) MeasureTheory.volume)

theorem Papers.Rockel2026ExactBlest.familyB_joint_law (a : ↑unitInterval) (ha : 1 / 2 ≤ ↑a) : (familyB a ha).survivalCopula.toMeasure = ENNReal.ofReal ↑a • MeasureTheory.Measure.map (blockLow a) MeasureTheory.volume + ENNReal.ofReal (1 - ↑a) • (ENNReal.ofReal ↑(randomSplit a ha) • MeasureTheory.Measure.map (blockPlus a (randomSplit a ha)) MeasureTheory.volume + ENNReal.ofReal (1 - ↑(randomSplit a ha)) • MeasureTheory.Measure.map (blockMinus a (randomSplit a ha)) MeasureTheory.volume)

theorem Papers.Rockel2026ExactBlest.block_branches_formula (a : ↑unitInterval) (ha : 1 / 2 ≤ ↑a) (u : ↑unitInterval) : ↑(blockMinus a (randomSplit a ha) u 1) = (↑(ProbabilityTheory.Copula.OrdinalSum.upperEmbed a u) - ↑a) / (2 * ↑a) ∧ ↑(blockPlus a (randomSplit a ha) u 1) = (↑a + ↑(ProbabilityTheory.Copula.OrdinalSum.upperEmbed a u) - 2 * ↑a * ↑(ProbabilityTheory.Copula.OrdinalSum.upperEmbed a u)) / (2 * ↑a) ∧ 1 - ↑(randomSplit a ha) = 1 / (2 * ↑a)

theorem Papers.Rockel2026ExactBlest.measurable_weighted_dirac (c : ENNReal) (f : ↑unitInterval → ↑unitInterval) (hf : Measurable f) : Measurable fun (x : ↑unitInterval) => c • MeasureTheory.Measure.dirac (f x)

noncomputable def Papers.Rockel2026ExactBlest.blockKernel (a p : ↑unitInterval) : ProbabilityTheory.Kernel ↑unitInterval ↑unitInterval

Equations

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

instance Papers.Rockel2026ExactBlest.blockKernel_markov (a p : ↑unitInterval) : ProbabilityTheory.IsMarkovKernel (blockKernel a p)

theorem Papers.Rockel2026ExactBlest.block_disintegration (a p : ↑unitInterval) (ha : ↑a < 1) (f : (Fin 2 → ↑unitInterval) → ENNReal) (hf : Measurable f) : ∫⁻ (y : Fin 2 → ↑unitInterval), f y ∂(((ProbabilityTheory.Copula.comonotonic 2).ordinalSum (skewTent p) a).reflect {1}).toMeasure = ∫⁻ (x : ↑unitInterval), ∫⁻ (z : ↑unitInterval), f ![x, z] ∂(blockKernel a p) x

theorem Papers.Rockel2026ExactBlest.familyB_disintegration (a : ↑unitInterval) (ha : 1 / 2 ≤ ↑a) (ha1 : ↑a < 1) (f : (Fin 2 → ↑unitInterval) → ENNReal) (hf : Measurable f) : ∫⁻ (y : Fin 2 → ↑unitInterval), f y ∂(familyB a ha).survivalCopula.toMeasure = ∫⁻ (x : ↑unitInterval), ∫⁻ (z : ↑unitInterval), f ![x, z] ∂(blockKernel a (randomSplit a ha)) x

theorem Papers.Rockel2026ExactBlest.block_not_first_graph (a p : ↑unitInterval) (ha : ↑a < 1) (hp0 : 0 < ↑p) (hp1 : ↑p < 1) (f : ↑unitInterval → ↑unitInterval) (hf : Measurable f) : ¬∀ᵐ (x : Fin 2 → ↑unitInterval) ∂(((ProbabilityTheory.Copula.comonotonic 2).ordinalSum (skewTent p) a).reflect {1}).toMeasure, x 1 = f (x 0)

theorem Papers.Rockel2026ExactBlest.familyB_not_first_graph (a : ↑unitInterval) (ha : 1 / 2 < ↑a) (ha1 : ↑a < 1) (f : ↑unitInterval → ↑unitInterval) (hf : Measurable f) : ¬∀ᵐ (x : Fin 2 → ↑unitInterval) ∂(familyB a ⋯).survivalCopula.toMeasure, x 1 = f (x 0)

theorem Papers.Rockel2026ExactBlest.upperEmbed_upperCoord (a x : ↑unitInterval) (ha : ↑a < 1) (hx : a ≤ x) : ProbabilityTheory.Copula.OrdinalSum.upperEmbed a (ProbabilityTheory.Copula.OrdinalSum.upperCoord a x) = x

theorem Papers.Rockel2026ExactBlest.familyB_conditional_formula (a : ↑unitInterval) (ha : 1 / 2 ≤ ↑a) (ha1 : ↑a < 1) (x : ↑unitInterval) : MeasureTheory.Measure.map (fun (z : ↑unitInterval) => ↑z) ((blockKernel a (randomSplit a ha)) x) = if x ≤ a then MeasureTheory.Measure.dirac (1 - ↑x) else ENNReal.ofReal (1 / (2 * ↑a)) • MeasureTheory.Measure.dirac ((↑x - ↑a) / (2 * ↑a)) + ENNReal.ofReal ((2 * ↑a - 1) / (2 * ↑a)) • MeasureTheory.Measure.dirac ((↑a + ↑x - 2 * ↑a * ↑x) / (2 * ↑a))

theorem Papers.Rockel2026ExactBlest.randomized_optimizer_not_first_graph (C : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha : 1 / 2 < ↑a) (ha1 : ↑a < 1) (he : eta C = etaB ↑a) (hn : Rockel2026XiBlest.blestNu C = nuB ↑a) (f : ↑unitInterval → ↑unitInterval) (hf : Measurable f) : ¬∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.survivalCopula.toMeasure, x 1 = f (x 0)