Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.setLIntegral_enorm_eq

Carleson.ToMathlib.Rearrangement · Carleson/ToMathlib/Rearrangement.lean:829 to 841

Mathematical statement

Exact Lean statement

lemma setLIntegral_enorm_eq {ε} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε}
  (hf : AEStronglyMeasurable f μ) {X : Set α} (hX : NullMeasurableSet X μ) :
    ∫⁻ x in X, ‖f x‖ₑ ∂μ =
      ∫⁻ t, μ (X ∩ {x | t < ‖f x‖ₑ})

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma setLIntegral_enorm_eq {ε} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε}  (hf : AEStronglyMeasurable f μ) {X : Set α} (hX : NullMeasurableSet X μ) :    ∫⁻ x in X, ‖f x‖ₑ ∂μ =      ∫⁻ t, μ (X ∩ {x | t < ‖f x‖ₑ}) := by  rw [← lintegral_indicator₀ hX, lintegral_eq_lintegral_distribution _ (by measurability)]  congr with t  unfold distribution  congr with x  unfold Set.indicator  simp only [enorm_eq_self]  have : (X ∩ {x | t < ‖f x‖ₑ}) x = (x ∈ X ∧ t < ‖f x‖ₑ) := rfl  rw [this]  split_ifs with hx <;> simp [hx]