Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.lintegral_trunc_mul₁

Carleson.ToMathlib.RealInterpolation.Misc · Carleson/ToMathlib/RealInterpolation/Misc.lean:1052 to 1065

Mathematical statement

Exact Lean statement

lemma lintegral_trunc_mul₁ {g : ℝ → ℝ≥0∞} {j : Bool} {x : α} {p : ℝ} {tc : ToneCouple} :
    ∫⁻ s : ℝ in res' (xor j tc.mon) (tc.inv ‖f x‖ₑ), (g s) * ‖trnc j f (tc.ton (ENNReal.ofReal s)) x‖ₑ ^ p =
    ∫⁻ s : ℝ in res (xor j tc.mon) (tc.inv ‖f x‖ₑ), (g s) * ‖trnc j f (tc.ton (ENNReal.ofReal s)) x‖ₑ ^ p

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma lintegral_trunc_mul₁ {g : ℝ → ℝ≥0∞} {j : Bool} {x : α} {p : ℝ} {tc : ToneCouple} :    ∫⁻ s : ℝ in res' (xor j tc.mon) (tc.inv ‖f x‖ₑ), (g s) * ‖trnc j f (tc.ton (ENNReal.ofReal s)) x‖ₑ ^ p =    ∫⁻ s : ℝ in res (xor j tc.mon) (tc.inv ‖f x‖ₑ), (g s) * ‖trnc j f (tc.ton (ENNReal.ofReal s)) x‖ₑ ^ p := by  apply setLIntegral_congr  unfold res res'  split_ifs  · simp  · simp  · exact Ioo_ae_eq_Ioc.symm  · by_cases h : (tc.inv ‖f x‖ₑ).toReal = 0; · rw [h, inter_eq_left.mpr Ioi_subset_Ici_self]    rw [inter_eq_right.mpr]    · exact Ioi_ae_eq_Ici.symm    · refine Ici_subset_Ioi.mpr <| toReal_pos ?_ (by assumption)      exact Ne.symm (ne_of_apply_ne ENNReal.toReal fun a ↦ h (id (Eq.symm a)))