Documentation

Copula.Rearrangement.Primitive

← Copula mathematical handbook

Rearranging a derivative: the primitive of a mean-zero function #

The primitive comparison lemma for decreasing rearrangements. For a measurable h : I → [0,1] with ∫ h = v, put f = h - v (a bounded mean-zero function) and

F(u) = ∫_0^u f = ∫_0^u h - u v, G(u) = ∫_0^u f↓ = ∫_0^u h↓ - u v,

where h↓ = decRearr h is the decreasing rearrangement (f↓ = h↓ - v). This file proves the structural statements: G is concave (chord inequality) and nonnegative, the two-sided bound -G(1 - λ(E)) ≤ ∫_E f ≤ G(λ(E)) for measurable E, hence -G(1-u) ≤ F(u) ≤ G(u) and |F| ≤ max G, and the level-set inequality λ{|F| > y} ≤ λ{G > y} for y ≥ 0 (with a quantitative improvement when F takes both signs). The integral consequences (∫ |F|^p ≤ ∫ G^p and the strict versions) are in Copula.Rearrangement.PrimitiveIntegral.

noncomputable def ProbabilityTheory.Copula.measureUnit (A : Set ↑unitInterval) :

↑unitInterval

The measure of a subset of the unit interval, as a point of the unit interval.

Equations

ProbabilityTheory.Copula.measureUnit A = ⟨MeasureTheory.volume.real A, ⋯⟩

Instances For

@[simp]

theorem ProbabilityTheory.Copula.coe_measureUnit (A : Set ↑unitInterval) :

↑(measureUnit A) = MeasureTheory.volume.real A

theorem ProbabilityTheory.Copula.measureUnit_Iic (u : ↑unitInterval) :

measureUnit (Set.Iic u) = u

theorem ProbabilityTheory.Copula.measureReal_Ioo_unit (a b : ↑unitInterval) (hab : a ≤ b) :

MeasureTheory.volume.real (Set.Ioo a b) = ↑b - ↑a

theorem ProbabilityTheory.Copula.measureReal_Icc_unit (a b : ↑unitInterval) (hab : a ≤ b) :

MeasureTheory.volume.real (Set.Icc a b) = ↑b - ↑a

theorem ProbabilityTheory.Copula.measureReal_compl_unit (A : Set ↑unitInterval) (hA : MeasurableSet A) :

MeasureTheory.volume.real Aᶜ = 1 - MeasureTheory.volume.real A

The primitive of a bounded function and its continuity #

noncomputable def ProbabilityTheory.Copula.primitive (h : ↑unitInterval → ℝ) (u : ↑unitInterval) :

The primitive u ↦ ∫_0^u h, as a function on the unit interval.

Equations

ProbabilityTheory.Copula.primitive h u = ∫ (t : ↑unitInterval) in Set.Iic u, h t

Instances For

theorem ProbabilityTheory.Copula.primitive_zero (h : ↑unitInterval → ℝ) :

primitive h 0 = 0

theorem ProbabilityTheory.Copula.primitive_one (h : ↑unitInterval → ℝ) :

primitive h 1 = ∫ (t : ↑unitInterval), h t

theorem ProbabilityTheory.Copula.integrable_of_unit_bounds {h : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) :

MeasureTheory.Integrable h MeasureTheory.volume

theorem ProbabilityTheory.Copula.primitive_sub_primitive {h : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) {a b : ↑unitInterval} (hab : a ≤ b) :

primitive h b - primitive h a = ∫ (t : ↑unitInterval) in Set.Ioc a b, h t

theorem ProbabilityTheory.Copula.primitive_sub_primitive_Ioo {h : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) {a b : ↑unitInterval} (hab : a ≤ b) :

primitive h b - primitive h a = ∫ (t : ↑unitInterval) in Set.Ioo a b, h t

theorem ProbabilityTheory.Copula.primitive_mono {h : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) {a b : ↑unitInterval} (hab : a ≤ b) :

primitive h a ≤ primitive h b

theorem ProbabilityTheory.Copula.primitive_sub_le {h : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) {a b : ↑unitInterval} (hab : a ≤ b) :

primitive h b - primitive h a ≤ ↑b - ↑a

theorem ProbabilityTheory.Copula.continuous_primitive {h : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) :

Continuous (primitive h)

The deviation functions `F` and `G` #

noncomputable def ProbabilityTheory.Copula.primDev (h : ↑unitInterval → ℝ) (v : ℝ) (u : ↑unitInterval) :

F(u) = ∫_0^u h - u v, the primitive of the mean-zero function h - v.

Equations

ProbabilityTheory.Copula.primDev h v u = ProbabilityTheory.Copula.primitive h u - ↑u * v

Instances For

noncomputable def ProbabilityTheory.Copula.rearrDev (h : ↑unitInterval → ℝ) (v : ℝ) (u : ↑unitInterval) :

G(u) = ∫_0^u h↓ - u v, the primitive of the decreasing rearrangement h↓ - v.

Equations

ProbabilityTheory.Copula.rearrDev h v u = ProbabilityTheory.Copula.primitive (fun (t : ↑unitInterval) => ProbabilityTheory.Copula.decRearr h ↑t) u - ↑u * v

