Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.Antitone.antitone_eapprox

Carleson.ToMathlib.MeasureTheory.Function.SimpleFunc · Carleson/ToMathlib/MeasureTheory/Function/SimpleFunc.lean:549 to 562

Mathematical statement

Exact Lean statement

lemma Antitone.antitone_eapprox {α : Type*} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  [LinearOrder α] [OrderClosedTopology α] ⦃f : α → ℝ≥0∞⦄ (hf : Antitone f) {n : ℕ} :
    Antitone (SimpleFunc.eapprox f n)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma Antitone.antitone_eapprox {α : Type*} [TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]  [LinearOrder α] [OrderClosedTopology α] ⦃f : α → ℝ≥0∞⦄ (hf : Antitone f) {n : ℕ} :    Antitone (SimpleFunc.eapprox f n) := by  unfold SimpleFunc.eapprox  intro x y hxy  rw [SimpleFunc.approx_apply _ hf.measurable, SimpleFunc.approx_apply _ hf.measurable]  gcongr with m hm  split_ifs with hy hx  · rfl  · exfalso    push Not at hx    exact lt_irrefl _ ((hy.trans (hf hxy)).trans_lt hx)  · simp only [zero_le]  · rfl