Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.rearrangement_indicator_le

Carleson.ToMathlib.Rearrangement · Carleson/ToMathlib/Rearrangement.lean:186 to 199

Mathematical statement

Exact Lean statement

lemma rearrangement_indicator_le {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε}
  {X : Set α} :
    rearrangement (X.indicator f) x μ ≤
      Set.indicator (Set.Iio (μ X)) (rearrangement f · μ) x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rearrangement_indicator_le {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {f : α → ε}  {X : Set α} :    rearrangement (X.indicator f) x μ ≤      Set.indicator (Set.Iio (μ X)) (rearrangement f · μ) x := by  rw [rearrangement_le_iff_distribution_le]  rw [Set.indicator_apply]  split_ifs with hx  · apply (distribution_mono_left _).trans distribution_rearrangement_le    filter_upwards    intro a    unfold Set.indicator    split_ifs <;> simp  · simp only [Set.mem_Iio, not_lt] at hx    exact distribution_indicator_le_measure.trans hx