Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.rearrangement_indicator_const

Carleson.ToMathlib.Rearrangement · Carleson/ToMathlib/Rearrangement.lean:201 to 224

Mathematical statement

Exact Lean statement

@[simp]
lemma rearrangement_indicator_const {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {s : Set α} {a : ε} :
  rearrangement (s.indicator (Function.const _ a)) x μ
    = ((Set.Iio (μ s)).indicator (Function.const _ ‖a‖ₑ) x)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[simp]lemma rearrangement_indicator_const {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {s : Set α} {a : ε} :  rearrangement (s.indicator (Function.const _ a)) x μ    = ((Set.Iio (μ s)).indicator (Function.const _ ‖a‖ₑ) x) := by  unfold rearrangement  simp_rw [distribution_indicator_const]  unfold Set.indicator  simp only [Set.mem_Iio, Function.const_apply]  split_ifs with h  · apply le_antisymm    · apply sInf_le      simp    · apply le_sInf      simp only [Set.mem_setOf_eq]      intro b hb      contrapose! hb      rwa [ite_cond_eq_true]      simpa  · rw [← ENNReal.bot_eq_zero, eq_bot_iff]    apply sInf_le    simp only [not_lt, bot_eq_zero', Set.mem_setOf_eq] at *    split_ifs    · assumption    · simp