Instances For

theorem ProbabilityTheory.Copula.decRearr_nonneg' {h : ↑unitInterval → ℝ} (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (s : ↑unitInterval) :

0 ≤ decRearr h ↑s

theorem ProbabilityTheory.Copula.decRearr_le_one' {h : ↑unitInterval → ℝ} (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (s : ↑unitInterval) :

decRearr h ↑s ≤ 1

theorem ProbabilityTheory.Copula.primDev_zero {h : ↑unitInterval → ℝ} {v : ℝ} :

primDev h v 0 = 0

theorem ProbabilityTheory.Copula.rearrDev_zero {h : ↑unitInterval → ℝ} {v : ℝ} :

rearrDev h v 0 = 0

theorem ProbabilityTheory.Copula.primDev_one {h : ↑unitInterval → ℝ} {v : ℝ} (hv : ∫ (u : ↑unitInterval), h u = v) :

primDev h v 1 = 0

theorem ProbabilityTheory.Copula.rearrDev_one {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (hv : ∫ (u : ↑unitInterval), h u = v) :

rearrDev h v 1 = 0

theorem ProbabilityTheory.Copula.continuous_primDev {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) :

Continuous (primDev h v)

theorem ProbabilityTheory.Copula.continuous_rearrDev {h : ↑unitInterval → ℝ} {v : ℝ} (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) :

Continuous (rearrDev h v)

theorem ProbabilityTheory.Copula.measurable_primDev {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) :

Measurable (primDev h v)

theorem ProbabilityTheory.Copula.measurable_rearrDev {h : ↑unitInterval → ℝ} {v : ℝ} (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) :

Measurable (rearrDev h v)

theorem ProbabilityTheory.Copula.rearrDev_chord {h : ↑unitInterval → ℝ} {v : ℝ} (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) {a b c : ↑unitInterval} (hab : a ≤ b) (hbc : b ≤ c) :

(↑b - ↑a) * rearrDev h v c + (↑c - ↑b) * rearrDev h v a ≤ (↑c - ↑a) * rearrDev h v b

The chord inequality expressing concavity of G.

theorem ProbabilityTheory.Copula.rearrDev_nonneg {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (hv : ∫ (u : ↑unitInterval), h u = v) (u : ↑unitInterval) :

0 ≤ rearrDev h v u

The rearranged primitive is nonnegative: G ≥ 0.

theorem ProbabilityTheory.Copula.rearrDev_ge_of_ge {h : ↑unitInterval → ℝ} {v : ℝ} (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) {y : ℝ} {a b c : ↑unitInterval} (hab : a ≤ b) (hbc : b ≤ c) (ha : y ≤ rearrDev h v a) (hc : y ≤ rearrDev h v c) :

y ≤ rearrDev h v b

Concavity keeps G ≥ y on the interval between two points where G ≥ y.

theorem ProbabilityTheory.Copula.rearrDev_le_one {h : ↑unitInterval → ℝ} {v : ℝ} (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hv0 : 0 ≤ v) (u : ↑unitInterval) :

rearrDev h v u ≤ 1

theorem ProbabilityTheory.Copula.integral_set_sub_le_rearrDev {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (E : Set ↑unitInterval) :

(∫ (u : ↑unitInterval) in E, h u) - MeasureTheory.volume.real E * v ≤ rearrDev h v (measureUnit E)

Two-sided bound, upper half: ∫_E f ≤ G(λ(E)) for every measurable E (bathtub principle).

theorem ProbabilityTheory.Copula.neg_rearrDev_le_integral_set_sub {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (hv : ∫ (u : ↑unitInterval), h u = v) (E : Set ↑unitInterval) (hE : MeasurableSet E) :

-rearrDev h v (unitInterval.symm (measureUnit E)) ≤ (∫ (u : ↑unitInterval) in E, h u) - MeasureTheory.volume.real E * v

Two-sided bound, lower half: -G(1 - λ(E)) ≤ ∫_E f for every measurable E.

theorem ProbabilityTheory.Copula.primDev_le_rearrDev {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (u : ↑unitInterval) :

primDev h v u ≤ rearrDev h v u

F ≤ G pointwise.

theorem ProbabilityTheory.Copula.neg_rearrDev_symm_le_primDev {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (hv : ∫ (u : ↑unitInterval), h u = v) (u : ↑unitInterval) :

-rearrDev h v (unitInterval.symm u) ≤ primDev h v u

-G(1-u) ≤ F(u).

theorem ProbabilityTheory.Copula.abs_primDev_le_max {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (hv : ∫ (u : ↑unitInterval), h u = v) (u : ↑unitInterval) :

|primDev h v u| ≤ max (rearrDev h v u) (rearrDev h v (unitInterval.symm u))

|F| ≤ max G, in pointwise form.

theorem ProbabilityTheory.Copula.abs_primDev_le_one {h : ↑unitInterval → ℝ} {v : ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ h u) (hf1 : ∀ (u : ↑unitInterval), h u ≤ 1) (hm : Measurable h) (hv : ∫ (u : ↑unitInterval), h u = v) (u : ↑unitInterval) :

|primDev h v u| ≤ 1