← Mathematical handbook

Schur order of functions: rearrangements versus convex tests

For measurable f g : I → [0,1], the rearrangement form of the Schur order ∫_0^x f* ≤ ∫_0^x g* (all x) with equal integrals is equivalent to ∫ φ(f) ≤ ∫ φ(g) for all continuous φ convex on [0,1] (Hardy–Littlewood–Pólya).

def Verification.RearrSchurLE (f g : ↑unitInterval → ℝ) : Prop

Schur order of functions via decreasing rearrangements (Ansari–Rockel, Definition 2.2).

Equations

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

def Verification.ConvexSchurLE (f g : ↑unitInterval → ℝ) : Prop

Schur order of functions via continuous convex tests.

Equations

• Verification.ConvexSchurLE f g = ∀ (φ : ℝ → ℝ), Continuous φ → ConvexOn ℝ (Set.Icc 0 1) φ → ∫ (u : ↑unitInterval), φ (f u) ≤ ∫ (u : ↑unitInterval), φ (g u)

theorem Verification.integrable_of_unit {f : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (hm : Measurable f) {φ : ℝ → ℝ} (hφ : Continuous φ) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => φ (f u)) MeasureTheory.volume

theorem Verification.hinge_continuous (c : ℝ) : Continuous fun (y : ℝ) => max (y - c) 0

theorem Verification.hinge_convex (c : ℝ) : ConvexOn ℝ (Set.Icc 0 1) fun (y : ℝ) => max (y - c) 0

