`PhysMeasureBasis.cdf_jump_separation` (F G : ℝ → ℝ) (_hF : Monotone F) (_hG : Monotone G) (x₀ : ℝ) (hFc : ContinuousAt F x₀) (ε : ℝ) (hε : 0 < ε) (hjump : ∀ a b : ℝ, a <...

Proved

PhysMeasureBasis.cdf_jump_separation

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from PhysMeasureBasis.

PhysMeasureBasis.cdf_jump_separation (F G : ℝ → ℝ) (_hF : Monotone F) (_hG : Monotone G) (x₀ : ℝ) (hFc : ContinuousAt F x₀) (ε : ℝ) (hε : 0 < ε) (hjump : ∀ a b : ℝ, a < x₀ → x₀ < b → G b - G a ≥ ε) : ∃ a b : ℚ, (a:ℝ) < b ∧ |(G b - G a) - (F b - F a)| ≥ ε / 2

Formalization note: Lean 4 identifier PhysMeasureBasis.cdf_jump_separation.

Preamble

-- Generated from PhysMeasureBasis.lean — theorem PhysMeasureBasis.cdf_jump_separation
import Mathlib
import Definitions.Def_PhysMeasureBasis
import Definitions.Def_ChapterA4
open PhysMeasureBasis


open MeasureTheory Set ProbabilityTheory
open scoped ENNReal

noncomputable section

Formal statement

theorem PhysMeasureBasis.cdf_jump_separation (F G : ℝ → ℝ) (_hF : Monotone F) (_hG : Monotone G)
    (x₀ : ℝ) (hFc : ContinuousAt F x₀) (ε : ℝ) (hε : 0 < ε)
    (hjump : ∀ a b : ℝ, a < x₀ → x₀ < b → G b - G a ≥ ε) :
    ∃ a b : ℚ, (a:ℝ) < b ∧ |(G b - G a) - (F b - F a)| ≥ ε / 2 := by sorry

View graph