← Mathematical handbook

Equality in the decreasing-function diagonal moment bound

Vanishing of an elementary nonnegative defect gives three possible values. The lengths of the one and positive level sets give canonical cut points.

noncomputable def Verification.oneLevel (g : ↑unitInterval → ℝ) (u : ↑unitInterval) : ℝ

Equations

• Verification.oneLevel g u = if g u = 1 then 1 else 0

noncomputable def Verification.positiveLevel (g : ↑unitInterval → ℝ) (u : ↑unitInterval) : ℝ

Equations

• Verification.positiveLevel g u = if 0 < g u then 1 else 0

theorem Verification.oneLevel_mem (g : ↑unitInterval → ℝ) (u : ↑unitInterval) : oneLevel g u ∈ Set.Icc 0 1

theorem Verification.positiveLevel_mem (g : ↑unitInterval → ℝ) (u : ↑unitInterval) : positiveLevel g u ∈ Set.Icc 0 1

theorem Verification.measurable_oneLevel {g : ↑unitInterval → ℝ} (hg : Measurable g) : Measurable (oneLevel g)

theorem Verification.measurable_positiveLevel {g : ↑unitInterval → ℝ} (hg : Measurable g) : Measurable (positiveLevel g)

theorem Verification.integral_unit_mem {g : ↑unitInterval → ℝ} (hg : Measurable g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) : ∫ (u : ↑unitInterval), g u ∈ Set.Icc 0 1

theorem Verification.oneLevel_le_self {g : ↑unitInterval → ℝ} (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) (u : ↑unitInterval) : oneLevel g u ≤ g u

theorem Verification.self_le_positiveLevel {g : ↑unitInterval → ℝ} (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) (u : ↑unitInterval) : g u ≤ positiveLevel g u

theorem Verification.oneLevel_antitone {g : ↑unitInterval → ℝ} (hg : Antitone g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) : Antitone (oneLevel g)

theorem Verification.positiveLevel_antitone {g : ↑unitInterval → ℝ} (hg : Antitone g) : Antitone (positiveLevel g)

noncomputable def Verification.threeLevel (A B : ↑unitInterval) (a : ℝ) (u : ↑unitInterval) : ℝ

Equations

• Verification.threeLevel A B a u = (1 - a) * Verification.lowerStep A u + a * Verification.lowerStep B u

theorem Verification.integrable_threeLevel (A B : ↑unitInterval) (a : ℝ) : MeasureTheory.Integrable (threeLevel A B a) MeasureTheory.volume

theorem Verification.integral_threeLevel_Iic (A B : ↑unitInterval) (a : ℝ) (v : ↑unitInterval) : ∫ (u : ↑unitInterval) in Set.Iic v, threeLevel A B a u = (1 - a) * min ↑v ↑A + a * min ↑v ↑B

theorem Verification.integral_threeLevel (A B : ↑unitInterval) (a : ℝ) : ∫ (u : ↑unitInterval), threeLevel A B a u = ↑A + a * (↑B - ↑A)

theorem Verification.threeLevel_sq (A B : ↑unitInterval) (hAB : A ≤ B) (a : ℝ) (u : ↑unitInterval) : threeLevel A B a u ^ 2 = threeLevel A B (a ^ 2) u

theorem Verification.threeLevel_moment_eq (A B : ↑unitInterval) (hAB : A ≤ B) (a v : ↑unitInterval) (hm : ∫ (u : ↑unitInterval), threeLevel A B (↑a) u = ↑v) : ∫ (u : ↑unitInterval), threeLevel A B (↑a) u ^ 2 = ∫ (u : ↑unitInterval) in Set.Iic v, threeLevel A B (↑a) u

theorem Verification.ae_three_values_of_diagonal_moment_eq {g : ↑unitInterval → ℝ} (hg : Antitone g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) (v : ↑unitInterval) (hm : ∫ (u : ↑unitInterval), g u = ↑v) (heq : ∫ (u : ↑unitInterval), g u ^ 2 = ∫ (u : ↑unitInterval) in Set.Iic v, g u) : ∀ᵐ (u : ↑unitInterval), g u = 0 ∨ g u = g v ∨ g u = 1

Equality forces at most one intermediate level, namely g(v).

theorem Verification.ae_threeLevel_of_three_values {g : ↑unitInterval → ℝ} (hg : Antitone g) (hb : ∀ (u : ↑unitInterval), g u ∈ Set.Icc 0 1) (a : ↑unitInterval) (hvals : ∀ᵐ (u : ↑unitInterval), g u = 0 ∨ g u = ↑a ∨ g u = 1) (A B : ↑unitInterval) (hA : ∫ (u : ↑unitInterval), oneLevel g u = ↑A) (hB : ∫ (u : ↑unitInterval), positiveLevel g u = ↑B) : g =ᵐ[MeasureTheory.volume] threeLevel A B ↑a

Canonical level-set cuts recover an antitone three-valued function.

theorem Verification.threeLevel_eq_normalized (A B : ↑unitInterval) (a : ℝ) (v : ↑unitInterval) (hm : ∫ (u : ↑unitInterval), threeLevel A B a u = ↑v) : threeLevel A B a = threeLevel A B ((↑v - ↑A) / (↑B - ↑A))

Changing the intermediate value to its value determined by the mean also works when the two cut points coincide.

noncomputable def Verification.threeLevelOpen (A B : ↑unitInterval) (a : ℝ) (u : ↑unitInterval) : ℝ

The source's open-interval convention differs only at the two cuts.

Equations

• Verification.threeLevelOpen A B a u = (if u < A then 1 else 0) + a * if A < u ∧ u < B then 1 else 0

theorem Verification.threeLevel_eq_open_ae (A B : ↑unitInterval) (hAB : A ≤ B) (a : ℝ) : threeLevel A B a =ᵐ[MeasureTheory.volume] threeLevelOpen A B a

theorem Verification.threeLevelOpen_max (A B : ↑unitInterval) (a : ℝ) : threeLevelOpen A (max A B) a = threeLevelOpen A B a

Unordered cuts in the source formula can always be normalized by max.