theorem Verification.integral_hinge_decRearr {f : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (hm : Measurable f) (c : ℝ) : ∫ (s : ↑unitInterval), max (decRearr f ↑s - c) 0 = ∫ (u : ↑unitInterval), max (f u - c) 0

theorem Verification.integral_Iic_decRearr_eq {f : ↑unitInterval → ℝ} (_hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (_hm : Measurable f) (x : ↑unitInterval) : ∫ (s : ↑unitInterval) in Set.Iic x, decRearr f ↑s = decRearr f ↑x * ↑x + ∫ (s : ↑unitInterval), max (decRearr f ↑s - decRearr f ↑x) 0

Partial integrals of an antitone rearrangement at its own level.

theorem Verification.integral_Iic_le_hinge {h : ↑unitInterval → ℝ} (hi : MeasureTheory.Integrable h MeasureTheory.volume) (x : ↑unitInterval) (c : ℝ) : ∫ (s : ↑unitInterval) in Set.Iic x, h s ≤ c * ↑x + ∫ (s : ↑unitInterval), max (h s - c) 0

theorem Verification.rearrSchurLE_of_convex {f g : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (hfm : Measurable f) (hg0 : ∀ (u : ↑unitInterval), 0 ≤ g u) (hg : ∀ (u : ↑unitInterval), g u ≤ 1) (hgm : Measurable g) (h : ConvexSchurLE f g) : RearrSchurLE f g

Convex tests imply the rearrangement Schur order.

theorem Verification.hinge_le_of_rearrSchurLE {f g : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (hfm : Measurable f) (hg0 : ∀ (u : ↑unitInterval), 0 ≤ g u) (hg : ∀ (u : ↑unitInterval), g u ≤ 1) (hgm : Measurable g) (h : RearrSchurLE f g) (c : ℝ) : ∫ (u : ↑unitInterval), max (f u - c) 0 ≤ ∫ (u : ↑unitInterval), max (g u - c) 0

The rearrangement Schur order implies all hinge comparisons.

Piecewise-linear convex interpolation

noncomputable def Verification.cellSlope (φ : ℝ → ℝ) (n k : ℕ) : ℝ

Slope of the k-th cell of the uniform partition with n cells.

Equations

• Verification.cellSlope φ n k = ↑n * (φ (↑(k + 1) / ↑n) - φ (↑k / ↑n))

noncomputable def Verification.hingeInterp (φ : ℝ → ℝ) (n : ℕ) (y : ℝ) : ℝ

Linear interpolation of φ at the nodes k/n, written with hinge functions.

Equations

• Verification.hingeInterp φ n y = φ 0 + Verification.cellSlope φ n 0 * y + ∑ k ∈ Finset.Ico 1 n, (Verification.cellSlope φ n k - Verification.cellSlope φ n (k - 1)) * max (y - ↑k / ↑n) 0

theorem Verification.cellSlope_mono {φ : ℝ → ℝ} (hφ : ConvexOn ℝ (Set.Icc 0 1) φ) {n k : ℕ} (hn : 0 < n) (hk : k + 1 < n) : cellSlope φ n k ≤ cellSlope φ n (k + 1)

theorem Verification.hinge_telescope (φ : ℝ → ℝ) (n : ℕ) (hn : 0 < n) (y : ℝ) (j : ℕ) : cellSlope φ n 0 * y + ∑ k ∈ Finset.Ico 1 (j + 1), (cellSlope φ n k - cellSlope φ n (k - 1)) * (y - ↑k / ↑n) = cellSlope φ n j * (y - ↑j / ↑n) + (φ (↑j / ↑n) - φ 0)

Algebraic telescoping identity for the hinge sum without the positive parts.

theorem Verification.hingeInterp_cell (φ : ℝ → ℝ) {n j : ℕ} (hn : 0 < n) (hj : j < n) {y : ℝ} (hy : y ∈ Set.Icc (↑j / ↑n) (↑(j + 1) / ↑n)) : hingeInterp φ n y = φ (↑j / ↑n) + cellSlope φ n j * (y - ↑j / ↑n)

theorem Verification.integral_hingeInterp_le {f g : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (hfm : Measurable f) (hg0 : ∀ (u : ↑unitInterval), 0 ≤ g u) (hg : ∀ (u : ↑unitInterval), g u ≤ 1) (hgm : Measurable g) (hint : ∫ (u : ↑unitInterval), f u = ∫ (u : ↑unitInterval), g u) (hh : ∀ (c : ℝ), ∫ (u : ↑unitInterval), max (f u - c) 0 ≤ ∫ (u : ↑unitInterval), max (g u - c) 0) {φ : ℝ → ℝ} (hφ : ConvexOn ℝ (Set.Icc 0 1) φ) {n : ℕ} (hn : 0 < n) : ∫ (u : ↑unitInterval), hingeInterp φ n (f u) ≤ ∫ (u : ↑unitInterval), hingeInterp φ n (g u)

Integral comparison for the hinge interpolant.

theorem Verification.hingeInterp_approx {φ : ℝ → ℝ} (hφc : Continuous φ) {ε : ℝ} (hε : 0 < ε) : ∃ (n : ℕ), 0 < n ∧ ∀ y ∈ Set.Icc 0 1, |hingeInterp φ n y - φ y| ≤ ε

Uniform approximation of a continuous convex function by its hinge interpolants.

theorem Verification.convexSchurLE_of_hinge {f g : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (hfm : Measurable f) (hg0 : ∀ (u : ↑unitInterval), 0 ≤ g u) (hg : ∀ (u : ↑unitInterval), g u ≤ 1) (hgm : Measurable g) (hint : ∫ (u : ↑unitInterval), f u = ∫ (u : ↑unitInterval), g u) (hh : ∀ (c : ℝ), ∫ (u : ↑unitInterval), max (f u - c) 0 ≤ ∫ (u : ↑unitInterval), max (g u - c) 0) : ConvexSchurLE f g

Majorization in the hinge form implies all continuous convex comparisons.

theorem Verification.rearrSchurLE_iff_convex {f g : ↑unitInterval → ℝ} (hf0 : ∀ (u : ↑unitInterval), 0 ≤ f u) (hf : ∀ (u : ↑unitInterval), f u ≤ 1) (hfm : Measurable f) (hg0 : ∀ (u : ↑unitInterval), 0 ≤ g u) (hg : ∀ (u : ↑unitInterval), g u ≤ 1) (hgm : Measurable g) : RearrSchurLE f g ↔ ConvexSchurLE f g

Hardy–Littlewood–Pólya on the unit interval, for [0,1]-valued functions.