Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.restrict_to_support_trnc

Carleson.ToMathlib.RealInterpolation.Minkowski · Carleson/ToMathlib/RealInterpolation/Minkowski.lean:440 to 453

Mathematical statement

Exact Lean statement

lemma restrict_to_support_trnc {p : ℝ} {j : Bool} [TopologicalSpace E₁]
  [ESeminormedAddMonoid E₁] (hp : 0 < p) (f : α → E₁) :
    ∫⁻ x : α in (fun x ↦ ‖f x‖ₑ).support, ‖trnc j f t x‖ₑ ^ p ∂μ =
    ∫⁻ x : α, ‖trnc j f t x‖ₑ ^ p ∂μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma restrict_to_support_trnc {p : ℝ} {j : Bool} [TopologicalSpace E₁]  [ESeminormedAddMonoid E₁] (hp : 0 < p) (f : α → E₁) :    ∫⁻ x : α in (fun x ↦ ‖f x‖ₑ).support, ‖trnc j f t x‖ₑ ^ p ∂μ =    ∫⁻ x : α, ‖trnc j f t x‖ₑ ^ p ∂μ := by  apply setLIntegral_eq_of_support_subset  unfold Function.support -- trnc trunc truncCompl  rw [setOf_subset_setOf]  intro x  contrapose!  have : ‖trnc j f t x‖ₑ ≤ ‖f x‖ₑ := by    exact trnc_le_func  intro h  refine (rpow_eq_zero_iff_of_pos hp).mpr ?_  simp_all