Papers.Rockel2026ExactBlest.ExactBlestRearrangement

← Mathematical handbook

The general integrable rearrangement lemma from exact-blest-regions.tex.

source

noncomputable def Papers.Rockel2026ExactBlest.tailIndicator (v t : ↑unitInterval) :

ℝ

Equations

Papers.Rockel2026ExactBlest.tailIndicator v t = if t < v then 1 else 0

Instances For

source

theorem Papers.Rockel2026ExactBlest.integral_tailIndicator (v : ↑unitInterval) :

∫ (t : ↑unitInterval), tailIndicator v t = ↑v

source

theorem Papers.Rockel2026ExactBlest.integral_uniform_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (V : Ω → ↑unitInterval) (hV : MeasureTheory.MeasurePreserving V μ MeasureTheory.volume) (t : ↑unitInterval) :

∫ (ω : Ω), tailIndicator (V ω) t ∂μ = 1 - ↑t

source

theorem Papers.Rockel2026ExactBlest.uniform_ae_ne {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (V : Ω → ↑unitInterval) (hV : MeasureTheory.MeasurePreserving V μ MeasureTheory.volume) (t : ↑unitInterval) :

∀ᵐ (ω : Ω) ∂μ, V ω ≠ t

source

theorem Papers.Rockel2026ExactBlest.integrable_weighted_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (G : Ω → ℝ) (hG : MeasureTheory.Integrable G μ) (V : Ω → ↑unitInterval) (hV : Measurable V) (t : ↑unitInterval) :

MeasureTheory.Integrable (fun (ω : Ω) => G ω * tailIndicator (V ω) t) μ

source

theorem Papers.Rockel2026ExactBlest.integrable_tail_prod {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (G : Ω → ℝ) (hG : MeasureTheory.Integrable G μ) (V : Ω → ↑unitInterval) (hV : Measurable V) :

MeasureTheory.Integrable (fun (p : Ω × ↑unitInterval) => G p.1 * tailIndicator (V p.1) p.2) (μ.prod MeasureTheory.volume)

source

theorem Papers.Rockel2026ExactBlest.weighted_tail_layercake {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.SFinite μ] (G : Ω → ℝ) (hG : MeasureTheory.Integrable G μ) (V : Ω → ↑unitInterval) (hV : Measurable V) :

∫ (t : ↑unitInterval), ∫ (ω : Ω), G ω * tailIndicator (V ω) t ∂μ = ∫ (ω : Ω), G ω * ↑(V ω) ∂μ

source

theorem Papers.Rockel2026ExactBlest.weighted_tail_shift {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (G : Ω → ℝ) (hG : MeasureTheory.Integrable G μ) (V : Ω → ↑unitInterval) (hV : MeasureTheory.MeasurePreserving V μ MeasureTheory.volume) (t : ↑unitInterval) (q : ℝ) :

∫ (ω : Ω), (G ω - q) * tailIndicator (V ω) t ∂μ = ∫ (ω : Ω), G ω * tailIndicator (V ω) t ∂μ - q * (1 - ↑t)

source

theorem Papers.Rockel2026ExactBlest.threshold_rearrangement {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (G : Ω → ℝ) (hG : MeasureTheory.Integrable G μ) (H V : Ω → ↑unitInterval) (hH : MeasureTheory.MeasurePreserving H μ MeasureTheory.volume) (hV : MeasureTheory.MeasurePreserving V μ MeasureTheory.volume) (t : ↑unitInterval) (q : ℝ) (halign : ∀ᵐ (ω : Ω) ∂μ, (t < H ω ↔ q < G ω) ∧ G ω ≠ q) :

∫ (ω : Ω), G ω * tailIndicator (V ω) t ∂μ ≤ ∫ (ω : Ω), G ω * tailIndicator (H ω) t ∂μ ∧ (∫ (ω : Ω), G ω * tailIndicator (V ω) t ∂μ = ∫ (ω : Ω), G ω * tailIndicator (H ω) t ∂μ ↔ ∀ᵐ (ω : Ω) ∂μ, tailIndicator (V ω) t = tailIndicator (H ω) t)

Among equal-probability events, the strict upper-tail event uniquely maximizes the G integral.

source

noncomputable def Papers.Rockel2026ExactBlest.cdfRank {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (G : Ω → ℝ) (ω : Ω) :

↑unitInterval

Equations

Papers.Rockel2026ExactBlest.cdfRank μ G ω = ProbabilityTheory.cdfUnit (MeasureTheory.Measure.map G μ) (G ω)

Instances For

source

theorem Papers.Rockel2026ExactBlest.cdfRank_uniform {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (G : Ω → ℝ) (hG : Measurable G) (hc : Continuous ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map G μ))) :

MeasureTheory.MeasurePreserving (cdfRank μ G) μ MeasureTheory.volume

source

theorem Papers.Rockel2026ExactBlest.cdfRank_threshold {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (G : Ω → ℝ) (hG : Measurable G) (hc : Continuous ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map G μ))) (t : ↑unitInterval) (ht : ↑t ∈ Set.Ioo 0 1) :

∃ (q : ℝ), ∀ᵐ (ω : Ω) ∂μ, (t < cdfRank μ G ω ↔ q < G ω) ∧ G ω ≠ q

source

theorem Papers.Rockel2026ExactBlest.rearrangement {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (G : Ω → ℝ) (hGm : Measurable G) (hG : MeasureTheory.Integrable G μ) (hc : Continuous ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map G μ))) (V : Ω → ↑unitInterval) (hV : MeasureTheory.MeasurePreserving V μ MeasureTheory.volume) :

∫ (ω : Ω), G ω * ↑(V ω) ∂μ ≤ ∫ (ω : Ω), G ω * ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map G μ)) (G ω) ∂μ ∧ (∫ (ω : Ω), G ω * ↑(V ω) ∂μ = ∫ (ω : Ω), G ω * ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map G μ)) (G ω) ∂μ ↔ ∀ᵐ (ω : Ω) ∂μ, ↑(V ω) = ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map G μ)) (G ω))

The manuscript's general rearrangement inequality and its almost-sure equality case. G is merely integrable; neither boundedness nor a strictly increasing CDF is assumed.